The reduction graph

Lax689614.Construction · concepts/Lax689614/Construction.lean · lax-689614

definition

Loading review…

Natural Language Statement

Definition

For a formula with $n$ variables and $m$ clauses, put $K=4n+6$ and $R=m+2n+2$ . The vertices are $s,t$ , $a_j,b_j$ for clauses, $v_i,t_i$ for $0\leq i<R$ , $f_i$ for variables, and $y_i,z_i$ for $0\leq i<K$ . The edges are $st$ , $sa_j$ , $a_jb_j$ , all $b_jv_i$ , $v_it_i$ , $v_if_i$ for $i<n$ , $b_jf_i$ when $x_i\in C_j$ , and $sy_i,y_iz_i$ . Labels use consecutive blocks in the displayed order. The correctness statements assume an odd number of clauses.

Concept map

5 concepts; 4 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

1	import Lax689614.Encoding
2
3	/-!
4	---
5	title: The reduction graph
6	type: definition
7	---
8	For a formula with $n$ variables and $m$ clauses, put $K=4n+6$ and
9	$R=m+2n+2$ . The vertices are $s,t$ , $a_j,b_j$ for clauses,
10	$v_i,t_i$ for $0\leq i<R$ , $f_i$ for variables, and $y_i,z_i$
11	for $0\leq i<K$ . The edges are $st$ , $sa_j$ , $a_jb_j$ , all $b_jv_i$ ,
12	$v_it_i$ , $v_if_i$ for $i<n$ , $b_jf_i$ when $x_i\in C_j$ ,
13	and $sy_i,y_iz_i$ . Labels use consecutive blocks in the displayed order.
14	The correctness statements assume an odd number of clauses.
15	-/
16
17	namespace Lax689614.Construction
18
19	open PositiveCNF
20
21	def K (φ : Formula) : ℕ := 4 * φ.nvars + 6
22	def R (φ : Formula) : ℕ := φ.clauses.length + 2 * φ.nvars + 2
23	def size (φ : Formula) : ℕ := 2 + 2 * φ.clauses.length + 2 * R φ + φ.nvars + 2 * K φ
24
25	def s : ℕ := 0
26	def t : ℕ := 1
27	def a (_φ : Formula) (j : ℕ) : ℕ := 2 + j
28	def b (φ : Formula) (j : ℕ) : ℕ := 2 + φ.clauses.length + j
29	def v (φ : Formula) (i : ℕ) : ℕ := 2 + 2 * φ.clauses.length + i
30	def vt (φ : Formula) (i : ℕ) : ℕ := 2 + 2 * φ.clauses.length + R φ + i
31	def f (φ : Formula) (i : ℕ) : ℕ := 2 + 2 * φ.clauses.length + 2 * R φ + i
32	def y (φ : Formula) (i : ℕ) : ℕ :=
33	2 + 2 * φ.clauses.length + 2 * R φ + φ.nvars + i
34	def z (φ : Formula) (i : ℕ) : ℕ :=
35	2 + 2 * φ.clauses.length + 2 * R φ + φ.nvars + K φ + i
36
37	def Edge (φ : Formula) (u w : ℕ) : Prop :=
38	(u = s ∧ w = t) ∨
39	(∃ j < φ.clauses.length, u = s ∧ w = a φ j) ∨
40	(∃ j < φ.clauses.length, u = a φ j ∧ w = b φ j) ∨
41	(∃ j < φ.clauses.length, ∃ i < R φ, u = b φ j ∧ w = v φ i) ∨
42	(∃ i < R φ, u = v φ i ∧ w = vt φ i) ∨
43	(∃ i < φ.nvars, u = v φ i ∧ w = f φ i) ∨
44	(∃ j : Fin φ.clauses.length, ∃ i ∈ φ.clauses[j],
45	u = b φ j ∧ w = f φ i) ∨
46	(∃ i < K φ, u = s ∧ w = y φ i) ∨
47	(∃ i < K φ, u = y φ i ∧ w = z φ i)
48
49	def graph (φ : Formula) : SimpleGraph ℕ := SimpleGraph.fromRel (Edge φ)
50
51	def board (φ : Formula) : Finset ℕ := Finset.range (size φ)
52
53	def labeledGraph (φ : Formula) : Encoding.Graph where
54	vertices := size φ
55	graph := SimpleGraph.fromRel fun u v : Fin (size φ) => Edge φ u.val v.val
56
57	end Lax689614.Construction
58

Builds on

Lax689614.Encoding

Used by

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 graph

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments