I have a set of expressions $E_1 .. E_n$ over boolean variables and I'm looking for an assignment to the variables so that all expressions are satisfied. Normally this would be NP-complete, but I found two particular properties over the set and I'm looking to combine and exploit them.
The idea I have is based on gaussian matrix elimination. In matrix elimination, you take a nonzero column and a row and use them to sweep the column from all other rows. Even for an integer matrix solution, you can find a solution in such a way if the number of rows is about the same as the number of columns and the matrix has exactly 1 solution. In my particular application, I have about as many variables as expressions and in some cases there is only 1 solution and the expressions do not imply each other. (property 1).
I take $E_1$ and one of it's variables. I combine $E_1$ with $E_2$ only if $E_2$ contains that variable. If so, I eliminate the variable from $E_2$ and I will (deterministically but somewhat arbitrarily) eliminate some more variables from $E_2$ that are both in $E_1$ and $E_2$. I keep the expressions as a truth table. Suppose for example that I want to eliminate a, b and c, $E_2$ would become
E_2 = (substitute/a,b,c/0,0,0 (E_1 && E_2)) || (substitute/a,b,c/0,0,1 (E_1 && E_2)) || (substitute/a,b,c/0,1,0 (E_1 && E_2)) || ... (substitute/a,b,c/1,1,1 (E_1 && E_2))
$E_2$ may take over some new variables from $E_1$. I would then combine $E_1$ and $E_3$ in the same way until $E_1$ with $E_n$ and then I'd start with $E_2$ with $E_3$ .. $E_n$ etc. at the end, $E_n$ will be an expression in a single variable. Normally this can lead to an exponential blowup for the size of an expression, but in my particular application, I found that because of variables are eliminated, $E_i$ && $E_k$ never has more than 39 variables (Property 2). Truth tables in 39 variables are still feasible.
Unfortunately, unlike matrix gaussian sweep, when substituting the variables, I lose information. For example, if $E_1 = a \rightarrow b$ and $E_2 = b \rightarrow c$ and I'm sweeping with $E_1:b$. $E_2$ would become $E_2 = a \rightarrow c$. Before the sweep, $a,b,c = 0,1,0$ was not a valid assignment, while after the sweep it is valid.
I'm not sure if this limitation can be overcome. Perhaps I should remember the original $E_2 = b \rightarrow c$ in a side-set of expressions, but then how to combine all the expressions in the side set? Or can I perhaps add $c$ to $E_1$, but then Property 2 won't hold anymore? Is there some 3rd property I should look for in my set of expressions, so that this method would work?
Truth table example
The truth table for $E_1 = a \rightarrow b$ (used above) is:
E_1 = ------------- |a|b|allowed| ------------- |0|0| 1 | |0|1| 1 | |1|0| 0 | |1|1| 1 | -------------
A truth table can express any boolean expression (or function) and the size is exponential in the number of variables.