<p>I think what you are asking about is also known as &quot;polynomial calculus&quot; 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.</p>
<p>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.</p>
<p>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.)</p>
<hr />
<sub>
<ol>
<li><p>Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. <em>Using the Groebner Basis Algorithm to Find Proofs
of Unsatisfiability.</em> <a href="https://dl.acm.org/doi/10.1145/237814.237860" rel="noreferrer">Link</a></p>
</li>
<li><p>Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. <em>Space Complexity in
Propositional Calculus.</em> <a href="http://people.cs.uchicago.edu/%7Erazborov/files/spaceres.pdf" rel="noreferrer">Link</a></p>
</li>
<li><p>Priyank Kalla, <em>Leveraging Gröbner Bases and SAT for Hardware Verification: Can Gröbner bases help SAT solving?</em> <a href="https://www.birs.ca/workshops/2014/14w5101/files/kalla_birs_talk.pdf" rel="noreferrer">Link</a></p>
</li>
</ol>
</sub>

CC BY-SA 4.0
2023-01-08T15:00:29.960Z
2023-01-08T16:04:54.160Z
2023-01-08T16:04:54.160Z
Martin Berger
<p>This is standard and widely used in computer science theory.</p>
<p>There are many references that use boolean polynomials with False -&gt; 0 and True -&gt; 1, or in other words, a polynomial over GF(2) used to represent a Boolean function <span class="math-container">$f:\{0,1\}^n \to \{0,1\}$</span>.  There are also many references that use polynomials constructed so that False -&gt; -1 and True -&gt; 1 (in the input) used to represent a Boolean function <span class="math-container">$f:\{-1,+1\}^n \to \{0,1\}$</span>.</p>
<p>See, e.g.,</p>
<ul>
<li><p>Wikipedia: <a href="https://en.wikipedia.org/wiki/Boolean_function#Real_polynomial_form" rel="noreferrer">Boolean_function</a></p>
</li>
<li><p>Wikipedia's article on <a href="https://en.wikipedia.org/wiki/Analysis_of_Boolean_functions" rel="noreferrer">Analysis of Boolean functions</a></p>
</li>
<li><p><a href="https://en.wikipedia.org/wiki/Algebraic_normal_form" rel="noreferrer">Algebraic normal form</a></p>
</li>
<li><p>Ryan O'Donnell's book <a href="https://www.cs.cmu.edu/%7Eodonnell/papers/Analysis-of-Boolean-Functions-by-Ryan-ODonnell.pdf" rel="noreferrer">Analysis of Boolean Functions</a></p>
</li>
<li><p>Claude Carlet's notes, <a href="http://www.math.univ-paris13.fr/%7Ecarlet/chap-fcts-Bool-corr.pdf" rel="noreferrer">Boolean Functions for Cryptography and Error Correcting Codes</a></p>
</li>
<li><p><a href="https://cstheory.stackexchange.com/q/2774/5038">Polynomial method for complexity results</a></p>
</li>
<li><p><a href="https://cstheory.stackexchange.com/q/33698/5038">A special case of the boolean multivariate quadratic polynomial problem</a></p>
</li>
<li><p><a href="https://cstheory.stackexchange.com/q/27042/5038">Representing boolean function by a polynomial</a></p>
</li>
</ul>

CC BY-SA 4.0
2023-01-07T23:34:22.720Z
Wow that’s exactly the kind of answer I was hoping for. Thanks!
Nicola Gigante
CC BY-SA 4.0
2023-01-07T23:25:58.223Z
2023-01-09T19:03:44.803Z
2023-01-09T19:03:44.803Z
D.W.
<p>Starting with a simple observation. If <span class="math-container">$x,y\in\{0,1\}$</span>, then the arithmetic product <span class="math-container">$x\cdot y$</span> corresponds to the logical conjunction if we interpret <span class="math-container">$1$</span> as <em>true</em> and <span class="math-container">$0$</span> as <em>false</em>.</p>
<p>But then, for a generic propositional logic formula <span class="math-container">$\phi$</span> in <span class="math-container">$n$</span> variables, we can obtain a polynomial <span class="math-container">$f(\phi)$</span> as follows:</p>
<p><span class="math-container">\begin{align}
f(p) &amp; = x_p \\
f(\neg \phi) &amp; = 1 - f(\phi) \\
f(\phi_1\land\phi_2) &amp;= f(\phi_1)\cdot f(\phi_2) \\
f(\phi_1\lor\phi_2) &amp;= f(\neg(\neg\phi_1\land\neg\phi_2)) \\
 &amp;= 1-((1-f(\phi_1))(1-f(\phi_2)))
\end{align}</span></p>
<p>Then if <span class="math-container">$f(\phi)=1$</span> has integer solutions in <span class="math-container">$[0,1]^n$</span>, the formula is satisfiable.</p>
<p>For example, if <span class="math-container">$\phi\equiv p\to q\equiv\neg p \lor q$</span>, then <span class="math-container">$f(\phi)=x_px_q-x_p+1$</span>, and indeed <span class="math-container">$x_px_q-x_p+1=1$</span> holds for <span class="math-container">$x_p=0$</span> and for <span class="math-container">$x_q=1$</span>.</p>
<p>So, finding this kind of roots of polynomials is NP-hard, as interesting as this might be.</p>
<p>My question risks to be too vague, but has this been used in NP-hardness proofs for some more interesting algebraic problem?</p>
<p>Is this connection between propositional formulas and polynomials (hence between SAT and algebra) useful for anything?</p>

<sat><polynomials><proof-complexity>
Algebraic equivalent of SAT?
Nicola Gigante
# Algebraic equivalent of SAT?

(Asked by: username_0 on 2023-01-07)

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?

**Tags:** sat, polynomials, proof-complexity

---

## 2 answers

### Answer by username_2 on 2023-01-07. Score: 24 | Accepted answer

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](https://en.wikipedia.org/wiki/Boolean_function#Real_polynomial_form)
* Wikipedia's article on [Analysis of Boolean functions](https://en.wikipedia.org/wiki/Analysis_of_Boolean_functions)
* [Algebraic normal form](https://en.wikipedia.org/wiki/Algebraic_normal_form)
* Ryan O'Donnell's book [Analysis of Boolean Functions](https://www.cs.cmu.edu/%7Eodonnell/papers/Analysis-of-Boolean-Functions-by-Ryan-ODonnell.pdf)
* Claude Carlet's notes, [Boolean Functions for Cryptography and Error Correcting Codes](http://www.math.univ-paris13.fr/%7Ecarlet/chap-fcts-Bool-corr.pdf)
* [Polynomial method for complexity results](https://cstheory.stackexchange.com/q/2774/5038)
* [A special case of the boolean multivariate quadratic polynomial problem](https://cstheory.stackexchange.com/q/33698/5038)
* [Representing boolean function by a polynomial](https://cstheory.stackexchange.com/q/27042/5038)

> **Comments:**
> **username_0**: Wow that’s exactly the kind of answer I was hoping for. Thanks!  

---

### Answer by username_1 on 2023-01-08. Score: 13

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](https://dl.acm.org/doi/10.1145/237814.237860)
2. Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. *Space Complexity in
   Propositional Calculus.* [Link](http://people.cs.uchicago.edu/%7Erazborov/files/spaceres.pdf)
3. Priyank Kalla, *Leveraging Gröbner Bases and SAT for Hardware Verification: Can Gröbner bases help SAT solving?* [Link](https://www.birs.ca/workshops/2014/14w5101/files/kalla_birs_talk.pdf)


---

