← Back to program

SAT/SMT

Session introduction · Wednesday, 15:30-17:00 · Chair: Dirk Beyer

Most verification tools do not reason by hand. They translate a question into a logical formula and hand it to a solver, and this session is about those solvers. The starting point is Boolean satisfiability, or SAT: given a formula built from true/false variables, is there an assignment that makes the whole formula true? SAT was the first problem proved NP-complete, so it can be very hard in the worst case, yet it is the building block for everything else here [1]. Even so, modern SAT solvers handle large formulas well, using a search method called conflict-driven clause learning (CDCL) that learns from each dead end to prune the remaining search [2]. Some applications need not one solution but all of them, a task called AllSAT, or model enumeration. The textbook approach adds a blocking clause to rule out each solution once it is found, but that is costly, so recent work instead lets the enumerator plug into the solver through an interface called IPASIR-UP [3].

SAT only knows plain true/false variables, so on its own it cannot talk about numbers, arrays, or other data. Satisfiability modulo theories, or SMT, closes that gap: it keeps the SAT search but adds background theories that fix the meaning of extra symbols, such as integers or arrays [4]. SMT solvers are the workhorse backend of many verification tools [5]. For each theory, a decision procedure determines whether a set of constraints in that theory can be satisfied, and whether such a procedure can exist at all, its decidability, is the central question [6]. There is also an asymmetry between the two answers. Showing that a formula is unsatisfiable often has a compact proof, but showing that it is satisfiable usually means exhibiting a model, which can be very large or, for some theories, impossible to build directly. One response is to certify satisfiability with an inductive argument that a model exists, instead of constructing it outright.

The talks put several such theories to work. Uninterpreted functions are functions with no fixed meaning, constrained only by the rule that equal inputs give equal outputs. Combined with universal quantifiers, which are claims that must hold for all values, they become undecidable in general [6]. Linear integer arithmetic (LIA) is a central decidable theory of constraints over the integers, and one line of work extends it with sums over sets of values. The theory of arrays models reading and writing indexed memory, and it too can be extended, here with summation over an array [7]. Strings form another rich theory: constraints over text, such as equalities, lengths, and pattern or replace operations, which matter in security and program analysis [8]. Modern string solvers are often automata-based, using finite automata to describe sets of strings and transducers to describe relations between strings, such as replacing one substring with another [9].

Keywords to look up: Boolean satisfiability (SAT) · NP-complete · CDCL · SAT solver · AllSAT / model enumeration · blocking clause · satisfiability modulo theories (SMT) · theory · decision procedure · decidability · uninterpreted function · quantifier · linear integer arithmetic (LIA) · theory of arrays · satisfiability certificate · string solving · finite automaton · transducer.

Sources

  1. S. A. Cook. "The Complexity of Theorem-Proving Procedures." STOC, 1971. doi.org/10.1145/800157.805047
  2. J. P. Marques-Silva, K. A. Sakallah. "GRASP: A Search Algorithm for Propositional Satisfiability." IEEE Trans. Computers, 1999. doi.org/10.1109/12.769433
  3. K. Fazekas, A. Niemetz, M. Preiner, M. Kirchweger, S. Szeider, A. Biere. "IPASIR-UP: User Propagators for CDCL." SAT, 2023. doi.org/10.4230/LIPIcs.SAT.2023.8
  4. C. Barrett, C. Tinelli. "Satisfiability Modulo Theories." In Handbook of Model Checking, Springer, 2018. doi.org/10.1007/978-3-319-10575-8_11
  5. L. de Moura, N. Bjørner. "Z3: An Efficient SMT Solver." TACAS, 2008. doi.org/10.1007/978-3-540-78800-3_24
  6. D. Kroening, O. Strichman. Decision Procedures: An Algorithmic Point of View. Springer, 2nd ed., 2016. doi.org/10.1007/978-3-662-50497-0
  7. A. R. Bradley, Z. Manna, H. B. Sipma. "What's Decidable About Arrays?" VMCAI, 2006. doi.org/10.1007/11609773_28
  8. R. Amadini. "A Survey on String Constraint Solving." ACM Computing Surveys, 2021. doi.org/10.1145/3484198
  9. J. E. Hopcroft, R. Motwani, J. D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 3rd ed., 2006. ISBN 978-0-321-45536-9.