3
$\begingroup$

I have a (fairly large) system of polynomial equations, of the form $$ c_1d_1=0,\ c_1d_2+c_2d_1=0,\ldots $$ (In case it is relevant, all the polynomials are homogeneous of degree 2, except for exactly one which is of the form "homogeneous poly of degree 2"=1.) I need to check if the system is satisfiable over $\mathbb{F}_2$. When it is, I'd also like to find one satisfying solution.

I've tried using Mathematica's built-in "Reduce" and "FindInstance" functions, but they time out. My system can be translated into an SAT problem, which should be tractable. So, my questions are the following:

Are SAT systems the right way to go? If so, which one should I use (and how do I transfer my system from Mathematica to the SAT solver?) If not, what is a better option?

Improve this question
$\endgroup$
4
  • $\begingroup$ Recent versions of Maple include a SAT solver based on MiniSAT. And it also has a translator from Mathematica (I don't know, however, whether your Mathematica data are in a format that translates directly to the correct format for Maple's Satisfy comand). $\endgroup$
    – Robert Israel
    Commented Feb 28 at 23:08
  • $\begingroup$ Is your system small enough that either libFES or the crossbred algorithm implemented by Charles Bouillaguet can handle it? $\endgroup$
    – j.p.
    Commented Feb 29 at 7:02
  • $\begingroup$ @j.p. No idea. I'm planning to work with hundreds of polynomials in hundreds of variables. I don't expect this is too big for most systems. $\endgroup$
    – Pace Nielsen
    Commented Feb 29 at 14:54
  • $\begingroup$ It turns out that Mathematica has a satisfiability solver "SatisfiableQ" which works well for the problem. $\endgroup$
    – Pace Nielsen
    Commented Mar 25 at 3:42

0

Reset to default

You must log in to answer this question.