Two-Satisfiability
Lax117284.TwoSatisfiability · concepts/Lax117284/TwoSatisfiability.lean · lax-117284
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A 2-CNF formula over variables is a finite conjunction of clauses, each clause a disjunction of two literals, a literal being a variable or a negated variable. The formula is satisfiable if some assignment of truth values to the variables makes at least one literal of every clause true. The language 2-SAT consists of the encodings of the satisfiable 2-CNF formulas; it is decidable in linear time.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax117284.Problems |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Two-Satisfiability |
| 6 | type: definition |
| 7 | --- |
| 8 | A *2-CNF formula* over variables is a finite conjunction of clauses, each clause a |
| 9 | disjunction of two literals, a literal being a variable or a negated variable. The formula |
| 10 | is *satisfiable* if some assignment of truth values to the variables makes at least one |
| 11 | literal of every clause true. The language 2-SAT consists of the encodings of the |
| 12 | satisfiable 2-CNF formulas; it is decidable in linear time. |
| 13 | |
| 14 | # Formalization Notes |
| 15 | |
| 16 | A clause is a pair of literals and not a set of at most two of them. The distinction is the |
| 17 | one that matters here: what breaks the tractability of 2-SAT is a clause with three |
| 18 | literals, so the width has to be part of the definition rather than a side condition. A |
| 19 | clause repeating its literal is allowed and expresses a unit clause. |
| 20 | |
| 21 | A literal is a variable together with a sign, `true` standing for the variable and `false` |
| 22 | for its negation, so that a literal holds under an assignment exactly when the assignment |
| 23 | agrees with the sign. |
| 24 | |
| 25 | The numbers of an encoded formula are written with the numeral code of the scheduling |
| 26 | languages, so that all words of this submission are read the same way. |
| 27 | -/ |
| 28 | |
| 29 | namespace Lax117284.TwoSatisfiability |
| 30 | |
| 31 | open Lax434930.PolynomialTime |
| 32 | |
| 33 | /-- A **2-CNF formula**: `clauses` clauses over `vars` variables, each clause a pair of |
| 34 | literals, a literal being a variable together with a sign. -/ |
| 35 | structure Formula where |
| 36 | /-- The number of variables. -/ |
| 37 | vars : ℕ |
| 38 | /-- The number of clauses. -/ |
| 39 | clauses : ℕ |
| 40 | /-- The two literals of each clause. -/ |
| 41 | lit : Fin clauses → Fin 2 → Fin vars × Bool |
| 42 | |
| 43 | namespace Formula |
| 44 | |
| 45 | variable (φ : Formula) |
| 46 | |
| 47 | /-- An assignment of a truth value to every variable. -/ |
| 48 | abbrev Assignment := Fin φ.vars → Bool |
| 49 | |
| 50 | /-- The assignment `a` satisfies `φ`: every clause has a literal that holds. -/ |
| 51 | def Satisfies (a : φ.Assignment) : Prop := |
| 52 | ∀ c, ∃ α, a (φ.lit c α).1 = (φ.lit c α).2 |
| 53 | |
| 54 | /-- **The question of 2-satisfiability**: is there a satisfying assignment? -/ |
| 55 | def Satisfiable : Prop := ∃ a : φ.Assignment, φ.Satisfies a |
| 56 | |
| 57 | end Formula |
| 58 | |
| 59 | /-- An unsatisfiable formula: one variable, required by one clause to be true and by |
| 60 | another to be false. It is the image a reduction into 2-SAT gives the words it must |
| 61 | reject. -/ |
| 62 | def unsatisfiable : Formula where |
| 63 | vars := 1 |
| 64 | clauses := 2 |
| 65 | lit c _ := (0, decide (c = 0)) |
| 66 | |
| 67 | /-- **The rejected formula is unsatisfiable.** -/ |
| 68 | axiom not_satisfiable_unsatisfiable : ¬ unsatisfiable.Satisfiable |
| 69 | |
| 70 | /-- A 2-CNF formula as a binary word: the number of variables, the number of clauses, and |
| 71 | then the variable and the sign of both literals of every clause. -/ |
| 72 | def encodeFormula (φ : Formula) : Word := |
| 73 | Problems.encodeNat φ.vars ++ Problems.encodeNat φ.clauses ++ |
| 74 | (List.finRange φ.clauses).flatMap fun c => |
| 75 | (List.finRange 2).flatMap fun α => |
| 76 | Problems.encodeNat (φ.lit c α).1 ++ [(φ.lit c α).2] |
| 77 | |
| 78 | /-- **2-SAT**, as a language. -/ |
| 79 | def TwoSat : Language := {w | ∃ φ : Formula, encodeFormula φ = w ∧ φ.Satisfiable} |
| 80 | |
| 81 | /-- **2-SAT is solvable in polynomial time**, indeed in linear time. -/ |
| 82 | axiom twoSat_mem_P : TwoSat ∈ P |
| 83 | |
| 84 | end Lax117284.TwoSatisfiability |
| 85 |
Formalization Notes
A clause is a pair of literals and not a set of at most two of them. The distinction is the one that matters here: what breaks the tractability of 2-SAT is a clause with three literals, so the width has to be part of the definition rather than a side condition. A clause repeating its literal is allowed and expresses a unit clause.
A literal is a variable together with a sign, standing for the variable and for its negation, so that a literal holds under an assignment exactly when the assignment agrees with the sign.
The numbers of an encoded formula are written with the numeral code of the scheduling languages, so that all words of this submission are read the same way.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments