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

Question

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

Answer 1

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;