SMT Solving for Equalities and Uninterpreted Functions

Satisfiability Checking is the task of checking the existence of a satisfying solution for a logical formula. For propositional logic formulas, being Boolean combinations of propositions such as $a \wedge (b\vee c)$ , SAT solvers can be used to determine whether there is an assignment mapping to each proposition a value either true or false, such that substituting these values into the formula, the formula evaluates to true.

For the satisfiability check of quantifier-free first-order logic formulas over different theories, SAT solvers can be extended with theory solver modules, resulting in SAT-modulo-theories (SMT) solvers. Thereby we move from checking satisfiability for propositional logic formulas, such as $a \wedge (b\vee c)$ , towards checking satisfiability for formulas such as $x < 5 \wedge (x \geq y^{2} \vee y < 2\cdot x)$ . Such logics can be syntactically more rich as well as semantically more expressive than propositional logic, and allow the natural formalisation of a wide range of practical problems, e.g., in scheduling, planning, software verification, or controller synthesis.

This practical course aims at the design, implementation, and optimization of state-of-the-art decision procedures for SMT solving for the theories of equality logic and uninterpreted functions. Equality logic is an extension of propositional logic with a theory, allowing the usage of constants and variables having values from some domain, and equality as the only predicate. I.e., equality logic formulas are Boolean combinations of equalities between constants and variables. An example for a satisfiable equality logic formula is $(a=b \wedge b=c) \rightarrow a=c$ , an example for an unsatisfiable formula is $a=b \wedge b=c \wedge a\not=c$ . In the theory of uninterpreted functions, additionally to constants and variables, we can use function symbols in theory terms. The semantics of the function symbols is not specified (i.e. they are “uninterpreted”); the only constraint on their semantics is functional congruence, i.e., $t_1=t_2 \rightarrow F(t_1)=F(t_2)$ for all theory terms $t_1$ , $t_2$ and function symbols $F$ . For example, $a\not=b \wedge F(a)=F(b)$ is a satisfiable formula, whereas $a=b \wedge F(a)\not= F(b)$ is unsatisfiable.

The implementation will take place within the SMT-RAT project and can benefit from its manifold features. The resulting SMT solver will be tested on the official SMT-LIB benchmarks and be compared to state-of-the-art SMT solvers. Furthermore, we will form at least two teams and compare their solvers within a competition.

Slides

Exercises