Papers

Tree ensembles (TEs) denote a prevalent machine learning model that do not offer guarantees of interpretability, that represent a challenge from the perspective of explainable artificial intelligence. Besides model agnostic approaches, recent work proposed to explain TEs with formally-defined explanations, which are computed with oracles for propositional satisfiability (SAT) and satisfiability modulo theories. The computation of explanations for TEs involves linear constraints to express the prediction. In practice, this deteriorates scalability of the underlying reasoners. Motivated by the inherent propositional nature of TEs, this paper proposes to circumvent the need for linear constraints and instead employ an optimization engine for pure propositional logic to efficiently handle the prediction. Concretely, the paper proposes to use a MaxSAT solver and exploit the objective function to determine a winning class. This is achieved by devising a propositional encoding for computing explanations of TEs. Furthermore, the paper proposes additional heuristics to improve the underlying MaxSAT solving procedure. Experimental results obtained on a wide range of publicly available datasets demonstrate that the proposed MaxSAT-based approach is either on par or outperforms the existing reasoning-based explainers, thus representing a robust and efficient alternative for computing formal explanations for TEs.

poster session 2 @ blue 4, poster session 9 @ blue 4, oral session 9 @ blue 4, poster session 2, poster session 9, oral session 9

The k-undercover Boolean Matrix Factorization problem aims at approximating an (m×n) Boolean matrix X as the Boolean product of an (m×k) and a (k×n) matrices A ◦ B such that X is a cover of A ◦ B, i.e., no representation error is allowed on the 0’s entries of the matrix X. In this paper, we propose two exact methods based on MaxSAT encodings to infer optimal and “block-optimal” k-undercover. From a theoretical standpoint, we prove that our method of inferring “block-optimal” k-undercover is a (1−1/e)-approximation for the optimal k-undercover problem, and from a practical standpoint, experimental results show that our “block-optimal” k-undercover algorithm outperforms the state of the art even when compared with algorithms for the more general k-undercover Boolean Matrix Factorization problem for which only minimizing reconstruction error is required.

poster session 2 @ blue 4, poster session 9 @ blue 4, oral session 9 @ blue 4, poster session 2, poster session 9, oral session 9

MAX k-SAT is one of canonical NP-hard problems. Its variation called random MAX k-SAT problem was suggested in order to understand how hard it is to solve instances of the problem on average. The most common random model from which random instances get sampled is the uniform model. However, the uniform model, while useful for studying properties of the space of all k-CNF formulas as a whole, cannot capture all the structural properties we observe in the real-world instances. Therefore, we propose to use another random model called configuration model, which is able to produce instances with an arbitrary variable's degree distribution. Thus, we may focus and ``probe'' different regions of the space of all k-CNF formulas. There are many questions one may ask about the instances from configuration model, and in this paper we study how effective the pure literal elimination rule (or heuristic) performs when solving random MAX k-SAT instances having an arbitrary but fixed variable's degree distribution. We provide an equality that depends on the distribution of degrees, solving which one obtains the number of clauses the pure literal elimination rule satisfies. We also show how the distribution of variable degrees changes over time as the heuristic progresses.

poster session 2 @ blue 4, poster session 9 @ blue 4, oral session 9 @ blue 4, poster session 2, poster session 9, oral session 9