Papers

The paper proposes a probabilistic generalization of the well-known Strong Backdoor Set~(SBS) concept applied to the Boolean Satisfiability Problem (SAT). We call a set of Boolean variables $B$ a $\rho$-backdoor, if for a fraction $\rho$ of possible assignments of variables from $B$, assigning their values to variables in a Boolean formula in Conjunctive Normal Form (CNF) results in polynomially solvable formulas. Clearly, a $\rho$-backdoor with $\rho=1$ is an SBS. For a given set $B$ it is possible to efficiently construct an $(\varepsilon, \delta)$-approximation of parameter $\rho$ using the Monte Carlo method. Thus, we define an $(\varepsilon, \delta)$-SBS as such a set $B$ for which the estimation of the parameter $\rho$ deviates from 1 by no more than $\varepsilon$ with probability no less than $1-\delta$. We consider the problems of finding the minimum SBS and the minimum $(\varepsilon, \delta)$-SBS. To solve the former, one can use the algorithm described by R.~Williams, C.~Gomes and B.~Selman in 2003. In the paper we propose a new probabilistic algorithm to solve the latter, and show that the asymptotic estimation of the worst case complexity of the proposed algorithm is significantly smaller than that of the algorithm by Williams~et~al. For practical applications, we suggest a metaheuristic optimization algorithm based on the penalty function method to seek the minimal $(\varepsilon, \delta)$-SBS. Results of computational experiments show that the use of $(\varepsilon, \delta)$-SBSes found by the proposed algorithm allows speeding up solving of test problems related to equivalence checking and hard crafted and combinatorial benchmarks compared to state-of-the-art SAT solvers.

poster session 6 @ blue 4, poster session 10 @ blue 4, oral session 6 @ blue 4, poster session 6, poster session 10, oral session 6

The growing interest in explainable artificial intelligence(XAI) for critical decision-making motivates the need for interpretable machine learning (ML) models. In fact, due to their structure (especially with small sizes), these models are inherently understandable by humans. Recently, several exact methods for computing such models are proposed to overcome weaknesses of traditional heuristic methods by providing more compact models or better prediction quality. Despite their compressed representation of Boolean functions, Binary decision diagrams (BDDs) did not gain enough interest as other interpretable ML models. In this paper, we first propose SAT-based models for learning optimal BDDs (in terms of the number of features) that classify all input examples. Then, we lift the encoding to a MaxSAT model to learn optimal BDDs give limited depths, that maximize the number of examples correctly classified. Finally, we tackle the fragmentation problem by introducing a method to merge compatible subtrees for the BDDs found via the MaxSAT model. Our empirical study shows clear benefits of the proposed approach in better prediction performance compared to the existing heuristic approach, and better interpretability and lighter en-coding size compared to the state-of-the-art approaches.

poster session 6 @ blue 4, poster session 10 @ blue 4, oral session 6 @ blue 4, poster session 6, poster session 10, oral session 6

Finding diverse solutions in combinatorial problems recently has received considerable attention (Baste et al. 2020, Fomin et al. 2020, Hanaka et al. 2021). In this paper we study the following type of problems: given an integer $k$, the problem asks for $k$ solutions such that the sum of pairwise (weighted) Hamming distances between these solutions is maximized. Such solutions are called \emph{diverse solutions}. We present a polynomial-time algorithm for finding diverse shortest $st$-paths in weighted directed graphs. Moreover, we study the diverse version of other classical combinatorial problems such as diverse weighted matroid bases, diverse weighted arborescences, and diverse bipartite matchings. We show that these problems can be solved in polynomial time as well. To evaluate the practical performance of our algorithm for finding diverse shortest $st$-paths, we conduct a computational experiment with synthetic and real-world instances. The experiment shows that our algorithm successfully computes diverse solutions within reasonable computational time.

poster session 6 @ blue 4, poster session 10 @ blue 4, oral session 6 @ blue 4, poster session 6, poster session 10, oral session 6