13
$\begingroup$

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?

$\endgroup$
0

2 Answers 2

22
$\begingroup$

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.,

$\endgroup$
1
  • 1
    $\begingroup$ Wow that’s exactly the kind of answer I was hoping for. Thanks! $\endgroup$
    – gigabytes
    Jan 7 at 23:34
12
$\begingroup$

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

$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.