# How to solve a system of nonlinear equations in GF(2)

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$ ?

• Are you asking about algorithms or software packages? – saulspatz Apr 16 '18 at 17:03
• @saulspatz I'm more interested in algorithms but software packages are welcomed! – Raoul722 Apr 16 '18 at 17:08
• 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. – Axel Kemper Apr 16 '18 at 17:26
• @AxelKemper Thank you for these tips. How to proceed to translate a boolean system of equations into a netlist of logical gates? – Raoul722 Apr 16 '18 at 18:08

Extended comment:

Your example written as netlist for bc2cnf:

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


Shorter form without auxiliary variables:

BC1.1
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;