The Reduction from (3,4)-Satisfiability to [2,3]-Bounded 3-SAT

Lax345332.Copies · concepts/Lax345332/Copies.lean · lax-345332

proven

Loading review…

Natural Language Statement

Definition

A (3,4) formula with $C$ clauses has $3C$ literal positions; position $p = 3c + t$ holds the $t$ -th literal of clause $c$ . Let $V$ be a strict bound on its variables. The construction gives every position $p$ its own variable $x_p = v + pV$ , where $v$ is the variable at that position, and produces two kinds of clauses.

The clauses of three literals are the original clauses, with each literal replaced by the copy for its position and keeping its sign.
The clauses of two literals are the implications $x_{v,p+1} \to x_{v,p}$ , that is $(x_{v,p} \vee \neg x_{v,p+1})$ , for every variable $v < V$ and every position $p$ , with positions taken cyclically. These chain the copies of $v$ around a cycle, so they all take the same value. They are the cycle clauses of the first reduction.

Every literal of the result occurs at most twice. A copy belongs to one position only, so it appears in at most one clause of three literals, and with one sign. In the cycle of its variable it is the consequent of one implication and the antecedent of another, which gives it one positive and one negative occurrence there.

On words, the reduction is the first reduction followed by this construction: a word is sent to the encoding of a (3,4) formula, that formula is decoded, and the construction is applied to it and written in the self-delimiting code.

Concept map

11 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

This concept declares 5 statements. Each proof establishes one of them relative to its assumptions.

In the paper

page 4 of this submission's paper

Lean source view on GitHub

1	import Lax345332.TwoThreeSat
2	import Lax345332.Construction
3
4	/-!
5	---
6	title: The Reduction from (3,4)-Satisfiability to [2,3]-Bounded 3-SAT
7	type: definition
8	---
9	A (3,4) formula with $C$ clauses has $3C$ literal positions; position $p = 3c + t$ holds the
10	$t$ -th literal of clause $c$ . Let $V$ be a strict bound on its variables. The construction
11	gives every position $p$ its own variable $x_p = v + pV$ , where $v$ is the variable at that
12	position, and produces two kinds of clauses.
13
14	* The clauses of three literals are the original clauses, with each literal replaced by the
15	copy for its position and keeping its sign.
16	* The clauses of two literals are the implications $x_{v,p+1} \to x_{v,p}$ , that is
17	$(x_{v,p} \vee \neg x_{v,p+1})$ , for every variable $v < V$ and every position $p$ , with
18	positions taken cyclically. These chain the copies of $v$ around a cycle, so they all
19	take the same value. They are the cycle clauses of the first reduction.
20
21	Every literal of the result occurs at most twice. A copy belongs to one position only, so
22	it appears in at most one clause of three literals, and with one sign. In the cycle of its
23	variable it is the consequent of one implication and the antecedent of another, which gives
24	it one positive and one negative occurrence there.
25
26	On words, the reduction is the first reduction followed by this construction: a word is
27	sent to the encoding of a (3,4) formula, that formula is decoded, and the construction is
28	applied to it and written in the self-delimiting code.
29
30	# Formalization Notes
31
32	A [2,3]-bounded formula carries its occurrence bound as a field. `build` therefore returns
33	the formula only when the copies meet the bound (`Occ`) and the empty formula otherwise;
34	`build_occ` states that the bound is always met, so the second case never arises. The guard
35	is there because a definition in a concept module may not depend on that module's
36	statements.
37
38	Copies are reduced modulo the number of variables only to give them the type `Fin`; they
39	are already below it.
40
41	`build` is correct only on formulas whose clauses all have three literals (`build_sat`),
42	which is all that the first reduction produces. On words, correctness is therefore stated
43	for the composition `reduceB` and not for `toBounded` alone, which reads any word.
44	-/
45
46	namespace Lax345332.Copies
47
48	open Lax429075.CNF Lax345332.Construction Lax345332.TwoThreeSat Lax434930.PolynomialTime
49
50	-- Positions and copies
51
52	/-- The literal at position `p` of the flattened formula, and a default literal past its
53	end. -/
54	def litAt (F : Lax429075.CNF.Formula) (p : ℕ) : Literal := (F.flatMap id).getD p dflt
55
56	/-- The number of literal positions: three per clause. -/
57	def npos (F : Lax429075.CNF.Formula) : ℕ := 3 * F.length
58
59	/-- The number of variables of the result: one copy for every variable and position. -/
60	def nvars (F : Lax429075.CNF.Formula) : ℕ := bound F * npos F
61
62	/-- The copy of the variable at position `p`. -/
63	def copyVar (F : Lax429075.CNF.Formula) (p : ℕ) : ℕ := wv (bound F) (litAt F p).index p
64
65	/-- The copy that the cycle clause of `kk` mentions negatively: the same variable at the
66	next position. -/
67	def succVar (V N kk : ℕ) : ℕ := wv V (kk % V) (next N (kk / V))
68
69	/-- The bound on the variables is positive, which the `Fin` indices need. -/
70	theorem bound_pos (F : Lax429075.CNF.Formula) : 0 < bound F := by
71	induction F with
72	\| nil => exact Nat.one_pos
73	\| cons C F ih => exact lt_of_lt_of_le ih (le_max_right _ _)
74
75	-- The clauses
76
77	/-- The literals of the cycle clause `kk`: the copy `kk`, and the negation of its
78	successor. -/
79	def twoLit (F : Lax429075.CNF.Formula) (kk : Fin (nvars F)) (α : Fin 2) :
80	Fin (nvars F) × Bool :=
81	if α.val = 0 then (kk, true)
82	else (⟨succVar (bound F) (npos F) kk.val % nvars F, Nat.mod_lt _ kk.pos⟩, false)
83
84	/-- The literals of clause `c`: for `t < 3`, the copy at position `3c + t`, with the sign of
85	the original literal. -/
86	def threeLit (F : Lax429075.CNF.Formula) (c : Fin F.length) (t : Fin 3) :
87	Fin (nvars F) × Bool :=
88	(⟨copyVar F (3 * c.val + t.val) % nvars F,
89	Nat.mod_lt _ (Nat.mul_pos (bound_pos F) (Nat.mul_pos (by decide) c.pos))⟩,
90	(litAt F (3 * c.val + t.val)).positive)
91
92	/-- The occurrence condition on the construction: every literal occupies at most two
93	positions. -/
94	def Occ (F : Lax429075.CNF.Formula) : Prop :=
95	∀ l : Fin (nvars F) × Bool,
96	(Finset.univ.filter fun o : (Fin (nvars F) × Fin 2) ⊕ (Fin F.length × Fin 3) =>
97	Sum.elim (fun q => twoLit F q.1 q.2) (fun q => threeLit F q.1 q.2) o = l).card ≤ 2
98
99	instance (F : Lax429075.CNF.Formula) : Decidable (Occ F) := by unfold Occ; infer_instance
100
101	/-- The formula with no variable and no clause. -/
102	def empty : Lax345332.TwoThreeSat.Formula :=
103	⟨0, 0, 0, fun c => c.elim0, fun c => c.elim0, fun l => l.1.elim0⟩
104
105	/-- The construction. It has `V·N` variables, where `V` bounds the variables of `F` and
106	`N = 3C` is its number of positions; the `V·N` cycle clauses; and the `C` clauses of three
107	literals on the copies. It is the empty formula if the occurrence condition fails. -/
108	def build (F : Lax429075.CNF.Formula) : Lax345332.TwoThreeSat.Formula :=
109	if h : Occ F then ⟨nvars F, nvars F, F.length, twoLit F, threeLit F, h⟩ else empty
110
111	-- The reduction
112
113	/-- The construction on words: decode a formula, apply `build`, and encode the result. -/
114	def toBounded (w : Word) : Word := encodeFormula (build (parseF w))
115
116	/-- The reduction from satisfiability: the first reduction, then the construction. -/
117	def reduceB : Word → Word := toBounded ∘ reduce
118
119	/-- Every clause of the formula has exactly three literals. -/
120	def Three (F : Lax429075.CNF.Formula) : Prop := ∀ C ∈ F, C.length = 3
121
122	/-- Every literal of the construction occurs at most twice. -/
123	axiom build_occ (F : Lax429075.CNF.Formula) : Occ F
124
125	/-- The result has at most as many variables as literal positions. -/
126	axiom build_vars_le_slots (F : Lax429075.CNF.Formula) : (build F).vars ≤ slots (build F)
127
128	/-- On a formula whose clauses all have three literals, the construction is satisfiable
129	exactly when the formula is. -/
130	axiom build_sat (F : Lax429075.CNF.Formula) (h : Three F) :
131	Satisfiable F ↔ (build F).Satisfiable
132
133	/-- The reduction from satisfiability is correct on words. -/
134	axiom reduceB_correct (w : Word) :
135	w ∈ Lax429075.Satisfiability.SAT ↔ reduceB w ∈ SAT23
136
137	/-- The construction on words is computable in polynomial time. -/
138	axiom toBounded_polyTime : Nonempty (Turing.TM2ComputableInPolyTime id id toBounded)
139
140	end Lax345332.Copies
141

Show ProofShow ProofShow ProofShow ProofShow Proof

Formalization Notes

A [2,3]-bounded formula carries its occurrence bound as a field. $build$ therefore returns the formula only when the copies meet the bound ( $Occ$ ) and the empty formula otherwise; $build_occ$ states that the bound is always met, so the second case never arises. The guard is there because a definition in a concept module may not depend on that module's statements.

Copies are reduced modulo the number of variables only to give them the type $Fin$ ; they are already below it.

$build$ is correct only on formulas whose clauses all have three literals ( $build_sat$ ), which is all that the first reduction produces. On words, correctness is therefore stated for the composition $reduceB$ and not for $toBounded$ alone, which reads any word.

Builds on

Used by

none

From Mathlib

none

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

The Reduction from (3,4)-Satisfiability to [2,3]-Bounded 3-SAT

Flags

Flag this concept

Natural Language Statement

Definition

1 `build_occ` proven

2 `build_sat` proven

3 `build_vars_le_slots` proven

4 `reduceB_correct` proven

5 `toBounded_polyTime` proven

In the paper

Lean source view on GitHub

Discussion

Settings

Your comments

The Reduction from (3,4)-Satisfiability to [2,3]-Bounded 3-SAT

Natural Language Statement

Definition

1 build_occ proven

2 build_sat proven

3 build_vars_le_slots proven

4 reduceB_correct proven

5 toBounded_polyTime proven

In the paper

Lean source view on GitHub

Discussion

1 `build_occ` proven

2 `build_sat` proven

3 `build_vars_le_slots` proven

4 `reduceB_correct` proven

5 `toBounded_polyTime` proven