Formalizing Methods for Propositional Model Counting and Enumeration

Many real-world problems, such as probabilistic reasoning, can be formulated as the task of counting the models of a propositional formula, called #SAT. A model of a formula is an assignment to its variables such that the formula evaluates to true. Related to model counting is model enumeration, or All-SAT, in which the models of a formula are recorded. It is applied, e. g., in model checking and verification. Both #SAT and All-SAT are therefore of practical relevance. In principle, we could check for every possible assignment whether it is a model of the formula. However, formulae stemming from real-world applications might be defined over thousands or millions of variables, and the number of possible assignments is exponential in the number of variables occurring in the formula. Clearly, checking them one by one is prohibitive. Therefore, state-of-the-art #SAT solvers partition the input formula into subformulae over pairwise disjoint sets of variables, called components, process them separately, and then combine the results. Each subformula is defined over a potentially small subset of the set of input variables, and the search space to be processed in each computation might be significantly smaller than the whole search space. Another means to reduce the number of assignments to be checked is to detect partial models, i. e., models in which not all variables occur. A partial model represents a set of total models whose size is exponential in the number of unassigned variables. The corresponding total assignments need not be checked one by one, hence partial model detection bears the potential to significantly reduce work in both space and time. In this thesis, we develop and rigorously formalize methods for propositional model counting and enumeration with a focus on the detection of partial models. We first present two dual model counting methods. Simultaneously processing the formula and its negation enables us to detect short partial models. Our first approach is based on the Davis-Putnam-Loveland-Logemann (DPLL) algorithm. Our second method implements methods used in modern SAT solvers, such as conflict-driven clause learning (CDCL) and conflict-driven backjumping. However, backjumping might cause the solver to repeat assignments just undone. To avoid these repetitions at least in part, conflict-driven clause learning was combined with chronological backtracking. In the context of model enumeration and counting, this allows for efficiently escaping search space regions without models while exploring the search space neighboring previously detected models. We formalize this method, which is called chronological CDCL, and its application to non-dual model counting and provide correctness proofs. Partial models can be detected by checking whether a partial assignment already logically entails the input formula. We present this entailment check in four flavors of different strengths and computational complexity some of which make use of dual reasoning. Since entailment checks might be expensive, we finally present a method for shrinking total models by means of dual reasoning. The focus of our work is on formalization and proofs. Preliminary results, either theoretical or experimental, show that the methods presented in this thesis enable us to find short partial models. Our methods are applicable in various domains and point out future directions for research in #SAT and All-SAT.

Keywords: propositional logic, propositional satisfiability, model counting, model enumeration, SAT, #SAT, All-SAT, formalization