HORN-SAT to CVP: the circuit that runs unit propagation #

The interpretation built here draws, inside a Language.sat-instance, the monotone circuit that evaluates unit propagation and reports failure of Horn satisfiability. Reducing from the complement is what keeps the circuit monotone – a circuit that reports satisfiability would have to negate the propagation – and costs nothing, since polynomial time is closed under complement (DescriptiveComplexity.piP_zero_eq), so hardness for HORNSATᶜ is hardness for HORNSAT; that step is taken in DescriptiveComplexity.Problems.Cvp.Hardness.

The layout #

Unit propagation is a fixed point, and a circuit is acyclic, so the stages are unrolled: the third coordinate of a gate is an element of the universe read as a stage number through its rank in the order (DescriptiveComplexity.orank), and Nat.card A stages suffice (DescriptiveComplexity.forced_forcedIn_card). Two more chains turn the two unbounded quantifiers of one propagation round into fan-in two, each walking the order one cover at a time:

bd c y s – a conjunction chain: every negative literal y' ≤ y of the clause c is forced within orank s rounds. Its right input is the gate hd y' ⊤ (pred s) when y is a negative literal of c, and the constant 1 when it is not: the wiring tests negIn, which is what an interpretation may do and a fixed circuit may not;
hd x c s – a disjunction chain: some clause c' ≤ c has x as its positive literal and all its negative literals forced within orank s rounds. At c = ⊤ this is one propagation round, so hd x ⊤ s is “x is forced within orank s + 1 rounds”;
bdTop c y – the same conjunction chain read at the last stage, needed because bd c y s reads the forced set one stage below s and the goal clause has to be tested against the fixed point itself;
gl c – a disjunction chain over the goal clauses: some clause c' ≤ c has no positive literal and all its negative literals forced. Its base carries the Horn condition: at c = ⊥ the chain starts from the constant 1 when the instance is not Horn, so a non-Horn instance is a yes-instance outright, and from the constant 0 when it is. The output gate is gl ⊤.

Junk is disposed of in the usual way: the coordinates a tag does not use are pinned to the minimum, and the copies with other coordinates carry no mark and no wire, so they derive nothing and are wired to nothing.

The tags #

source

inductive DescriptiveComplexity.CvpTag :

Type

The tags of the interpretation: the two constants, the two conjunction chains, the propagation chain and the goal chain.

tt : CvpTag
The constant 1 gate.
ff : CvpTag
The constant 0 gate.
bd : CvpTag
bd c y s: all negative literals of c up to y are forced within orank s rounds.
bdTop : CvpTag
bdTop c y: the same, read at the last stage.
hd : CvpTag
hd x c s: some clause up to c forces x within orank s + 1 rounds.
gl : CvpTag
gl c: some clause up to c is a falsified goal clause.

Instances For

Dependency graph

source

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqCvpTag :

DecidableEq CvpTag

Equations

DescriptiveComplexity.instDecidableEqCvpTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Dependency graph

source

@[instance_reducible]

instance DescriptiveComplexity.instFintypeCvpTag :

Fintype CvpTag

Equations

One or more equations did not get rendered due to their size.

Dependency graph

source

instance DescriptiveComplexity.instNonemptyCvpTag :

Nonempty CvpTag

Dependency graph

The formula builders #

The occurrence builders of DescriptiveComplexity.SatOcc supply clF, posF, negF and eqF over the ordered expansion; only three builders are new. All are parameterized by the variables they speak about, so that the same builder serves the unary marks (variables (0, j)) and the binary wires (variables (0, j) for the gate and (1, j) for its input).

source

noncomputable def DescriptiveComplexity.CvpInterp.noPosClF {α : Type} (c : α) :

SatOcc.satOrd.Formula α

“c is a clause with no positive literal”, i.e., a goal clause: the shape that makes an instance unsatisfiable once its negative literals are forced.

Equations