# Solving systems of boolean equations

So I have a system of equations where varibles range over $\{0,1\}$ and the only operation is logical or ($\lor$). Each equation is of the one of two forms

1) $a = b \lor c$

2) $1 = a \lor b$

where a, b ,and c are all positive literals. No negations occur anywhere in these systems of equations.

We say $(x_1, ..., x_n) \le (y_1, ..., y_n)$ if $x_i \le y_i$ forall $i$.

I'd like to find all minimal solutions to these systems efficiently. I can reduce them to SAT by treating $=$ as $\leftrightarrow$ and solving the corresponding sat problem but it seems like this might be a subset that is more efficiently solvable.

Is there an efficient algorithm to solve this problem? Does it belong to some efficiently solvable subset of SAT? is it close to an efficiently solvable subset?

• Your clauses of type (1) can be converted to Horn clauses: convert $a = b \lor c$ to $(b \lor c) \implies a$. After this conversion, the system has the same set of minimal solutions. The minimal solution to a set of Horn clauses can be computed in polynomial time. I don't know how to handle the type-(2) clauses, though. – D.W. Jul 24 '16 at 1:35
• There is no hope for a polynomial-time algorithm to solve this problem, because there can be exponentially many minimal solutions. For instance, imagine the equations are $x_1 \lor x_2 = 1$, $x_3 \lor x_4 = 1$, $x_5 \lor x_6 = 1$, .., $x_{2n-1} \lor x_{2n} = 1$. Then there are $2^n$ minimal solutions. Do you want to edit your question to ask for an output-sensitive algorithm, where the running time is polynomial in the number of minimal solutions? Or do you want me to post this as an answer? – D.W. Jul 24 '16 at 1:37
• So I think I need help finding the correct notion of "efficiency" here then. Given what you've pointed out this clearly can't be done efficiently in the formal since. Basically I want do this asymptotically faster than I would with SAT solving. I know how to do this with SAT solving and how to avoid searching for non-minimal solutions while doing that. Unfortunately it might still take exponential time to find each of those minimal solutions. I'm basically want to know what the asymptotic best time we can get is. – Jake Jul 24 '16 at 2:15
• We might need more information about what you're trying to achieve, to help you formulate a useful variant of this question. Maybe you have a special case. What my example shows is that there exists systems of equations where you basically can't really do better than SAT solving if you want to list all minimal solutions (since you'll have to do exponential work if you want to list them all). That doesn't rule out the possibility that there might be more efficient solutions for systems that have only a few minimal solutions, or only a few type-(2) constraints, or in other special cases. – D.W. Jul 24 '16 at 2:18
• The problem I'm trying to solve has a very simple and direct one to one correspondence unfortunately. I do expect that the systems I'll be solving will tend to have very few minimal solutions but in general that's not true. I can think of a problem that gives exactly the case above that you mentioned. There will also be lots of both kinds of equations, half the time there will be fewer type 1 and half the time there will be fewer type 2. For reference the problem I'm solving is ACUI E-unification with constants. Another step that I have to perform breaks the equations down to this form. – Jake Jul 24 '16 at 2:44