Holography For Satisfiability

A Nullstellensatz Result For Boolean SAT.

Abstract

We present a discrete differential Nullstellensatz style result for finding satisfiability/unsatisfiability proofs to any 3 SAT formula, along with novel upper bound results. We begin by defining a notion of holographic algorithms sourced mainly from Valiant [1] and a topological interpretation drawn from the holographic principle [2] in physics. In our interpretation, holographic instructions (and their accumulating sequences) live as points on a differential manifold and are (partial with progression towards totality) solutions to the 3 SAT problem expressed in differential form. These forms can be expressed as (implicit) polynomials generated from ring expansions of an algebraic identity which Valiant says holographic algorithms must follow - a definition of algorithms with algorithmic identity based on an algebraic quantity (usually as sets of zeroes of some polynomial), instead of traditionally as a sequence of instructions. This definitional model which is summarized semantically in the following formulafor some problem p, forgetting the underlying model used to obtain the quantity is:∑(sets of solutions/zeroes of p) ∏(functional constraints on p) Our result is that, if any solutions exist for a formula F recast into an initial polynomial P(x) in some differential ring PR{x}, defined by the above identity, then they are multiplicative set extensions of the minimal solutions that our framework provides (they are values in a differentially closed field) and that these values are exactly the zeros of ideals in the ring of differential polynomials generated using P(x) reflexively itself as a basis.
Restated, our main theorem says that there exists an integration procedure for computing a differential closure as a prime model M, consisting of a single ideal, using P(x) as a basis, and when F is satisfiable, M is either a satisfying saturation model OR there exists satisfying saturation models derivable from M, where derivations are multiplicative interpretations, that isfor natural numbers i, n and k and a set of inducible interpretations S where all f are interpretations in S, t is the continuous time variable and X is the set of all satisfying solutions:
∀F, ∃M ⇒ ∀f, (n, f) ∈ S ∧ ∂
kf/ ∂
kt: Mk → X, ⇒ M = ∫P(x)∂ix∂it, iff F is satisfiable.
The differential ideal generated, or more specifically, its field of coeffficients, functions logically as an assignability predicate over solutions in the original formula, and in line with Tarski, our procedure provides an implicit model of truth over these predicates not directly expressible within the logic exposed by the predicates themselves. This procedure functions to yield an operator valued second order logic in line with Fagin’s theorem, capable of exactly describing the (holographic) algorithms that prove the 3 SAT formulae and therefore can be extended as an efficient logic over the whole NP class.