There we SAT down

Keywords: Reasoning, SAT, Description Logics

SAT solving is a non-numeric constraint problem involving Boolean logic. SAT (short for "satisfiability") determines the ability for a propositional formula to be satisfied by some assignment of truth values to its variables. Its significance is wide:

• Many reasoning problems can be reduced to SAT or one of its variants or extensions. Configuration and logic verification problems are frequently addressed with SAT solvers.
• SAT is the quintessential problem in the study of complexity of computation. It has been shown to be NP-complete. Many problems have been shown to be as hard to solve as SAT and because SAT is well understood, it is strong evidence of the complexity theory conjecture that the class of problems designated as P is not equivalent to the class NP.
• Much progress has been made toward the creation of efficient SAT solvers for problems as they tend to arise in the real world. In other words, just because a problem is theoretically intractable across all possible problems does not imply that the problems that are actually encountered will be intractable given some approach.
• Many of the techniques employed in state-of-the-art SAT solvers can be applied to the implementation of other reasoning mechanisms such as Description Logic ("DL"), Temporal Logic and other theorem provers.
• Some of the sub-problems of inference within a DL, Temporal Logic or other theorem prover can be exported to a SAT solver.

This post addresses in brief a problem that is at the heart of DL reasoning and some techniques used to solve SAT constraint problems.

Defining the problem formally

The Boolean Satisfiability (SAT) problem consists of determining a satisfying variable assignment, V, for a Boolean function, f, or determining that no such V exists. Most solvers operate on problems for which f is specified in conjunctive normal form (CNF). This form consists of the logical AND of one or more clauses, which consist of the logical OR of one or more literals. The literal comprises the fundamental logical unit in the problem, being merely an instance of a variable or its complement. All Boolean functions can be described in the CNF format. The advantage of CNF is that in this form, for f to be satisfied, each individual clause must be satisfied.

The usual approaches to SAT are modifications of a method proposed by Davis, Putnam, Logemann, and Loveland for backtracking through a search space that is explored using Boolean constraint propagation (BCP). BCP is based on the observation that if a clause whose literals are all 0 save one is to be satisfied, then that single literal must be assigned the value 1. That variable assignment is propagated to all clauses forcing each to be satisfied (and eliminated), false (forcing backtracking over the assignment and to a previous choice point), unit (again all 0 save one and a candidate for BCP), or unknown (more than one literal unknown).

BCP is applied until there is a contradiction, all clauses have been satisfied and removed, or all remaining clauses have at least 2 unknown literals. A choice must be made for assignment, a choice point is recorded, and the variable assignment is propagated. Again, some clauses may be satisfied, false, unit, or have more than one unknown (with the remaining literals 0). BCP and choices ("splitting") continues until satisfiability has been determined.

Modern SAT solvers employ many refinements. Some of these are:

• Conflict analysis and non-chronological backtracking
• Recording conflicts so portions of a previously searched subtree are not searched again
• Heuristics to select which variable is to be assigned a value when BCP does not apply
• Splitting heuristics which choose which of the two phase assignments is made first for a variable
• Restarts where the solver abandons the current search tree

All the state-of-the-art versions of SAT are based on "lazy" data structures for clauses which "watch" literals in some form to efficiently recognize opportunities for BCP.

Various extensions and variant problems to SAT have been developed. The two most interesting directions are QSAT which adds universal quantification to selected variables and integration of SAT with numeric solvers. The latter extensions address problems involving Boolean functions over literals and mathematical propositions.

Quantified Number Restrictions in DLs

Description Logics often support quantified number restrictions (QNRs). A complete description of how DL languages such as SHIQ(D) or SHOIQ(D) are implemented is beyond the scope of this post but some insight may be gained in exploring some aspects of the problem in isolation.

We can understand QNR processing as a "black box" that may either return that the constraints cannot be satisfied or a (minimal) set of assertions that must be true for satisfaction. Looking more closely at a simplified version of the problem we have the following:

Inputs:

• A set of concepts that are taxonomically related in a directed acyclic graph and a collection of collectively unsatisfiable sets of concepts.
• A set of roles that are organized in a role hierarchy as a directed acyclic graph and inverse role assertions.
• A set of distinct individuals. Each individual is labelled with those concepts that are currently known to (directly) subsume it and with those concepts that are currently known to be the most general that cannot subsume it (out of contradiction).
• A set of QNRs of the form =nR.C or =nR.C

Unsatisifiable Output:

• A minimal set of individuals and QNRs that led to the contradiction.

Satisfiable Output (non-deterministic):

• A set of assertions in the form of i:C (existing individual i is asserted as a concept C)
• A set of assertions in the forms =nR.C and =nR.C

The implementation of such a black box (and its equivalent as implemented as interleaved processing of the tableau of an ABOX consistency test) has been the subject of intensive research within the Description Logic community. A spectrum of solutions ranging from direct expansion of individuals in the tableau, to signature representations which merge processing for sets of unnamed, distinct but otherwise identical individuals, to direct solving using integer programming, have been proposed. As with reasoning problems generally, no single approach dominates.

One of the complications of the problem as I have posed it above is that we seek an "explanation" for unsatisfiability and a non-deterministic set of assertions for satisfiability. The careful reader will note that there may be more than one reason for unsatisfiability and more than one satisfiable set of assertions. The explanation of unsatisfiability is input to the non-chronological backtracking control; it is hard to determine what may be a "best" explanation, any is better than none. The satisfiable output actually must create choice points whenever alternative sets of assertions may exist. Backtracking will enumerate alternatives until unsatisfiability results.

References

Babic, D.; Bingham, J.; Hu, A. J. (2006). "B-Cubing: New Possibilities for Efficient SAT-Solving" (PDF). IEEE Transactions on Computers. 55 (11): 1315. doi:10.1109/TC.2006.175.

Clarke, E.; Biere, A.; Raimi, R.; Zhu, Y. (2001). "Bounded Model Checking Using Satisfiability Solving". Formal Methods in System Design. 19: 7. doi:10.1023/A:1011276507260.

Davis, M., and Putnam, H. 1960. A computing procedure for quantication theory. Journal of the Association for Computing Machinery 7:201-215.

Davis, M.; Logemann, G.; and Loveland, D. 1962. A machine program for theorem-proving. Communications of the Association for Computing Machinery 5:394-397.

Michael R. Garey & David S. Johnson (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman. ISBN 0-7167-1045-5. A9.1: LO1 - LO7, pp. 259 - 260.

Giunchiglia, E., Narizzano, M., and Tacchella, A. Backjumping for Quantified Boolean Logic Satisfiability.

Giunchiglia, E.; Tacchella, A. (2004). Giunchiglia, Enrico; Tacchella, Armando (eds.). "Theory and Applications of Satisfiability Testing". Lecture Notes in Computer Science. 2919. doi:10.1007/b95238. ISBN 978-3-540-20851-8.

Goldberg, E., and Novikov, Y. 2002. BerkMin: a Fast and Robust SAT-Solver.

Carla P. Gomes; Henry Kautz; Ashish Sabharwal; Bart Selman (2008). "Satisfiability Solvers". In Frank Van Harmelen; Vladimir Lifschitz; Bruce Porter (eds.). Handbook of knowledge representation. Foundations of Artificial Intelligence. 3. Elsevier. pp. 89-134. doi:10.1016/S1574-6526(07)03002-7. ISBN 978-0-444-52211-5.

Lynce, I. and Marques-Silva, J. P. 2001. Efficient Data Structures for Fast SAT Solvers.

Marques-Silva, J.; Glass, T. (1999). "Combinational equivalence checking using satisfiability and recursive learning" (PDF). Design, Automation and Test in Europe Conference and Exhibition, 1999. Proceedings (Cat. No. PR00078). p. 145. doi:10.1109/DATE.1999.761110. ISBN 0-7695-0078-1.

Marques-Silva, J. P., and Sakallah, K. A. 1999. GRASP-A search algorithm for propositional satisability. IEEE Transactions on Computers 48(5):506-521.

Moskewicz, M.; Madigan, C.; Zhao, Y.; Zhang, L.; and Malik, S. 2001. Chaff: Engineering an efficient SAT solver. In Proceedings of the Design Automation Conference.

Rodriguez, C.; Villagra, M.; Baran, B. (2007). "Asynchronous team algorithms for Boolean Satisfiability" (PDF). 2007 2nd Bio-Inspired Models of Network, Information and Computing Systems. p. 66. doi:10.1109/BIMNICS.2007.4610083.

Sebastiani, R. Integrating SAT Solvers with Math Reasoners: Foundations and Basic Algorithms.

Van Gelder, A. 2001. Generalizations of Watched Literals for Backtracking Search.

Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Boolean Satisfiability Solvers and Their Applications in Model Checking". Proceedings of the IEEE. 103 (11). doi:10.1109/JPROC.2015.2455034.

Zhang, H. 1997. SATO: An effcient propositional prover. In Proceedings of the International Conference on Automated Deduction, 272-275.

Zhang, H. and Stickel, M. E. 1999. Implementing the Davis-Putnam Method.