Satisfiability Modulo

In this lecture by Sriram Rajamani, key topics covered include the integration of theory solvers, Nelson-Oppen method for combining theories in conjunctive formulas, and deciding satisfiability of disjunctive theory formulas using SAT solvers. The discussion delves into stably infinite theories, convex theories, and the conditions under which the Nelson-Oppen procedure works effectively, showcasing a comprehensive understanding of Satisfiability Modulo Theories.

• SMT
• Solvers
• Nelson-Oppen
• Theory
• Formulas

xitlallyp Follow

Uploaded on Mar 03, 2025 | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.

Presentation Transcript

1. Satisfiability Modulo Theories Lecture 4(a) Sriram Rajamani (some parts adapted from notes/slides by Leo DeMoura and Emina Torlak)

2. What we have covered so far Last week: SAT solvers Last lecture: SMT (Satsifiability Modulo Theories) Theory solvers (to decide satisfiability of conjunctive quantifier free formulas) EUF - Congruence closure DIA - Negative cycle detection --Bellman Ford LRA - Simplex, Fourier-Motzkin LIA - Branch and bound, combinatorial search Today: Nelson-Oppen method for combining theories (still conjunctive, quantifier free formulas) Deciding satisfiability of disjunctive theory formulas using SAT solvers

3. Solvers for combination of theories Example: ? ? + ? ? ? ? + ? ? Contains functions and relations from two different theories: EUF LRA

4. Nelson-Oppen procedure Example: ? ? + ? ? ? ? + ? ?

5. Nelson-Oppen procedure Works under certain conditions: 1 . Both formulas are conjunctive and quantifier free 2. Equality is the only symbol in the intersection of 1 and 2 2. Both theories are stably infinite 3. Both theories are convex Example: ? ? + ? ? ? ? + ? ? A theory T is stably infinite iff for every satisfiable ? formula ?, there is a T model that satisfies ? and has a universe of infinite cardinality A theory ? is convex if for every conjunctive formula ?, if ? ?1= ?1 ?2= ?2 ??= ?? for some finite ? > 1 then we have that ? ??= ?? for some ? 1,2, ? In other words: If ? implies a disjunction of equalities, then it also implies one of the equalities

6. Stably infinite? 1. ?= ?,?,= Axiom: ?. ? = ? ? = ? 2. Fixed width bit vectors 3. EUF 4. LIA 5. LRA 6. Arrays A theory T is stably infinite iff for every satisfiable ? formula ?, there is a T model that satisfies ? and has a universe of infinite cardinality

7. Stably infinite? 1. ?= ?,?,= Axiom: ?. ? = ? ? = ? 2. Fixed width bit vectors 3. EUF 4. LIA 5. LRA 6. Arrays A theory T is stably infinite iff for every satisfiable ? formula ?, there is a T model that satisfies ? and has a universe of infinite cardinality

8. Convex ? LIA A theory ? is convex if for every conjunctive formula ?, if ? ?1= ?1 ?2= ?2 ??= ?? for some finite ? > 1 then we have that ? ??= ?? for some ? 1,2, ? In other words: If ? implies a disjunction of equalities, then it also implies one of the equalities LRA EUF

9. Convex ? LIA 1 ? ? 2 ? = 1 ? = 2, but 1 ? ? 2 ? = 1 and 1 ? ? 2 ? = 2 LRA A theory ? is convex if for every conjunctive formula ?, if ? ?1= ?1 ?2= ?2 ??= ?? for some finite ? > 1 then we have that ? ??= ?? for some ? 1,2, ? In other words: If ? implies a disjunction of equalities, then it also implies one of the equalities EUF

10. Convex ? LIA 1 ? ? 2 ? = 1 ? = 2, but 1 ? ? 2 ? = 1 and 1 ? ? 2 ? = 2 LRA A theory ? is convex if for every conjunctive formula ?, if ? ?1= ?1 ?2= ?2 ??= ?? for some finite ? > 1 then we have that ? ??= ?? for some ? 1,2, ? In other words: If ? implies a disjunction of equalities, then it also implies one of the equalities EUF

11. Purification: example ? ? + ? ? ? ? + ?(?) Purification

12. Purification: example ? ? + ? ? ? ? + ?(?) Purification

13. Purification: example ? ? + ? ? ? ? + ?(?) Purification

14. Nelson-Oppen procedure (for Convex theories)

15. Nelson-Oppen procedure (for Convex theories) ?(?(?) ?(?)) ?(?) ? ? ? + ? ? 0 ?

16. Nelson-Oppen procedure (for Convex theories) ?(?(?) ?(?)) ?(?) ? ? ? + ? ? 0 ?

17. Nelson-Oppen procedure (for Convex theories) ?(?(?) ?(?)) ?(?) ? ? ? + ? ? 0 ? (will formally define convexity later)

18. Nelson-Oppen procedure (for Convex theories) ?(?(?) ?(?)) ?(?) ? ? ? + ? ? 0 ? (will formally define convexity later)

19. Homework Nelsson-Oppen procedure can be extended to non-convex theories, at more computational cost. Find out how to do this.

20. How to handle disjunctions? Nelson-Oppen helps us handle conjunctive formula mixed across theories. Example: ? ? ? ? ? ? ? ? ? ? + ? ? 0 ? Disjunctions need a new approach. Example: ? 0,? = ? + 1,(? > 2 ? < 1) Modern SMT solvers use a SAT solver to handle disjunctions!

21. DPLL(T): Handling disjunctions using SAT Basic Idea: 1. Abstract theory formula ? to propositional formula ??= ?2? ? 2. Send ?? to SAT solver 3. If ?? is UNSAT then ? is UNSAT 4. If ??is SAT Let ? be a satisfying assignment for ?? Concretize ? to a theory formula ??= ?2?(?) Check if ?? is SAT using Nelson-Oppen If ?? is SAT then ? is SAT Else add negation of unsat core of ?? as conflict clause to ? and loop back to Step 1. ? 0,? = ? + 1,(? > 2 ? < 1)

22. DPLL(T): Handling disjunctions using SAT Basic Idea: 1. ? 0,? = ? + 1,(? > 2 ? < 1) Abstract theory formula ? to propositional formula ??= ?2? ? Send ?? to SAT solver If ?? is UNSAT then ? is UNSAT If ??is SAT Let ? be a satisfying assignment for ?? Concretize ? to a theory formula ??= ?2?(?) Check if ?? is SAT using Nelson-Oppen If ?? is SAT then ? is SAT Else add negation of unsat core of ?? as conflict clause to ? and loop back to Step 1. 2. 3. 4.

23. DPLL(T): Optimizations(1) ?1= ? 0,?2= ? = ? + 1, ?4= ? < 1,?5= ? < 2 ?3= ? > 2, Incrementality: Pass literals to the Theory solver as they are assigned by the SAT solver

24. DPLL(T): Optimizations(1) ?1= ? 0,?2= ? = ? + 1, ?4= ? < 1,?5= ? < 2 ?3= ? > 2, Incrementality: Pass literals to the Theory solver as they are assigned by the SAT solver

25. DPLL(T): Optimizations(2) ?1= ? 0,?2= ? = ? + 1, ?4= ? < 1,?5= ? < 2 ?3= ? > 2, Theory Propagation: SMT equivalent of unit propagation

26. DPLL(T): Optimizations(2) ?1= ? 0,?2= ? = ? + 1, ?4= ? < 1,?5= ? < 2 ?3= ? > 2, Theory Propagation: SMT equivalent of unit propagation

27. DPLL(T): Optimizations(2) ?1= ? 0,?2= ? = ? + 1, ?4= ? < 1,?5= ? < 2 ?3= ? > 2, Theory Propagation: SMT equivalent of unit propagation

28. Homework Go through Z3 online tutorial at https://rise4fun.com/z3/tutorial Come up with problems from your own research interests that can be encoded as SMT formulas and try running Z3 on these