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.

$\endgroup$
7
  • 1
    $\begingroup$ $ik\in\{1,\dots,M\}$, where $M$ is number of variables. $\endgroup$
    – Valera
    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
    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
    Oct 27, 2014 at 15:15
  • $\begingroup$ Please see the updated version $\endgroup$
    – Valera
    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$ Oct 27, 2014 at 15:21

2 Answers 2

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

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

$\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
    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$ Oct 27, 2014 at 16:32
  • $\begingroup$ @EmilJeřábek cool, thanks for the help. $\endgroup$
    – Valera
    Oct 27, 2014 at 16:40

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.