Understanding Satisfiability Modulo Theories: Lecture Insights
Variables, terms, signatures, and formulas explained in first-order logic. Explore models, interpretations, and satisfiability modulo theories (SMT). Discover common theories like EUF, LIA, LRA, and decision procedures for EUF.
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. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Satisfiability Modulo Theories Lecture 3(b) Sriram Rajamani (some parts adapted from notes/slides by Leo DeMoura and Emina Torlak)
Terms: Variables and constants are terms If function symbol ? has arity n, then ?(?1,?2, ,??) is a term if ?1,?2, ,?? are terms First Order Logic Signature: A signature is a finite set of: 1. Function symbols ?,?, , 2. Predicate symbols ?,?,?, 3. An arity function which maps function and predicate symbols to integers [Function symbols with 0 arity are constants ] Atomic Formulas: If predicate symbol ? has arity n, then ?(?1,?2, ,??) is an atomic formula if ?1,?2, ,?? are terms We assume that = is a binary predicate Quantifier Free Formulas (QFF): Evert atomic formula is a QFF If ? is a QFF then ? is QFF If ?1,?2are QFFs, then ?1 ?2, ?1 ?2, ?1 ?2,?1 ?2 are QFFs Variables: We also assume a finite set ? of variables ?,?, disjoint from First Order Logic Formulas (FOLF): The set of FOLFs is the closure of QFFs under existential and universal quantification of variables. Free variables are variables not bound by quantifiers A FOLF without free variables is called a sentence
Models and interpretations A model ? is a set of elements (could be infinite), a set of functions over the elements, and predicates over the elements For example, the set of integers with functions +, , ,.. and predicates such as <,>, , ,???????(),??????(),?????() is a model Given a model ? and a formula ?, an interpretation ? maps: Every free variable ? of ? to an element of ? Every function symbol of ? to a function of M with matching arity Every predicate symbol of ? to a predicate of M with matching arity Unsatisfiable Valid We say that ? is satisfiable if there is a model ? and interpretation ? such that ?,? ?
Satisfiability Modulo Theories (SMT) A first order theory ?over a signature and a set of variables ? is a set of deductively closed sentences (over and?) The sentences of ? can usually be specified succinctly using a set of axioms (which generates the sentences using deductive closure) A theory ?is consistent if ????? ? A first order theory ? can also be viewed as the set of all models of ? (due to completeness of first order logic). These models are called ?-models. A formula ? is satisfiable modulo ? if ? ?, for some ?-model ? A formula ? is valid modulo ? if ? ?, for all ?-models ?
Common Theories 1. EUF: Equality with uninterpreted functions E.g. ? = ? ? , ? ? ? 2. LIA: Linear Integer Arithmetic E.g. ? 5 ? + ? > ? 3. LRA: Linear Real Arithmetic E.g. ? 5 ? + ? > ? 4. Difference Logic (sub-fragment of linear arithmetic) E.g. ? ? ? 5. Theory of Arrays E.g. ???? ????? ?,?,4 ,? = 4 6. Theory of fixed-width Bitvectors E.g. ? 5 = ? ? ? ,
Decision procedure for EUF First let us consider only equalities and disequalities (add uninterpreted functions later) Idea: Maintain equivalence classes of variables Merge equivalence classes related by equalities Maintain disequalities between equivalence classes
Decision procedure for EUF First let us consider only equalities and disequalities (add uninterpreted functions later) ? = ?, ? = ?, ? = ?, ? ?, ? = ?, ? ? ? = ?, Idea: Maintain equivalence classes of variables Merge equivalence classes related by equalities UNSAT if disequalty is in the same clas
Decision procedure for EUF First let us consider only equalities and disequalities (add uninterpreted functions later) ? = ?, ? = ?, ? = ?, ? ?, ? = ?, ? ? ? = ?, Idea: Maintain equivalence classes of variables Merge equivalence classes related by equalities UNSAT if disequalty is in the same clas
Decision procedure for EUF First let us consider only equalities and disequalities (add uninterpreted functions later) ? = ?, ? = ?, ? = ?, ? ?, ? = ?, ? ? ? = ?, Idea: Maintain equivalence classes of variables Merge equivalence classes related by equalities UNSAT if disequalty is in the same clas
Decision procedure for EUF First let us consider only equalities and disequalities (add uninterpreted functions later) ? = ?, ? = ?, ? = ?, ? ?, ? = ?, ? ? ? = ?, Idea: Maintain equivalence classes of variables Merge equivalence classes related by equalities UNSAT if disequality is in the same class
Decision procedure for full EUF Idea: Maintain equivalence classes of variables Merge equivalence classes related by equalities Propagate congruences implied by merging UNSAT if disequality is in the same class ? ?,? = ? ? ? ?,? ,? ?
Decision procedure for full EUF Idea: Maintain equivalence classes of variables Merge equivalence classes related by equalities Propagate congruences implied by merging UNSAT if disequality is in the same class ? ?,? = ? ? ? ?,? ,? ?
Decision procedure for full EUF Idea: Maintain equivalence classes of variables Merge equivalence classes related by equalities Propagate congruences implied by merging UNSAT if disequality is in the same class ? ?,? = ? ? ? ?,? ,? ?
Decision procedure for full EUF Idea: Maintain equivalence classes of variables Merge equivalence classes related by equalities Propagate congruences implied by merging UNSAT if disequality is in the same class ? ?,? = ? ? ? ?,? ,? ?
Decision procedure for full EUF Idea: Maintain equivalence classes of variables Merge equivalence classes related by equalities Propagate congruences implied by merging UNSAT if disequality is in the same class ? ?,? = ? ? ? ?,? ,? ? Can be implemented in almost-linear-time using union-find trees
Homework Work out the decision procedure for EUF on this example. Is the formula below satisfiable in the theory of EUF? ? = ?, ? = ?,? = ?,? = ?,? = ?,?(?,?(?)) ?(?,?(?))
Decision Procedure for Difference logic Signature Domain: { ,-2, -1, 0, 1, 2, .} Functions: +, -, Relations =, >, <, Formulas Conjunctions of the form ? ? ? ? ? 0 ? ? 0 ? ? 0 ? ? 5 ? ? 2 ? ? 3 ? ? 2 Idea: Construct a graph with variables in formula as nodes For every conjunct ? ? ?, add an edge from ? to ? with weight ? Formula is UNSAT iff there are negative weighted loops
Decision Procedure for Difference logic Signature Domain: { ,-2, -1, 0, 1, 2, .} Functions: +, -, Relations =, >, <, Formulas Conjunctions of the form ? ? ? ? ? 0 ? ? 0 ? ? 0 ? ? 5 ? ? 2 ? ? 3 ? ? 2 Idea: Construct a graph with variables in formula as nodes For every conjunct ? ? ?, add an edge from ? to ? with weight ? Formula is UNSAT iff there are negative weighted loops
Decision Procedure for Difference logic Can be implemented in O(mn) time using Bellman-Ford algorithm Signature Domain: { ,-2, -1, 0, 1, 2, .} Functions: +, -, Relations =, >, <, Formulas Conjunctions of the form ? ? ? ? ? 0 ? ? 0 ? ? 0 ? ? 5 ? ? 2 ? ? 3 ? ? 2 Idea: Construct a graph with variables in formula as nodes For every conjunct ? ? ?, add an edge from ? to ? with weight ? Formula is UNSAT iff there are negative weighted loops
Decision procedures for LIA and LRA LRA Many solvers implement variants of simplex or Fouier-Motzkin methods in spite of worst-case exponential complexity. Domain: Reals Functions: +, -, Relations =, >, <, LIA Solutions include branch and bound (extension of Simplex), Omega test(extension of Fourier-Motzkin), or using small domain encodings followed by SAT Domain: { ,-2, -1, 0, 1, 2, .} Functions: +, -, Relations =, >, <,
Next time How do wereason about conjunctions which involve formulas from multiple theories?(Nelson-Oppen Method) How to reason about disjunctions? (use SAT solvers together with theory solvers) How to reason about quantifiers, which are needed to solve synthesis problems? (CEGIS..)
