Documentation

Mathlib.Tactic.Sat.FromLRAT

lrat_proof command #

Defines a macro for producing SAT proofs from CNF / LRAT files. These files are commonly used in the SAT community for writing proofs.

Most SAT solvers support export to DRAT format, but this format can be expensive to reconstruct because it requires recomputing all unit propagation steps. The LRAT format solves this issue by attaching a proof to the deduction of each new clause. (The L in LRAT stands for Linear time verification.) There are several verified checkers for the LRAT format, and the program implemented here makes it possible to use the lean kernel as an LRAT checker as well and expose the results as a standard propositional theorem.

The input to the lrat_proof command is the name of the theorem to define, and the statement (written in CNF format) and the proof (in LRAT format). For example:

lrat_proof foo
  "p cnf 2 4  1 2 0  -1 2 0  1 -2 0  -1 -2 0"
  "5 -2 0 4 3 0  5 d 3 4 0  6 1 0 5 1 0  6 d 1 0  7 0 5 2 6 0"

produces a theorem:

foo : ∀ (a a_1 : Prop), (¬a ∧ ¬a_1 ∨ a ∧ ¬a_1) ∨ ¬a ∧ a_1 ∨ a ∧ a_1
inductive Sat.Literal :

A literal is a positive or negative occurrence of an atomic propositional variable. Note that unlike DIMACS, 0 is a valid variable index.

Instances For

    Construct a literal. Positive numbers are translated to positive literals, and negative numbers become negative literals. The input is assumed to be nonzero.

    Equations
    Instances For

      Swap the polarity of a literal.

      Equations
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.

        A clause is a list of literals, thought of as a disjunction like a ∨ b ∨ ¬c.

        Equations
        Instances For
          Equations
          Instances For
            Equations
            Instances For
              @[reducible, inline]
              abbrev Sat.Fmla :

              A formula is a list of clauses, thought of as a conjunction like (a ∨ b) ∧ c ∧ (¬c ∨ ¬d).

              Equations
              Instances For

                A single clause as a formula.

                Equations
                Instances For

                  A conjunction of formulas.

                  Equations
                  • a.and b = a ++ b
                  Instances For
                    structure Sat.Fmla.subsumes (f : Sat.Fmla) (f' : Sat.Fmla) :

                    Formula f subsumes f' if all the clauses in f' are in f. We use this to prove that all clauses in the formula are subsumed by it.

                    Instances For
                      theorem Sat.Fmla.subsumes.prop {f : Sat.Fmla} {f' : Sat.Fmla} (self : f.subsumes f') (x : Sat.Clause) :
                      x f'x f
                      theorem Sat.Fmla.subsumes_self (f : Sat.Fmla) :
                      f.subsumes f
                      theorem Sat.Fmla.subsumes_left (f : Sat.Fmla) (f₁ : Sat.Fmla) (f₂ : Sat.Fmla) (H : f.subsumes (f₁.and f₂)) :
                      f.subsumes f₁
                      theorem Sat.Fmla.subsumes_right (f : Sat.Fmla) (f₁ : Sat.Fmla) (f₂ : Sat.Fmla) (H : f.subsumes (f₁.and f₂)) :
                      f.subsumes f₂

                      A valuation is an assignment of values to all the propositional variables.

                      Equations
                      Instances For

                        v.neg lit asserts that literal lit is falsified in the valuation.

                        Equations
                        Instances For

                          v.satisfies c asserts that clause c satisfied by the valuation. It is written in a negative way: A clause like a ∨ ¬b ∨ c is rewritten as ¬a → b → ¬c → False, so we are asserting that it is not the case that all literals in the clause are falsified.

                          Equations
                          • v.satisfies [] = False
                          • v.satisfies (l :: c) = (v.neg lv.satisfies c)
                          Instances For

                            v.satisfies_fmla f asserts that formula f is satisfied by the valuation. A formula is satisfied if all clauses in it are satisfied.

                            Instances For
                              theorem Sat.Valuation.satisfies_fmla.prop {v : Sat.Valuation} {f : Sat.Fmla} (self : v.satisfies_fmla f) (c : Sat.Clause) :
                              c fv.satisfies c

                              f.proof c asserts that c is derivable from f.

                              Equations
                              • f.proof c = ∀ (v : Sat.Valuation), v.satisfies_fmla fv.satisfies c
                              Instances For
                                theorem Sat.Fmla.proof_of_subsumes {f : Sat.Fmla} {c : Sat.Clause} (H : f.subsumes (Sat.Fmla.one c)) :
                                f.proof c

                                If f subsumes c (i.e. c ∈ f), then f.proof c.

                                theorem Sat.Valuation.by_cases {v : Sat.Valuation} {l : Sat.Literal} (h₁ : v.neg l.negateFalse) (h₂ : v.neg lFalse) :

                                The core unit-propagation step.

                                We have a local context of assumptions ¬l' (sometimes called an assignment) and we wish to add ¬l to the context, that is, we want to prove l is also falsified. This is because there is a clause a ∨ b ∨ ¬l in the global context such that all literals in the clause are falsified except for ¬l; so in the context h₁ where we suppose that ¬l is falsified, the clause itself is falsified so we can prove False. We continue the proof in h₂, with the assumption that l is falsified.

                                v.implies p [a, b, c] 0 definitionally unfolds to (v 0 ↔ a) → (v 1 ↔ b) → (v 2 ↔ c) → p. This is used to introduce assumptions about the first n values of v during reification.

                                Equations
                                • v.implies p [] x = p
                                • v.implies p (a :: as) x = ((v x a)v.implies p as (x + 1))
                                Instances For

                                  Valuation.mk [a, b, c] is a valuation which is a at 0, b at 1 and c at 2, and false everywhere else.

                                  Equations
                                  Instances For
                                    theorem Sat.Valuation.mk_implies {p : Prop} {as : List Prop} {ps : List Prop} (as₁ : List Prop) :
                                    as = as₁.reverseAux ps(Sat.Valuation.mk as).implies p ps as₁.lengthp

                                    The fundamental relationship between mk and implies: (mk ps).implies p ps 0 is equivalent to p.

                                    structure Sat.Fmla.reify (v : Sat.Valuation) (f : Sat.Fmla) (p : Prop) :

                                    Asserts that ¬⟦f⟧_v implies p.

                                    • prop : ¬v.satisfies_fmla fp
                                    Instances For
                                      theorem Sat.Fmla.reify.prop {v : Sat.Valuation} {f : Sat.Fmla} {p : Prop} (self : Sat.Fmla.reify v f p) :
                                      ¬v.satisfies_fmla fp
                                      theorem Sat.Fmla.refute {p : Prop} {ps : List Prop} (f : Sat.Fmla) (hf : f.proof []) (hv : ∀ (v : Sat.Valuation), v.implies (Sat.Fmla.reify v f p) ps 0) :
                                      p

                                      If f is unsatisfiable, and every v which agrees with ps implies ¬⟦f⟧_v → p, then p. Equivalently, there exists a valuation v which agrees with ps, and every such valuation yields ¬⟦f⟧_v because f is unsatisfiable.

                                      theorem Sat.Fmla.reify_or {v : Sat.Valuation} {f₁ : Sat.Fmla} {a : Prop} {f₂ : Sat.Fmla} {b : Prop} (h₁ : Sat.Fmla.reify v f₁ a) (h₂ : Sat.Fmla.reify v f₂ b) :
                                      Sat.Fmla.reify v (f₁.and f₂) (a b)

                                      Negation turns AND into OR, so ¬⟦f₁ ∧ f₂⟧_v ≡ ¬⟦f₁⟧_v ∨ ¬⟦f₂⟧_v.

                                      structure Sat.Clause.reify (v : Sat.Valuation) (c : Sat.Clause) (p : Prop) :

                                      Asserts that ¬⟦c⟧_v implies p.

                                      • prop : ¬v.satisfies cp
                                      Instances For
                                        theorem Sat.Clause.reify.prop {v : Sat.Valuation} {c : Sat.Clause} {p : Prop} (self : Sat.Clause.reify v c p) :
                                        ¬v.satisfies cp

                                        Reification of a single clause formula.

                                        structure Sat.Literal.reify (v : Sat.Valuation) (l : Sat.Literal) (p : Prop) :

                                        Asserts that ¬⟦l⟧_v implies p.

                                        • prop : v.neg lp
                                        Instances For
                                          theorem Sat.Literal.reify.prop {v : Sat.Valuation} {l : Sat.Literal} {p : Prop} (self : Sat.Literal.reify v l p) :
                                          v.neg lp
                                          theorem Sat.Clause.reify_and {v : Sat.Valuation} {l : Sat.Literal} {a : Prop} {c : Sat.Clause} {b : Prop} (h₁ : Sat.Literal.reify v l a) (h₂ : Sat.Clause.reify v c b) :

                                          Negation turns OR into AND, so ¬⟦l ∨ c⟧_v ≡ ¬⟦l⟧_v ∧ ¬⟦c⟧_v.

                                          The reification of the empty clause is True: ¬⟦⊥⟧_v ≡ True.

                                          The reification of a singleton clause ¬⟦l⟧_v ≡ ¬⟦l⟧_v.

                                          theorem Sat.Literal.reify_pos {v : Sat.Valuation} {a : Prop} {n : } (h : v n a) :

                                          The reification of a positive literal ¬⟦a⟧_v ≡ ¬a.

                                          theorem Sat.Literal.reify_neg {v : Sat.Valuation} {a : Prop} {n : } (h : v n a) :

                                          The reification of a negative literal ¬⟦¬a⟧_v ≡ a.

                                          The representation of a global clause.

                                          • lits : Array

                                            The list of literals as read from the input file

                                          • expr : Lean.Expr

                                            The clause expression of type Clause

                                          • proof : Lean.Expr

                                            A proof of ⊢ ctx.proof c. Note that we do not use have statements to cache these proofs: this is literally the proof expression itself. As a result, the proof terms rely heavily on dag-like sharing of the expression, and printing these proof terms directly is likely to crash lean for larger examples.

                                          Instances For

                                            Construct the clause expression from the input list. For example [1, -2] is translated to Clause.cons (Literal.pos 1) (Clause.cons (Literal.neg 2) Clause.nil).

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              partial def Mathlib.Tactic.Sat.buildConj (arr : Array (Array )) (start : ) (stop : ) :

                                              Constructs the formula expression from the input CNF, as a balanced tree of Fmla.and nodes.

                                              Constructs the proofs of ⊢ ctx.proof c for each clause c in ctx. The proofs are stashed in a HashMap keyed on the clause ID.

                                              A localized clause reference. It is the same as Clause except that the proof is now a local variable.

                                              • lits : Array

                                                The list of literals as read from the input file

                                              • expr : Lean.Expr

                                                The clause expression of type Clause

                                              • depth :

                                                The bound variable index of the hypothesis asserting ⊢ ctx.proof c, counting from the outside and 1-based. (We use this numbering because we will need to reference the variable from multiple binder depths.)

                                              Instances For

                                                Construct an individual proof step ⊢ ctx.proof c.

                                                • db: the current global context
                                                • ns, clause: the new clause
                                                • pf: the LRAT proof trace
                                                • ctx: the main formula

                                                The proof has three steps:

                                                1. Introduce local assumptions have h1 : ctx.proof c1 := p1 for each clause c1 referenced in the proof. We actually do all the introductions at once, as in (fun h1 h2 h3 ↦ ...) p1 p2 p3, because we want p_i to not be under any binders to avoid the cost of instantiate during typechecking and get the benefits of dag-like sharing in the pi (which are themselves previous proof steps which may be large terms). The hypotheses are in gctx, keyed on the clause ID.

                                                2. Unfold ⊢ ctx.proof [a, b, c] to ∀ v, v.satisfies_fmla ctx → v.neg a → v.neg b → v.neg c → False and intro v hv ha hb hc, storing each ha : v.neg a in lctx, keyed on the literal a.

                                                3. For each LRAT step hc : ctx.proof [x, y], hc v hv : v.neg x → v.neg y → False. We look for a literal that is not falsified in the clause. Since it is a unit propagation step, there can be at most one such literal.

                                                  • If x is the non-falsified clause, let x' denote the negated literal of x. Then x'.negate reduces to x, so hnx : v.neg x'.negate |- hc v hv hnx hy : False, so we construct the term by_cases (fun hnx : v.neg x'.negate ↦ hc v hv hnx hy) (fun hx : v.neg x ↦ ...) and hx is added to the local context.
                                                  • If all clauses are falsified, then we are done: hc v hv hx hy : False.
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For

                                                  An LRAT step is either an addition or a deletion step.

                                                  Instances For

                                                    Build the main proof of ⊢ ctx.proof [] using the LRAT proof trace.

                                                    • arr: The input CNF
                                                    • ctx: The abbreviated formula, a constant like foo.ctx_1
                                                    • ctx': The definitional expansion of the formula, a tree of Fmla.and nodes
                                                    • steps: The input LRAT proof trace
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For

                                                      Build the type and value of the reified theorem. This rewrites all the SAT definitions into standard operators on Prop, for example if the formula is [[1, 2], [-1, 2], [-2]] then this produces a proof of ⊢ ∀ a b : Prop, (a ∧ b) ∨ (¬a ∧ b) ∨ ¬b. We use the input nvars to decide how many quantifiers to use.

                                                      Most of the proof is under 2 * nvars + 1 quantifiers a1 .. an : Prop, v : Valuation, h1 : v 0 ↔ a1, ... hn : v (n-1) ↔ an ⊢ ..., and we do the index arithmetic by hand.

                                                      1. First, we call reifyFormula ctx' which returns a and pr : reify v ctx' a
                                                      2. Then we build fun (v : Valuation) (h1 : v 0 ↔ a1) ... (hn : v (n-1) ↔ an) ↦ pr
                                                      3. We have to lower expression a from step 1 out of the quantifiers by lowering all variable indices by nvars+1. This is okay because v and h1..hn do not appear in a.
                                                      4. We construct the expression ps, which is a1 .. an : Prop ⊢ [a1, ..., an] : List Prop
                                                      5. refute ctx (hf : ctx.proof []) (fun v h1 .. hn ↦ pr) : a forces some definitional unfolding since fun h1 .. hn ↦ pr should have type implies v (reify v ctx a) [a1, ..., an] a, which involves unfolding implies n times as well as ctx ↦ ctx'.
                                                      6. Finally, we intro a1 ... an so that we have a proof of ∀ a1 ... an, a.
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For

                                                        The v variable under the a1 ... an, v, h1 ... hn context

                                                        Equations
                                                        Instances For

                                                          Returns a and pr : reify v f a given a formula f

                                                          Returns a and pr : reify v c a given a clause c

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For

                                                            Returns a and pr : reify v c a given a nonempty clause c

                                                            Returns a and pr : reify v l a given a literal c

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For

                                                              Returns a and pr : v n ↔ a given a variable index n. These are both lookups into the context (a0 .. a(n-1) : Prop) (v) (h1 : v 0 ↔ a0) ... (hn : v (n-1) ↔ a(n-1)).

                                                              Equations
                                                              Instances For

                                                                Parse an integer

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For

                                                                  Parse a list of integers terminated by 0

                                                                  Parse a list of natural numbers terminated by 0

                                                                  Parse a DIMACS format .cnf file. This is not very robust; we assume the file has had comments stripped.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For

                                                                    Parse an LRAT file into a list of steps.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For

                                                                      Core of fromLRAT. Constructs the context and main proof definitions, but not the reification theorem. Returns:

                                                                      • nvars: the number of variables specified in the CNF file
                                                                      • ctx: The abbreviated formula, a constant like foo.ctx_1
                                                                      • ctx': The definitional expansion of the formula, a tree of Fmla.and nodes
                                                                      • proof: A proof of ctx.proof []
                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For

                                                                        Main entry point. Given strings cnf and lrat with unparsed file data, and a name name, adds theorem name : type := proof where type is a propositional theorem like ∀ (a a_1 : Prop), (¬a ∧ ¬a_1 ∨ a ∧ ¬a_1) ∨ ¬a ∧ a_1 ∨ a ∧ a_1.

                                                                        Also creates auxiliaries named name.ctx_1 (for the CNF formula) and name.proof_1 (for the LRAT proof), with name itself containing the reification proof.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For

                                                                          A macro for producing SAT proofs from CNF / LRAT files. These files are commonly used in the SAT community for writing proofs.

                                                                          The input to the lrat_proof command is the name of the theorem to define, and the statement (written in CNF format) and the proof (in LRAT format). For example:

                                                                          lrat_proof foo
                                                                            "p cnf 2 4  1 2 0  -1 2 0  1 -2 0  -1 -2 0"
                                                                            "5 -2 0 4 3 0  5 d 3 4 0  6 1 0 5 1 0  6 d 1 0  7 0 5 2 6 0"
                                                                          

                                                                          produces a theorem:

                                                                          foo : ∀ (a a_1 : Prop), (¬a ∧ ¬a_1 ∨ a ∧ ¬a_1) ∨ ¬a ∧ a_1 ∨ a ∧ a_1
                                                                          
                                                                          • You can see the theorem statement by hovering over the word foo.
                                                                          • You can use the example keyword in place of foo to avoid generating a theorem.
                                                                          • You can use the include_str macro in place of the two strings to load CNF / LRAT files from disk.
                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For

                                                                            A macro for producing SAT proofs from CNF / LRAT files. These files are commonly used in the SAT community for writing proofs.

                                                                            The input to the from_lrat term syntax is two string expressions with the statement (written in CNF format) and the proof (in LRAT format). For example:

                                                                            def foo := from_lrat
                                                                              "p cnf 2 4  1 2 0  -1 2 0  1 -2 0  -1 -2 0"
                                                                              "5 -2 0 4 3 0  5 d 3 4 0  6 1 0 5 1 0  6 d 1 0  7 0 5 2 6 0"
                                                                            

                                                                            produces a theorem:

                                                                            foo : ∀ (a a_1 : Prop), (¬a ∧ ¬a_1 ∨ a ∧ ¬a_1) ∨ ¬a ∧ a_1 ∨ a ∧ a_1
                                                                            
                                                                            • You can use this term after have := or in def foo := to produce the term without constraining the type.
                                                                            • You can use it when a specific type is expected, but it currently does not pay any attention to the shape of the goal and always produces the same theorem, so you can only use this to do alpha renaming.
                                                                            • You can use the include_str macro in place of the two strings to load CNF / LRAT files from disk.
                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For