<p>Let <span class="math-container">$v(a, b)$</span> be a binary predicate, and define <span class="math-container">$\phi$</span> as follows:</p>
<p><span class="math-container">$$\phi: v(a_1, b_1) \land v(a_1, b_2) \land (a_1, b_3)$$</span></p>
<p>where our universe consists of two sorts <span class="math-container">$A: \{a_1, a_2, a_3\}$</span> and <span class="math-container">$B: \{b_1, b_2, b_3\}$</span>. A priori, we can let <span class="math-container">$G = S_3 \times S_3$</span> act on logical formulas, and this will permute them syntactically. In the case of <span class="math-container">$\phi$</span>, we may fully act on it by <span class="math-container">$G$</span> and get an orbit of size 36. However, it is clear that only 3 of these are semantically different, namely the ones pertaining to different choice of <span class="math-container">$a_i$</span>.</p>
<p>The current way of doing this computationally is to generate the entire orbit under <span class="math-container">$G$</span>, then reducing modulo semantic equivalence. This may be pretty expensive for larger formulae, and I have a vague intuition that this may be approached via some type of Galois theory analog where I can access what groups semantically fix a particular formula.</p>
<p>We may translate logical formulae into Boolean polynomials, and vice versa. For example, if <span class="math-container">$x, y \in \{0, 1\}$</span> we translate <span class="math-container">$x \land y$</span> as <span class="math-container">$xy \in (\mathbb{Z}/2\mathbb{Z})[x, y]$</span>. Likewise <span class="math-container">$x \oplus y$</span> (XOR) <span class="math-container">$\leftrightarrow x + y$</span>, and <span class="math-container">$\neg x \leftrightarrow 1 - x$</span>.</p>
<p><em>Disclaimer:</em> there might be tiny issues with this proposed map into <span class="math-container">$(\mathbb{Z}/2\mathbb{Z})[\bar{X}]$</span> that can be fixed with minor adjustments; however, the key idea is we get a polynomial on the other side that evaluates to 0 iff the formula is true and to 1 iff the formula is false. Finding a satisfying assignment of variables is then equivalent to finding a root of this polynomial. This scheme might get overly complicated with predicates such a <span class="math-container">$v$</span> above, so if easier consider only the case of Boolean variables and I can worry about encoding such predicates later.</p>
<p>My main questions are the following:</p>
<ol>
<li>Are root-finding algorithms fast enough to make this a feasible way to SAT solve?</li>
<li>Are algorithms for computing Galois groups reasonably fast? As finding formulae that are semantically equivalent under permutation seems to be related to the Galois group (or perhaps what is fixed by the Galois group) of a formulas related polynomial.</li>
<li>Has anyone worked with something like this, or where can I go to learn more about properties of these Boolean polynomials?</li>
</ol>
<p>Given a Galois group <span class="math-container">$G$</span> of a polynomial <span class="math-container">$f$</span>, we often look at <span class="math-container">$\prod_{\sigma \in G} \sigma(f)$</span>. I'm interested in what the analogous formula looks like/can tell is on the logical side of this bijection. Additionally, I'm hoping to leverage other algebraic facts about the associated polynomials to gain knowledge on the logical side. In particular, this may speed up incremental induction algorithms by drastically reducing the search space and/or learning more clauses at each step than current algorithms.</p>
<p>I apologize if this question is a little open-ended and not fleshed out enough. Additionally, I recognize that this intersects with math enough so <a href="https://mathoverflow.net/q/414588/37212">I cross-posted on MathOverflow (only visible to some users)</a> this to related fora. Thank you for any help!</p>

CC BY-SA 4.0
2022-01-29T09:04:37.530Z
Are you familiari with **algebraic complexity theory**?
Andrej Bauer
CC BY-SA 4.0
2022-01-30T13:20:55.830Z
@AndrejBauer Algebraic complexity theory is asymptotic and worst-case oriented.
I imagine that the question is about SAT-solving performance in
practise. SAT being NP-complete, SAT should not be feasible
according to (worst-case) complexity theory. Yet, SAT
solvers work really well. Alternative proof systems for SAT solving
like *Cutting Planes* and *Polynomial Calculus* are known to be better
than DPLL in an asymptotic sense.  Can SAT solvers based on
polynomials or similar beat DPLL/CDCL based SAT-solvers in practise?
Not that we know.
Martin Berger
CC BY-SA 4.0
2022-01-31T04:20:09.503Z
@MartinBerger yes, precisely! I am interested in these in practice rather than in theory. I understand that SAT-solving is in general NP-complete, but the problems that show up in certain tasks (verification, automated proofs, etc) may hopefully have enough regularity to run fast enough on modern hardware.
Steven Schaefer
CC BY-SA 4.0
2022-02-02T09:52:40.703Z
There has been a bit of research on using Gröbner basis for improving SAT solvers. We know that in theory this will help (in the limit), but I am not aware of anyone who has been able to get speed-ups in practical SAT solving. The place where this might be most immediately applicable is hardware verification of finite-precision arithmetic datapaths.
Martin Berger
<lo.logic><fl.formal-languages><algebra><formal-methods>
Satisfiability and a Galois Theory Analog
Steven Schaefer
# Satisfiability and a Galois Theory Analog

(Asked by: username_0 on 2022-01-25)

Let $v(a, b)$ be a binary predicate, and define $\phi$ as follows:

$$\phi: v(a\_1, b\_1) \land v(a\_1, b\_2) \land (a\_1, b\_3)$$

where our universe consists of two sorts $A: \{a\_1, a\_2, a\_3\}$ and $B: \{b\_1, b\_2, b\_3\}$. A priori, we can let $G = S\_3 \times S\_3$ act on logical formulas, and this will permute them syntactically. In the case of $\phi$, we may fully act on it by $G$ and get an orbit of size 36. However, it is clear that only 3 of these are semantically different, namely the ones pertaining to different choice of $a\_i$.

The current way of doing this computationally is to generate the entire orbit under $G$, then reducing modulo semantic equivalence. This may be pretty expensive for larger formulae, and I have a vague intuition that this may be approached via some type of Galois theory analog where I can access what groups semantically fix a particular formula.

We may translate logical formulae into Boolean polynomials, and vice versa. For example, if $x, y \in \{0, 1\}$ we translate $x \land y$ as $xy \in (\mathbb{Z}/2\mathbb{Z})[x, y]$. Likewise $x \oplus y$ (XOR) $\leftrightarrow x + y$, and $\neg x \leftrightarrow 1 - x$.

*Disclaimer:* there might be tiny issues with this proposed map into $(\mathbb{Z}/2\mathbb{Z})[\bar{X}]$ that can be fixed with minor adjustments; however, the key idea is we get a polynomial on the other side that evaluates to 0 iff the formula is true and to 1 iff the formula is false. Finding a satisfying assignment of variables is then equivalent to finding a root of this polynomial. This scheme might get overly complicated with predicates such a $v$ above, so if easier consider only the case of Boolean variables and I can worry about encoding such predicates later.

My main questions are the following:

1. Are root-finding algorithms fast enough to make this a feasible way to SAT solve?
2. Are algorithms for computing Galois groups reasonably fast? As finding formulae that are semantically equivalent under permutation seems to be related to the Galois group (or perhaps what is fixed by the Galois group) of a formulas related polynomial.
3. Has anyone worked with something like this, or where can I go to learn more about properties of these Boolean polynomials?

Given a Galois group $G$ of a polynomial $f$, we often look at $\prod\_{\sigma \in G} \sigma(f)$. I'm interested in what the analogous formula looks like/can tell is on the logical side of this bijection. Additionally, I'm hoping to leverage other algebraic facts about the associated polynomials to gain knowledge on the logical side. In particular, this may speed up incremental induction algorithms by drastically reducing the search space and/or learning more clauses at each step than current algorithms.

I apologize if this question is a little open-ended and not fleshed out enough. Additionally, I recognize that this intersects with math enough so [I cross-posted on MathOverflow (only visible to some users)](https://mathoverflow.net/q/414588/37212) this to related fora. Thank you for any help!

**Tags:** lo.logic, fl.formal-languages, algebra, formal-methods

> **Comments:**
> **username_1**: Are you familiari with **algebraic complexity theory**?  
> **username_2**: @AndrejBauer Algebraic complexity theory is asymptotic and worst-case oriented. I imagine that the question is about SAT-solving performance in practise. SAT being NP-complete, SAT should not be feasible according to (worst-case) complexity theory. Yet, SAT solvers work really well. Alternative proof systems for SAT solving like *Cutting Planes* and *Polynomial Calculus* are known to be better than DPLL in an asymptotic sense.  Can SAT solvers based on polynomials or similar beat DPLL/CDCL based SAT-solvers in practise? Not that we know.  
> **username_0**: @MartinBerger yes, precisely! I am interested in these in practice rather than in theory. I understand that SAT-solving is in general NP-complete, but the problems that show up in certain tasks (verification, automated proofs, etc) may hopefully have enough regularity to run fast enough on modern hardware.  
> **username_2**: There has been a bit of research on using Gröbner basis for improving SAT solvers. We know that in theory this will help (in the limit), but I am not aware of anyone who has been able to get speed-ups in practical SAT solving. The place where this might be most immediately applicable is hardware verification of finite-precision arithmetic datapaths.  

---

## 0 answers

