5
$\begingroup$

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) this to related fora. Thank you for any help!

$\endgroup$
4
  • $\begingroup$ Are you familiari with algebraic complexity theory? $\endgroup$ Jan 29 at 9:04
  • $\begingroup$ @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. $\endgroup$ Jan 30 at 13:20
  • $\begingroup$ @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. $\endgroup$ Jan 31 at 4:20
  • $\begingroup$ 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. $\endgroup$ Feb 2 at 9:52

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.