SMT and Theorem Proving in Computer Science

lecture 14 n.w
1 / 41
Embed
Share

Dive into the world of Satisfiability Modulo Theories (SMT) and Theorem Proving in computer science. Explore the concepts of theories, candidate logic, formula meanings, proof procedures, algorithms, and theorem provers with practical examples like linear inequalities.

  • SMT
  • Theorem Proving
  • Computer Science
  • Logic
  • Algorithms
rayaanacharya
mott_ndy Follow

Uploaded on | 1 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.

Download 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.

E N D

Presentation Transcript

  1. Lecture 14 SMT and Theorem Proving Armando Solar-Lezama partially based on slides by Isil Dillig http://www.cs.utexas.edu/~isil/cs780-02/lecture16.pdf

  2. What is a theory A language of expressions and predicates over those expressions where we have a satisfiability procedure for conjunctions over predicates

  3. Candidate Logic ? ? ???? ?1 ?2? ? ?.? ? ? ???? ?1 ?2 ? ?(?1, ,??) ? ? | ?(?1, ,??) Goals: Hypotheses Literals Background theory Gives meaning to these Expressions

  4. Candidate Logic ? ? ???? ?1 ?2 ? ? ?.? ? ? ???? ?1 ?2 ? ?(?1, ,??) ? ? | ?(?1, ,??) Goals: Hypotheses Literals Expressions Note that our alternative VC gen procedure produces formulas in this form! Assuming invariants, preconditions and postcond are all from H.

  5. Meaning of a formula ? means that formula ? holds ???? ?1 ?2 when ?1 ??? ?2 ?.? when for all ? ? ?[?/?] where D is the domain of x ? ? when ? whenever ? ?(?1, ??) when ? is true according to the theory

  6. A simple prove procedure What we want: ?????(?) = ???? iff ?

  7. A simple algorithm ????? ? = ?????(????,?) ????? ?,???? = ???? ????? ?,?1 ?2 = ????? ?,?1 ?????(?,?2) ????? ?,?1 ?2 = ?????(? ?1,?2) ????? ?, ?.? = ?????(?,? ?/? ) where ? is fresh ????? ?,? =?

  8. Theorem prover for literals Reduces the problem to ?????(?,?) H is a conjunction of literals ?1 ?? ? (?1 ?? ?) ????? ?,? = ?????(? ?)

  9. Example: Linear Inequalities ? ?? | ? + ? ? 0 | E = 0 Expressions: Literals: ?,?0,?,?0,?,? ,? , ? = ?0 ? = ?0 ? = ?0 ?0 ? = ?0+ ? ? = ?0+ ? ? > 0 ? 1 = ?0+ (? 1) ? = ?0+ ? ? > 0 ? ?0

  10. Linear Inequalities ? = ?0+ ? ? > 0 ? 1 = ?0+ (? 1) ? = ?0+ ? ? 0 ? ?0 ? = ?0+ ? ?????(????, ? = ?0 ? = ?0 ? = ?0 ?0 ) ? = ?0+ ? ? > 0 ? 1 = ?0+ (? 1) ? = ?0+ ? ? 0 ? ?0 ? = ?0+ ? ?????(? = ?0 ? = ?0 ? = ?0 ?0, )

  11. Linear Inequalities ? = ?0+ ? ? > 0 ? 1 = ?0+ (? 1) ? = ?0+ ? ? 0 ? ?0 ? = ?0+ ? ?????(? = ?0 ? = ?0 ? = ?0 ?0, ) ?????(? = ?0 ? = ?0 ? = ?0 ?0,? = ?0+ ?) ?????(? = ?0 ? = ?0 ? = ?0 ?0, ? = ?0+ ? ? > 0 ? 1 = ?0+ (? 1)) ?????(? = ?0 ? = ?0 ? = ?0 ?0,? = ?0+ ? ? 0 ? ?0)

  12. Linear Inequalities ? = ?0+ ? ? > 0 ? 1 = ?0+ (? 1) ? = ?0+ ? ? 0 ? ?0 ? = ?0+ ? ?????(? = ?0 ? = ?0 ? = ?0 ?0, ) ?????(? = ?0 ? = ?0 ? = ?0 ?0,? = ?0+ ?) ?????(? = ?0 ? = ?0 ? = ?0 ?0 ? = ?0+ ? ? > 0 ,? 1 = ?0+ (? 1)) ?????(? = ?0 ? = ?0 ? = ?0 ?0 ? = ?0+ ? ? 0 ,? ?0)

  13. Linear Inequalities ? = ?0+ ? ? > 0 ? 1 = ?0+ (? 1) ? = ?0+ ? ? 0 ? ?0 ? = ?0+ ? ?????(? = ?0 ? = ?0 ? = ?0 ?0, ) ?????(? = ?0 ? = ?0 ? = ?0 ?0 ? ?0+ ?) ?????(? = ?0 ? = ?0 ? = ?0 ?0 ? = ?0+ ? ? > 0 ? 1 ?0+ (? 1)) ?????(? = ?0 ? = ?0 ? = ?0 ?0 ? = ?0+ ? ? 0 ? > ?0)

  14. Is this enough to check VCs? Given a definition of VC ??(????,{?}) = ? ??(? = ?,{?}) = ?[?/?] ?? ?1;?2 ? ?? ?? ? ? ?? ?1 ???? ?2 ? ?? ? ???? ? ?? ?,? = = ??(?1 ??(?2{?}) ) = ? ??? ?? ?1 ? ?? ( ? ??? ?? ?2 ? ) ? ?1, ?? ? ? ?? ?,? ? ? Where x_i are variables modified in c. ?? ?????? ? ? = {? ?} ?? ?????? ? ? = {? ?}

  15. Is this enough to check VCs? Given a definition of VC ??(????,{?}) = ? ??(? = ?,{?}) = ?[?/?] ?? ?1;?2 ? ?? ?? ? ? ?? ?1 ???? ?2 ? ?? ? ???? ? ?? ?,? = = ??(?1 ??(?2{?}) ) = ? ?? ?1 ? ( ? ?? ?2 ? ) ? ?1, ?? ? ? ?? ?,? ? ? Where x_i are variables modified in c. ?? ?????? ? ? = {? ?} ?? ?????? ? ? = {? ?}

  16. Equality with uninterpreted functions Equality with uninterpreted functions Symbols: =, ,?,?, Axioms: ?=? ?2=?1 ?1=?2 ?1=?2 ?2=?3 ?1=?3 ?1=?2 ? ?1=?(?2)

  17. Equality with UF x y z t x=y y=z f(x)=f(z) g(t)=z f(y) = g(t) f(x) != f(f(f(x))) f(x) f(y) f(z) g(t) f(f(x)) f(g(t)) f(f(f(x)))

  18. Equality with UF x y z t x=y y=z f(x)=f(z) g(t)=z f(y) = g(t) f(x) != f(f(f(x))) f(x) f(y) f(z) g(t) f(f(x)) f(g(t)) f(f(f(x)))

  19. Equality with UF x y z t x=y y=z f(x)=f(z) g(t)=z f(y) = g(t) f(x) != f(f(f(x))) f(x) f(y) f(z) g(t) f(f(x)) f(g(t)) f(f(f(x)))

  20. Equality with UF x y z t x=y y=z f(x)=f(z) g(t)=z f(y) = g(t) f(x) != f(f(f(x))) f(x) f(y) f(z) g(t) f(f(x)) f(g(t)) f(f(f(x)))

  21. Equality with UF x y z t x=y y=z f(x)=f(z) g(t)=z f(y) = g(t) f(x) != f(f(f(x))) f(x) f(y) f(z) g(t) f(f(x)) f(g(t)) f(f(f(x)))

  22. Equality with UF x y z t x=y y=z f(x)=f(z) g(t)=z f(y) = g(t) f(x) != f(f(f(x))) f(x) f(y) f(z) g(t) f(f(x)) f(g(t)) f(f(f(x))) Contradiction!

  23. Nelson-Oppen Two step process Formulas ?? each in theory T? such that ? ?? Formula ? in mixed theory Equality Propagation Solution Purification

  24. Purification Break up formula ? into a set of formulas ?? each in theory T? such that ? and ?? are equisatisfiable Steps For every expression ?(?1, ,??) if ? belongs to some theory ?? and ??belongs to a different theory ??, replace ? ?? ? ? and add a constraint ? = ?? to ?? (? is a fresh variable) For every literal ?(?1, ,??) if ? belongs to some theory ?? and ??belongs to a different theory ??, replace ? ?? ? ? and add a constraint ? = ?? to ?? (? is a fresh variable)

  25. Example ? ? + ? ? ? ? + ? ? ? ? = ? ? ? = ? ? ?1 ? ?2 ? ? = ? ? ? = ? ?1= ? + ? ?2= ?3+ ?4 ?3= ? ? ?4= ? ?

  26. Equality Propagation 1) Run each UNSAT procedure independently If any returns UNSAT we are done 2) Broadcast any equalities that were discovered If no new equalities were discovered, return SAT = = Uninterpreted Fun. Linear Integer Arithmetic ? ? = ? ?1 ? ?2 ? ? = ? ? ? = ? ?3= ? ? ?4= ? ? ?1= ? + ? ?2= ?3+ ?4 ? ? = ?1 ?2 ?3 ?4 ? ? x y + + = =

  27. Equality Propagation 1) Run each UNSAT procedure independently If any returns UNSAT we are done 2) Broadcast any equalities that were discovered If no new equalities were discovered, return SAT = = Uninterpreted Fun. Linear Integer Arithmetic ? ? = ? ?1 ? ?2 ? ? = ? ? ? = ? ?3= ? ? ?4= ? ? ?1= ? + ? ?2= ?3+ ?4 ? = ?4 ? = ?3 ? ? = ?1 ?2 ?3 ?4 ? ? x y ? = ?4 ? = ?3 + + = =

  28. Equality Propagation 1) Run each UNSAT procedure independently If any returns UNSAT we are done 2) Broadcast any equalities that were discovered If no new equalities were discovered, return SAT = = Uninterpreted Fun. Linear Integer Arithmetic ? ? = ? ?1 ? ?2 ? ? = ? ? ? = ? ?3= ? ? ?4= ? ? ?1= ? + ? ?2= ?3+ ?4 ? = ?4 ? = ?3 ?1= ?2 ? ? = ?1 ?2 ?3 ?4 ? ? x y ? = ?4 ? = ?3 ?1= ?2 + + = =

  29. Equality Propagation 1) Run each UNSAT procedure independently If any returns UNSAT we are done 2) Broadcast any equalities that were discovered If no new equalities were discovered, return SAT = = Uninterpreted Fun. Linear Integer Arithmetic ? ? = ? ?? ? ?? ? ? = ? ? ? = ? ?3= ? ? ?4= ? ? ?1= ? + ? ?2= ?3+ ?4 ? = ?4 ? = ?3 ?1= ?2 ? ? = ?1 ?2 ?3 ?4 ? ? x y ? = ?4 ? = ?3 ??= ?? + + = =

  30. Soundness and Completeness Soundness (when it says unsat, it is true) Yes assuming theory solvers don t lie Completeness (will it always say unsat when required?) Yes under certain conditions Argument not as obvious

  31. Convex theories Consider the formula: 1 ? ? 2 ? ? ? 1 ? ? ?(2) Theory E 1 ? ? 2 ?1= 1 ?2= 2 Theory R ? ? ? ?1 ? ? ?(?2) No equalities to propagate The two subformulas are satisfiable Yet, the problem is clearly unsat!

  32. Convex theories A theory is convex if for every conjunctive formula F ? ??= ?? ? ??????? ? ? ??= ?? In the previous example: 1 ? ? 2 (? = 1) (? = 2) It does not imply either ? = 1 ??(? = 2)

  33. Completeness Nelson-Oppen is complete for Convex theories What to do for non-convex ones?

  34. Backtracking Consider the formula: 1 ? ? 2 ? ? ? 1 ? ? ?(2) ?? in theory E 1 ? ? 2 ?1= 1 ?2= 2 ?? in theory R ? ? ? ?1 ? ? ?(?2) Formula from theory E implies (? = ?1) (? = ?2). Try ?? ? = ?1 Try ?? ? = ?2 Since both are unsat, we can say UNSAT

  35. Backtracking Key issues How do we decide which disjunctive equalities to branch on? How to perform backtracking efficiently?

  36. Recap What we have so far: Simple boolean structure + 1 theory Simple boolean structure + multiple theories Today: Deal with complex boolean structure

  37. DPLL(T) Key idea Theory Solver Handles Theories Theory Solver 1 SAT Solver Handles Boolean Structure Theory Solver 2

  38. Boolean Abstraction Given a formula ?, a boolean abstraction ?? has the following property ????? ?? ?????(?)

  39. Eager approach Simple, sometimes efficient Find a boolean abstraction s.t. ????? ? ?????(??) Give ?? to a sat solver DONE! Can t really pull it off if you have an infinite theory

  40. Lazy approach Start with a simple boolean abstraction Check solutions against theory solver If theory solver determines unsat improve your boolean abstraction Repeat until either theory solver agrees or boolean abstraction becomes unsat Theory Solver Handles Theories Theory Solver 1 SAT Solver Handles Boolean Structure Theory Solver 2

  41. Complex boolean structure Example: ? > ? ? > 0 ? 0 Equivalent to ?????( (? > ? ? > 0 ? 0) )

Related


No related presentations.

More Related Content