The Algorithm: Reachability in the Implication Graph, One Variable at a Time
Lax117284.TwoSatAlgorithm · concepts/Lax117284/TwoSatAlgorithm.lean · lax-117284
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
The algorithm decides a formula in three steps. It rejects if some clause is empty or has more than two literals. It builds the implication graph on the literals whose variable index is below one more than the largest index that occurs. Then, for each variable that occurs, it computes the set of literals reachable from by a breadth-first search and, if is among them, the set reachable from ; it rejects if is among those. If no variable is rejected the formula is accepted.
Concept map
Lean source view on GitHub
| 1 | import Lax117284.TwoSatImplicationGraph |
| 2 | import Mathlib.Data.Finset.Prod |
| 3 | import Mathlib.Data.Finset.Union |
| 4 | import Mathlib.Data.Fintype.Basic |
| 5 | import Mathlib.Logic.Function.Iterate |
| 6 | |
| 7 | /-! |
| 8 | --- |
| 9 | title: The Algorithm: Reachability in the Implication Graph, One Variable at a Time |
| 10 | type: definition |
| 11 | --- |
| 12 | The algorithm decides a formula in three steps. It rejects if some clause is empty or has more |
| 13 | than two literals. It builds the implication graph on the literals whose variable index is below |
| 14 | one more than the largest index that occurs. Then, for each variable that occurs, it |
| 15 | computes the set of literals reachable from by a breadth-first search and, if is |
| 16 | among them, the set reachable from ; it rejects if is among those. If no variable is |
| 17 | rejected the formula is accepted. |
| 18 | |
| 19 | # Formalization Notes |
| 20 | |
| 21 | The breadth-first search is written as what it computes: starting from the singleton of the |
| 22 | source, add the successors of every literal in the current set, and repeat as many times as |
| 23 | there are literals in the graph. Every literal at distance from the source is in the set |
| 24 | after rounds, and no round adds anything not reachable, so the final set is exactly the set |
| 25 | of reachable literals. The machine program computes the same set with a queue, visiting every |
| 26 | literal at most once, which is what makes a search cost linear in the size of the graph. |
| 27 | |
| 28 | The nodes of the graph are the literals with index below `indexBound`, and the successors of a |
| 29 | literal are its out-neighbours among them. Reachability from a literal that occurs never |
| 30 | leaves the nodes, since every edge joins two literals of one clause, so the restriction loses |
| 31 | nothing; it is there so that the sets are finite and the search terminates. |
| 32 | |
| 33 | The decision is a Boolean, computed by Boolean operations over lists and finite sets, so |
| 34 | `decide F` is a definition that Lean can evaluate; it is the specification the machine program |
| 35 | is proved to implement. The result is stated as a function of the formula; on the machine it is |
| 36 | a function of the word, through the decoder of `lax-429075`. |
| 37 | -/ |
| 38 | |
| 39 | namespace Lax117284.TwoSatAlgorithm |
| 40 | |
| 41 | open Lax429075.CNF Lax117284.TwoSatCNF Lax117284.TwoSatImplicationGraph |
| 42 | |
| 43 | /-- One more than the largest variable index occurring in `F`, and `0` for no literal. -/ |
| 44 | def indexBound (F : Formula) : ℕ := (literals F).foldr (fun l n => max (l.index + 1) n) 0 |
| 45 | |
| 46 | /-- The nodes of the graph the algorithm searches: the literals with index below the bound. -/ |
| 47 | def nodes (F : Formula) : Finset Literal := |
| 48 | (Finset.range (indexBound F) ×ˢ (Finset.univ : Finset Bool)).image fun p => ⟨p.1, p.2⟩ |
| 49 | |
| 50 | instance (F : Formula) : DecidableRel (Implies F) := by |
| 51 | unfold Implies; infer_instance |
| 52 | |
| 53 | /-- The successors of a literal among the nodes. -/ |
| 54 | def successors (F : Formula) (a : Literal) : Finset Literal := |
| 55 | (nodes F).filter fun b => Implies F a b |
| 56 | |
| 57 | /-- One round of the search: add the successors of every literal in the set. -/ |
| 58 | def expand (F : Formula) (S : Finset Literal) : Finset Literal := S ∪ S.biUnion (successors F) |
| 59 | |
| 60 | /-- **The literals reachable from `s`**: the set the breadth-first search from `s` marks, here |
| 61 | as the result of as many rounds of expansion as there are nodes. -/ |
| 62 | def reachable (F : Formula) (s : Literal) : Finset Literal := (expand F)^[(nodes F).card] {s} |
| 63 | |
| 64 | /-- Every clause has one or two literals. -/ |
| 65 | def widthOk (F : Formula) : Bool := F.all fun C => 1 ≤ C.length && C.length ≤ 2 |
| 66 | |
| 67 | /-- The variable `x` is found contradictory: its negation is reachable from it, and it from its |
| 68 | negation. -/ |
| 69 | def contradictory (F : Formula) (x : ℕ) : Bool := |
| 70 | neg x ∈ reachable F (pos x) && pos x ∈ reachable F (neg x) |
| 71 | |
| 72 | /-- **The algorithm.** Reject unless every clause has one or two literals; then reject exactly |
| 73 | when some occurring variable is contradictory. -/ |
| 74 | def decide (F : Formula) : Bool := |
| 75 | widthOk F && ((literals F).map Literal.index).dedup.all fun x => !contradictory F x |
| 76 | |
| 77 | end Lax117284.TwoSatAlgorithm |
| 78 |
Formalization Notes
The breadth-first search is written as what it computes: starting from the singleton of the source, add the successors of every literal in the current set, and repeat as many times as there are literals in the graph. Every literal at distance from the source is in the set after rounds, and no round adds anything not reachable, so the final set is exactly the set of reachable literals. The machine program computes the same set with a queue, visiting every literal at most once, which is what makes a search cost linear in the size of the graph.
The nodes of the graph are the literals with index below , and the successors of a literal are its out-neighbours among them. Reachability from a literal that occurs never leaves the nodes, since every edge joins two literals of one clause, so the restriction loses nothing; it is there so that the sets are finite and the search terminates.
The decision is a Boolean, computed by Boolean operations over lists and finite sets, so is a definition that Lean can evaluate; it is the specification the machine program is proved to implement. The result is stated as a function of the formula; on the machine it is a function of the word, through the decoder of .
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments