The Reduction from Satisfiability to (3,4)-Satisfiability

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

proven

Loading review…

Natural Language Statement

Definition

A CNF formula $F$ with $N$ literal occurrences, over variables below $V$ , is turned into a (3,4) formula in two steps.

Splitting. The occurrence at position $p$ of a variable $v$ is replaced by a fresh variable $w_{v,p}$ . A clause is chained through link variables $z_p$ : the clause $(l_0 \vee \dots \vee l_{L-1})$ becomes $(l_0 \vee z_0), (\bar z_0 \vee l_1 \vee z_1), \dots, (\bar z_{L-2} \vee l_{L-1})$ , and an empty clause stays empty. For every $v$ , the implications $w_{v,p+1} \to w_{v,p}$ , taken cyclically over all positions, force the copies of $v$ to agree. Afterwards every clause has at most three literals and every variable occurs at most three times.

Padding. Each clause with fewer than three literals is filled up with literals $\bar y$ , where every $y$ is a fresh variable that a private copy of Tovey's gadget forces to be true. The gadget has thirteen clauses on ten variables: $y$ occurs three times in it and each of the other nine variables four times.

On words, the reduction decodes a formula, applies the two steps and encodes the result. A word that encodes no formula is treated as the formula consisting of one empty clause.

Concept map

9 concepts; 1 descendant hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

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

In the paper

page 2 of this submission's paper

Lean source view on GitHub

Show types on hover

1	import Lax345332.ThreeFourSat
2
3	/-!
4	---
5	title: The Reduction from Satisfiability to (3,4)-Satisfiability
6	type: definition
7	---
8	A CNF formula $F$ with $N$ literal occurrences, over variables below $V$ , is turned into a
9	(3,4) formula in two steps.
10
11	Splitting. The occurrence at position $p$ of a variable $v$ is replaced by a fresh
12	variable $w_{v,p}$ . A clause is chained through link variables $z_p$ : the clause
13	$(l_0 \vee \dots \vee l_{L-1})$ becomes
14	$(l_0 \vee z_0), (\bar z_0 \vee l_1 \vee z_1), \dots, (\bar z_{L-2} \vee l_{L-1})$ , and an
15	empty clause stays empty. For every $v$ , the implications $w_{v,p+1} \to w_{v,p}$ , taken
16	cyclically over all positions, force the copies of $v$ to agree. Afterwards every clause
17	has at most three literals and every variable occurs at most three times.
18
19	Padding. Each clause with fewer than three literals is filled up with literals $\bar y$ ,
20	where every $y$ is a fresh variable that a private copy of Tovey's gadget forces to be
21	true. The gadget has thirteen clauses on ten variables: $y$ occurs three times in it and
22	each of the other nine variables four times.
23
24	On words, the reduction decodes a formula, applies the two steps and encodes the result. A
25	word that encodes no formula is treated as the formula consisting of one empty clause.
26
27	# Formalization Notes
28
29	The copies $w_{v,p}$ are created and tied together for all $v < V$ and $p < N$ , not only
30	for the pairs $(v, p)$ that occur. This way the cyclic successor of a position is simply
31	the next position, at the price of an output of quadratic size.
32	-/
33
34	namespace Lax345332.Construction
35
36	open Lax429075.CNF Lax429075.Encoding Lax434930.PolynomialTime Lax345332.ThreeFourSat
37
38	-- The gadget
39
40	/-- Tovey's thirteen clauses on the variables `g, g+1, …, g+9`; they force `g` to be true. -/
41	def gadget (g : ℕ) : Formula :=
42	let y := g
43	let a (j : ℕ) := g + 1 + 3 * j
44	let b (j : ℕ) := g + 2 + 3 * j
45	let d (j : ℕ) := g + 3 + 3 * j
46	((List.range 3).map fun j => [⟨y, true⟩, ⟨a j, true⟩, ⟨b j, true⟩]) ++
47	((List.range 3).flatMap fun j =>
48	[[⟨d j, true⟩, ⟨a j, true⟩, ⟨b j, false⟩], [⟨d j, true⟩, ⟨a j, false⟩, ⟨b j, true⟩],
49	[⟨d j, true⟩, ⟨a j, false⟩, ⟨b j, false⟩]]) ++
50	[[⟨d 0, false⟩, ⟨d 1, false⟩, ⟨d 2, false⟩]]
51
52	-- Padding
53
54	/-- The base of the `t`-th gadget of the `k`-th clause, above the variables below `B`. -/
55	def ybase (B k t : ℕ) : ℕ := B + 30 * k + 10 * t
56
57	/-- The padding literals of a clause of length `n`. -/
58	def pads (B k n : ℕ) : Clause := (List.range (3 - n)).map fun t => ⟨ybase B k t, false⟩
59
60	/-- The `k`-th clause, padded, with its three gadgets. -/
61	def unit (B k : ℕ) (C : Clause) : Formula :=
62	(C ++ pads B k C.length) ::
63	(gadget (ybase B k 0) ++ gadget (ybase B k 1) ++ gadget (ybase B k 2))
64
65	/-- Every clause of `G`, padded to three literals and followed by its gadgets. `B` bounds the
66	variables in use. -/
67	def pad (B : ℕ) (G : Formula) : Formula :=
68	(List.range G.length).flatMap fun k => unit B k (G.getD k [])
69
70	-- Splitting
71
72	/-- The copy of the variable `v` at position `p`. -/
73	def wv (V v p : ℕ) : ℕ := v + p * V
74
75	/-- The link variable after position `p`. -/
76	def zv (V N p : ℕ) : ℕ := V * N + p
77
78	/-- A placeholder literal, used when an index is past the end of a list. -/
79	def dflt : Literal := ⟨0, false⟩
80
81	/-- The `i`-th clause of the chain of `C`, whose first literal sits at position `o`: the
82	negated link before it (except for `i = 0`), the copy of the `i`-th literal, and the link
83	after it (except for the last). -/
84	def chainClause (V N o : ℕ) (C : Clause) (i : ℕ) : Clause :=
85	(if i = 0 then [] else [⟨zv V N (o + i - 1), false⟩]) ++
86	[⟨wv V (C.getD i dflt).index (o + i), (C.getD i dflt).positive⟩] ++
87	(if i + 1 = C.length then [] else [⟨zv V N (o + i), true⟩])
88
89	/-- The chain of the clause `C`, whose first literal sits at position `o`; an empty clause
90	becomes one empty clause. -/
91	def chainClauses (V N o : ℕ) (C : Clause) : Formula :=
92	if C.length = 0 then [[]] else (List.range C.length).map (chainClause V N o C)
93
94	/-- The chains of all clauses of a formula, the first literal of the formula being at
95	position `o`. -/
96	def chains (V N : ℕ) : ℕ → Formula → Formula
97	\| _, [] => []
98	\| o, C :: F => chainClauses V N o C ++ chains V N (o + C.length) F
99
100	/-- The cyclic successor on positions. -/
101	def next (N p : ℕ) : ℕ := if p + 1 < N then p + 1 else 0
102
103	/-- The cycle clauses `w v (next p) → w v p`, one for every variable `v < V` and position
104	`p < N`. Their variables are numbered `k = w v p`. -/
105	def cycles (V N : ℕ) : Formula :=
106	(List.range (V * N)).map fun k => [⟨k, true⟩, ⟨wv V (k % V) (next N (k / V)), false⟩]
107
108	/-- The number of literal occurrences of a formula. -/
109	def size (F : Formula) : ℕ := (F.map List.length).sum
110
111	/-- A strict bound on the variable indices of a formula (at least 1). -/
112	def bound : Formula → ℕ
113	\| [] => 1
114	\| C :: F => max (C.foldr (fun l b => max (l.index + 1) b) 1) (bound F)
115
116	/-- The splitting step: the chains of all clauses, then the cycle clauses. -/
117	def split (F : Formula) : Formula :=
118	chains (bound F) (size F) 0 F ++ cycles (bound F) (size F)
119
120	-- The reduction
121
122	/-- The reduction on formulas: split, then pad above every variable in use. -/
123	def transform (F : Formula) : Formula := pad (bound F * size F + size F) (split F)
124
125	/-- The formula a word stands for: the decoded one, or one empty clause if the word encodes
126	no formula. -/
127	def parseF (w : Word) : Formula := (decodeCNF w).getD [[]]
128
129	/-- The reduction on words. -/
130	def reduce (w : Word) : Word := encodeCNF (transform (parseF w))
131
132	/-- The image is a (3,4) formula. -/
133	axiom transform_isThreeFour (F : Formula) : IsThreeFour (transform F)
134
135	/-- The image is satisfiable exactly when the formula is. -/
136	axiom transform_sat (F : Formula) : Satisfiable F ↔ Satisfiable (transform F)
137
138	/-- The reduction on words is correct. -/
139	axiom reduce_correct (w : Word) : w ∈ Lax429075.Satisfiability.SAT ↔ reduce w ∈ SAT34
140
141	/-- The reduction on words is computable in polynomial time. -/
142	axiom reduce_polyTime : Nonempty (Turing.TM2ComputableInPolyTime id id reduce)
143
144	end Lax345332.Construction
145

Show ProofShow ProofShow ProofShow Proof

Formalization Notes

The copies $w_{v,p}$ are created and tied together for all $v < V$ and $p < N$ , not only for the pairs $(v, p)$ that occur. This way the cyclic successor of a position is simply the next position, at the price of an output of quadratic size.

Builds on

Lax345332.ThreeFourSat

Used by

Lax345332.Copies

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 Satisfiability to (3,4)-Satisfiability

Flags

Flag this concept

Natural Language Statement

Definition

1 `reduce_correct` proven

2 `reduce_polyTime` proven

3 `transform_isThreeFour` proven

4 `transform_sat` proven

In the paper

Lean source view on GitHub

Discussion

Settings

Your comments

The Reduction from Satisfiability to (3,4)-Satisfiability

Natural Language Statement

Definition

1 reduce_correct proven

2 reduce_polyTime proven

3 transform_isThreeFour proven

4 transform_sat proven

In the paper

Lean source view on GitHub

Discussion

1 `reduce_correct` proven

2 `reduce_polyTime` proven

3 `transform_isThreeFour` proven

4 `transform_sat` proven