3
$\begingroup$

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.

Improve this question
$\endgroup$
7
  • 1
    $\begingroup$ $ik\in\{1,\dots,M\}$, where $M$ is number of variables. $\endgroup$
    – Valera
    Commented Oct 27, 2014 at 14:33
  • $\begingroup$ @RamirodelaVega I am not sure this is solution, since you might get contradiction $x_i \ne x_i$. $\endgroup$
    – joro
    Commented Oct 27, 2014 at 15:13
  • $\begingroup$ If $b_i=0$ this implies all involved $x_i$ are zero, so set them to zero and eliminate them from the the other equations. If equations remains, pick any solution to each equation by setting one $x$ to $1$. $\endgroup$
    – joro
    Commented Oct 27, 2014 at 15:15
  • $\begingroup$ Please see the updated version $\endgroup$
    – Valera
    Commented Oct 27, 2014 at 15:19
  • $\begingroup$ You should make it clearer that you are not trying to solve this system (which may be inconsistent), but rather satisfy as many (in some sense) of the equations as possible. $\endgroup$
    – Sam Hopkins
    Commented Oct 27, 2014 at 15:21

2 Answers 2

Reset to default
3
$\begingroup$

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

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thanks, this formulation does look equivalent. Any idea, if the MaxSat solvers would behave nicely with this type of clauses? And one more side question, since you look like an expert in the field: can you recommend open-source sat-solver, that can treat millions of variables and tens of millions of clauses? $\endgroup$
    – Valera
    Commented Oct 27, 2014 at 16:37
  • $\begingroup$ I’m sorry, but I do not have practical experience with SAT solvers, so I can’t give recommendations. My guess would be that a (MAX)SAT solver should be able to exploit the fact that the variable $y_i$ is localized to only four clauses (one of which is a unit clause), so the translation shouldn’t introduce any performance penalty, but there is really no way to know how efficient it is in practice other than trying it out. $\endgroup$
    – Emil Jeřábek
    Commented Oct 27, 2014 at 17:42
2
$\begingroup$

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

Improve this answer
$\endgroup$
3
  • $\begingroup$ This is not correct. The inequality $(1-x_i) + (1-x_j) + (1-x_k) + y_C \geq 1$ is not equivalen to $x_i\vee x_j \vee x_k = 0$, check for $(0, 0, 1)$. This can be somehow feasible to impose the following $(1-x_i) + (1-x_j) + (1-x_k) + y_C \geq 3$, but this will make weighting of $y_C$ sensitive to number of nonzero $x$'s in equation. $\endgroup$
    – Valera
    Commented Oct 27, 2014 at 16:27
  • 1
    $\begingroup$ For $x_i\lor x_j\lor x_k=0$, you can take the constraints $y_C-x_i\ge0$, $y_C-x_j\ge0$, $y_C-x_k\ge0$ instead. $\endgroup$
    – Emil Jeřábek
    Commented Oct 27, 2014 at 16:32
  • $\begingroup$ @EmilJeřábek cool, thanks for the help. $\endgroup$
    – Valera
    Commented Oct 27, 2014 at 16:40

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .