Let's say I have a system of $n$ nonlinear boolean equations and $n$ unknowns like:

$ \begin{cases} (x_i \oplus \neg x_j) \wedge x_n &=1\\ &\vdots \\ (x_k \wedge x_i \oplus x_j) \wedge \neg x_l &=0 \end{cases} $

where $i,k,l \leq n$.

What is the most efficient method to solve this kind of systems when $n > 200$ ?

  • $\begingroup$ Are you asking about algorithms or software packages? $\endgroup$ – saulspatz Apr 16 '18 at 17:03
  • $\begingroup$ @saulspatz I'm more interested in algorithms but software packages are welcomed! $\endgroup$ – Raoul722 Apr 16 '18 at 17:08
  • 1
    $\begingroup$ You could write your problem as netlist of logical gates, use bc2cnf to translate it into Conjunctive Normal Form (CNF) and a SAT solver like Z3 or Cryptominisat to get a solution. An easy alternative is a constraint solver like MiniZinc. $\endgroup$ – Axel Kemper Apr 16 '18 at 17:26
  • $\begingroup$ @AxelKemper Thank you for these tips. How to proceed to translate a boolean system of equations into a netlist of logical gates? $\endgroup$ – Raoul722 Apr 16 '18 at 18:08

Extended comment:

Your example written as netlist for bc2cnf:

a1 := (xi ^ !xj) & xn;
a2 := (xk & xi ^ xj) & !xl;
ASSIGN a1, !a2;

Shorter form without auxiliary variables:

ASSIGN (xi ^ !xj) & xn;
ASSIGN !((xk & xi ^ xj) & !xl);

MiniZinc model:

var bool: xi;
var bool: xj;
var bool: xk;
var bool: xl;
var bool: xn;

constraint (xi != not xj) /\ xn;
constraint ((xk /\ xi) != xj) /\ not xl;

solve satisfy;

Your Answer

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

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