SC Chapter 5 SMT Solving

1. Replace equalities by boolean variables into phi_sk // So-called over-approximative propositional skeleton

2. Add transitivity constraints into phi_trans for each cycle in E-Graph // Otherwise they are lost

3. Check phi^PL := phi_sk \land phi_trans

1. Only simple cycles

2. Only chord-free simple cycles

3. Make a graph chordal

1. Iff every cycle of length 4 or more has one chord

2. Only constraint triangles (polynomial effort)

1. Create phi_sk

2. Make a chordal version of G^E(phi^E)

3. phi_trans = true

4. Add to phi_trans for each triangle (ex \land ey) → ez

5. Return phi_sk \land phi_trans

1. Model bit-level operations (F and P) by boolean circuits

2. Use Tseitin’s encoding to generate phi^PL

3. Use SAT solver

4. Convert solution back to the theory

5. Efficient solution e.g. Clarke et al. With CBMC

Switches between SAT solver and theory

1. Put boolean abstraction of phi into SAT solver

2. If unsatisfiable return UNSAT

3. Put (in)equation set into theory solver

4. If satisfiable return SAT

5. Put explanation into SAT solver and move to step 2.

1. Each constraint is a boolean variable

2. Solve the PL formula with variable order and first false

1. Find conflicting true constraints

2. Compute a partition defining the equivalence classes of terms // Uninterpreted functions get their own equivalence classes

Add conflicting constraints to PL formula

1. Init with no (dis)equations, empty partition and state=SAT

2. Put boolean abstraction of phi in CNF into SAT solver

3. If solution return SAT elseif unsatisfiable return UNSAT

4. Put (in)equation set into theory solver(s)

5. Put (partial) SAT or UNSAT explanation into SAT solver and move to step 3.

1. Be incremental using previous for next check

2. Compute (minimal) infeasible subsets for a reason of unsatisfaction

3. Backtrack removing constraints in chronological order

1. For new equation check previous disequations

2. For new disequations check them

Set of equations proving t=t’ and disequation t=t’

1. Some approaches strictly divides between logical structure and theory constraints some not

2. E.g propagate in the SAT-solver bounds on theory variables

1. SMT-LIB exists with language benchmarks tutorials

2. SMT-COMP exists with measuring performance and capabilities of tools

3. SMT workshops are held annually

1. First theory and then SAT solver

2. Transformation of all NP-complete problems with polynomial effort to equivalent SAT problems // Not always most effective

First SAT solver and then theory

1. UCLID

2. STP

3. Spear

4. Boolector

5. Beaver

6. SONOLAR

7. SWORD

8. CVC3

9. MathSAT

10. Z3

1. Propositional with equalities (P) and uninterpreted functions (F)

2. Both are NP-complete thus they model same decision problems

3. Input in NNF

4. Formula of propositional logic is phi^B

5. Formula with equalities is phi^E

6. Formula with equalities and uninterpreted functions is phi^UF

Algorithm for phi^UF in polynomial time

1. Replace f(a) by x_f(a)

2. Assume that for all a,b in Dⁿ that f(a)!=f(b) → a!=b

1. Ackermann’s and 2. Bryant’s

1. phi^E := phi_flat \land phi_cong with phi_flat is a flattening of phi^UF and phi_cong is a conjunction of constraints for functional congruence

2. phi^E := phi_cong → phi_flat [which is the proper definition

1. Every F(x) is replaced by f_x in phi_flat

2. Every G(F(x)) is replaced by g_fx in phi_flat

1. or all pairs F(x),F(y) insert (x=y→f_x=f_y) into phi_cong

2. For all pairs G(F(x)),G(F(y)) insert (x=y→fx=fy \land fx=fy→g_fx=g_fy) into phi_cong

3. For all paris F(a,x),F(b,y) insert ((a=b \land x=y) → f_ax=f_by) into phi_cong

1. Consider cases Fi*

2. Values of function are compared

3. Free mappings are considered fi and exchanged with F

1. E-graphs and 2. Sparse Method

1. Extract set E= (dashed) and E!= (solid)

2. Equality graph G^E(phi^E) = <V,E=,E!=>

3. Ignores boolean structure of phi^E representing an abstraction