System of boolean equations, Satisfiability Are there any methods to "solve" large systems of boolean equations?
$$x_{i1}\vee x_{i2}\vee x_{i3} = b_i, \quad\text{for}\quad i=1,\dots,N,$$
where $x_i, b_i \in\{0, 1\}$
For example
$$x_{1}\vee x_{2}\vee x_{5} = 0$$
$$x_{1}\vee x_{3}\vee x_{4} = 1$$
$$x_{2}\vee x_{3}\vee x_{5} = 1$$
$$x_{1}\vee x_{4}\vee x_{5} = 1$$
$$x_{1}\vee x_{2}\vee x_{3} = 0$$
$$...$$
The problem is to find $x$, that satisfies the most of equations. I couldn't employ any maxsat-like method, or integer linear programming to solve this problem.
 A: You can reduce the problem to MAXSAT as follows. For each equation $x_{i1}\lor x_{i2}\lor x_{i3}=1$, include directly the clause $x_{i1}\lor x_{i2}\lor x_{i3}$. For each equation $x_{i1}\lor x_{i2}\lor x_{i3}=0$, choose a fresh variable $y_i$, and include the four clauses
\begin{gather}
y_i\lor\neg x_{i1}\\
y_i\lor\neg x_{i2}\\
y_i\lor\neg x_{i3}\\
\neg y_i
\end{gather}
Given an assignment to the original variables, you can satisfy all 4 clauses if $x_{i1}=x_{i2}=x_{i3}=0$ by making $y_i=0$, otherwise you can satisfy 3 of them by making $y_i=1$. Thus, the maximum number of satisfied clauses is the maximum number of satisfied original equations plus 3 times the number of equations with $b_i=0$.
A: This is only an answer because it is maybe too long for a comment, but here is an integer linear program formulation: for each disjunction constraint $C$ add a variable $y_C \in \{0,1\}$, and replace $x_i \vee x_j \vee x_k = 0$ with $(1-x_i)+(1-x_j)+(1-x_k)+y_C \geq 1$ and $x_i \vee x_j \vee x_k = 1$ with $x_i + x_j + x_k + y_C \geq 1$.  Each $y_C$ can be zero only if the corresponding $x$'s are picked to satisfy the constraint.  The objective is to minimize $\sum y_C$.
