Satisfiability Checking: Theory and Applications
Satisfiability checking aims to develop algorithms and tools for checking the satisfiability of existentially quantified logical formulas. Besides powerful SAT solvers for solving propositional logic formulas, sophisticated SAT-modulo-theories (SMT) solve
- PDF / 548,765 Bytes
- 15 Pages / 439.37 x 666.142 pts Page_size
- 47 Downloads / 216 Views
Abstract. Satisfiability checking aims to develop algorithms and tools for checking the satisfiability of existentially quantified logical formulas. Besides powerful SAT solvers for solving propositional logic formulas, sophisticated SAT-modulo-theories (SMT) solvers are available for a wide range of theories, and are applied as black-box engines for many techniques in different areas. In this paper we give a short introduction to the theoretical foundations of satisfiability checking, mention some of the most popular tools, and discuss the successful embedding of SMT solvers in different technologies.
1
Introduction
First-order-logic is a powerful modelling formalism frequently used to specify problems in different areas like verification, termination analysis, test case generation, controller synthesis, equivalence checking, combinatorial tasks, scheduling, planning, and product design automation and optimisation, just to mention a few well-known examples. Once the problem is formalised, algorithms and their implementations are needed to check the validity or satisfiability of the formulas, and in case they are satisfiable, to identify satisfying solutions. Algorithms to solve this problem are called decision procedures. In mathematical logic, in the early 20th century some novel decision procedures were developed for arithmetic theories. With the advent of computer systems, big efforts were made to provide automated solutions in form of practically feasible implementations of decision procedures. In the area of symbolic computation, this development led to computer algebra systems supporting all kinds of scientific computations. Another line of research, satisfiability checking [10], started to focus on the more specific aim of checking the satisfiability of existentially quantified logical formulas. For Boolean propositional logic, which is known to be NP-complete, in the late ’90s impressive progress was made in the area of satisfiability checking, resulting in powerful SAT solvers. The first idea used resolution for quantifier elimination [30], but it had serious problems with the explosion of the memory requirements with increasing problem size. A combination of enumeration and Boolean constraint propagation [29] brought important enhancements. Another major improvement was achieved by a novel combination of enumeration, Boolean constraint propagation and resolution, leading to conflict-driven c Springer International Publishing Switzerland 2016 R. De Nicola and E. K¨ uhn (Eds.): SEFM 2016, LNCS 9763, pp. 9–23, 2016. DOI: 10.1007/978-3-319-41591-8 2
10
´ E. Abrah´ am and G. Kremer
clause-learning and non-chronological backtracking [50]. Later on, this impressive progress was continued by novel efficient implementation techniques (e.g., sophisticated decision heuristics, two-watched-literal scheme, restarts, cache performance, etc.). Also different extensions are available, for example QBF solvers for quantified Boolean formulas, Max-SAT solvers to find solutions which satisfy a maximal number of clauses, or #SAT solvers to
Data Loading...
