Algebraic equivalent of SAT?

Question

Starting with a simple observation. If $x,y\in\{0,1\}$, then the arithmetic product $x\cdot y$ corresponds to the logical conjunction if we interpret $1$ as true and $0$ as false.

But then, for a generic propositional logic formula $\phi$ in $n$ variables, we can obtain a polynomial $f(\phi)$ as follows:

\begin{align} f(p) & = x_p \\ f(\neg \phi) & = 1 - f(\phi) \\ f(\phi_1\land\phi_2) &= f(\phi_1)\cdot f(\phi_2) \\ f(\phi_1\lor\phi_2) &= f(\neg(\neg\phi_1\land\neg\phi_2)) \\ &= 1-((1-f(\phi_1))(1-f(\phi_2))) \end{align}

Then if $f(\phi)=1$ has integer solutions in $[0,1]^n$, the formula is satisfiable.

For example, if $\phi\equiv p\to q\equiv\neg p \lor q$, then $f(\phi)=x_px_q-x_p+1$, and indeed $x_px_q-x_p+1=1$ holds for $x_p=0$ and for $x_q=1$.

So, finding this kind of roots of polynomials is NP-hard, as interesting as this might be.

My question risks to be too vague, but has this been used in NP-hardness proofs for some more interesting algebraic problem?

Is this connection between propositional formulas and polynomials (hence between SAT and algebra) useful for anything?

Answer 1

This is standard and widely used in computer science theory.

There are many references that use boolean polynomials with False -> 0 and True -> 1, or in other words, a polynomial over GF(2) used to represent a Boolean function $f:\{0,1\}^n \to \{0,1\}$. There are also many references that use polynomials constructed so that False -> -1 and True -> 1 (in the input) used to represent a Boolean function $f:\{-1,+1\}^n \to \{0,1\}$.

See, e.g.,

• Wikipedia: Boolean_function

• Wikipedia's article on Analysis of Boolean functions

• Algebraic normal form

• Ryan O'Donnell's book Analysis of Boolean Functions

• Claude Carlet's notes, Boolean Functions for Cryptography and Error Correcting Codes

• Polynomial method for complexity results

• A special case of the boolean multivariate quadratic polynomial problem

• Representing boolean function by a polynomial

Answer 2

I think what you are asking about is also known as "polynomial calculus" in proof complexity and SAT solving. It was introduced in [1, 2] to investigate whether coNP can be separated from NP or not. This amounts to the understanding the hardness of certifying the unsatisfiability of formulas in conjunctive normal form.

In theory polynomial calculus should have advantages over the DPLL/CDCL-based SAT solvers that dominate general purpose SAT solving today. In practise DPLL/CDCL works much better. Whether that's simply because much more engineering has gone into optimisation of DPLL/CDCL or whether there is a theoretical reason is unclear.

For some special cases of SAT solving, e.g. processors verification, polynomial calculus (using Groebner basis) is used. See e.g. [3] for an overview. I suspect that if this works well in practise, this would not be published. (Industrial research labs in this field tend to be rather secretive.)

---

1. Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. Using the Groebner Basis Algorithm to Find Proofs of Unsatisfiability. Link

2. Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. Space Complexity in Propositional Calculus. Link

3. Priyank Kalla, Leveraging Gröbner Bases and SAT for Hardware Verification: Can Gröbner bases help SAT solving? Link