# 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

• 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.
inductive Sat.Literal :
• pos:
• neg:

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.

Instances For

Swap the polarity of a literal.

Instances For

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

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

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

Instances For

A single clause as a formula.

Instances For

A conjunction of formulas.

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_left (f : Sat.Fmla) (f₁ : Sat.Fmla) (f₂ : Sat.Fmla) (H : Sat.Fmla.subsumes f (Sat.Fmla.and f₁ f₂)) :
theorem Sat.Fmla.subsumes_right (f : Sat.Fmla) (f₁ : Sat.Fmla) (f₂ : Sat.Fmla) (H : Sat.Fmla.subsumes f (Sat.Fmla.and f₁ f₂)) :

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

Instances For

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

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

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

Instances For
theorem Sat.Fmla.proof_of_subsumes {f : Sat.Fmla} {c : Sat.Clause} (H : ) :

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

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

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
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 : } {ps : } (as₁ : ) :
as = List.reverseAux as₁ psSat.Valuation.implies () p ps (List.length as₁)p

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) :
• prop :

Asserts that ¬⟦f⟧_v implies p.

Instances For
theorem Sat.Fmla.refute {p : Prop} {ps : } (f : Sat.Fmla) (hf : ) (hv : ∀ (v : Sat.Valuation), Sat.Valuation.implies v () 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 (Sat.Fmla.and f₁ 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) :
• prop : p

Asserts that ¬⟦c⟧_v implies p.

Instances For
theorem Sat.Fmla.reify_one {v : Sat.Valuation} {c : Sat.Clause} {a : Prop} (h : ) :

Reification of a single clause formula.

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

Asserts that ¬⟦l⟧_v implies p.

Instances For
theorem Sat.Clause.reify_and {v : Sat.Valuation} {l : Sat.Literal} {a : Prop} {c : Sat.Clause} {b : Prop} (h₁ : ) (h₂ : ) :

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

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

theorem Sat.Clause.reify_one {v : Sat.Valuation} {l : Sat.Literal} {a : Prop} (h₁ : ) :

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.

• lits :

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.

The representation of a global clause.

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

Instances For
partial def Mathlib.Tactic.Sat.buildConj (arr : Array ()) (start : ) (stop : ) :

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

partial def Mathlib.Tactic.Sat.buildClauses (arr : Array ()) (ctx : Lean.Expr) (start : ) (stop : ) (f : Lean.Expr) (p : Lean.Expr) (accum : ) :

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.

• lits :

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

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

Instances For
def Mathlib.Tactic.Sat.buildProofStep (ns : ) (pf : ) (ctx : Lean.Expr) (clause : Lean.Expr) :

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.
Instances For

An addition step, with the clause ID, the clause literal list, and the proof trace

• del:

A (multiple) deletion step, which deletes all the listed clause IDs from the context

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

Instances For
def Mathlib.Tactic.Sat.buildProof (arr : Array ()) (ctx : Lean.Expr) (ctx' : Lean.Expr) (steps : ) :

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
Instances For
def Mathlib.Tactic.Sat.buildReify (ctx : Lean.Expr) (ctx' : Lean.Expr) (proof : Lean.Expr) (nvars : ) :

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.
Instances For
partial def Mathlib.Tactic.Sat.buildReify.mkPS (cons : Lean.Expr) (depth : ) (e : Lean.Expr) :

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

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

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

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

Instances For

Parse a natural number

Instances For

Parse an integer

Instances For
partial def Mathlib.Tactic.Sat.Parser.parseInts (arr : optParam () #[]) :

Parse a list of integers terminated by 0

partial def Mathlib.Tactic.Sat.Parser.parseNats (arr : optParam () #[]) :

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.

Instances For

Parse an LRAT file into a list of steps.

Instances For
def Mathlib.Tactic.Sat.fromLRATAux (cnf : String) (lrat : String) (name : Lean.Name) :

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 []
Instances For
def Mathlib.Tactic.Sat.fromLRAT (cnf : String) (lrat : String) (name : Lean.Name) :

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.

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.
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.
Instances For