Solving Symbolic Boolean variables in Python

Question

I need to solve a set of symbolic Boolean expressions like:

>>> solve(x | y = False)
(False, False)

>>> solve(x & y = True)
(True, True)

>>> solve (x & y & z = True)
(True, True, True)

>>> solve(x ^ y = False)
((False, False), (True, True))

Number of such variables is large (~200) so that Brute Force strategy is not possible. I searched the web and found that Sympy and Sage have symbolic manipulation capabilities (particularly this and this may be useful). How can I do that?

EDIT: I mainly tried to manipulate such things:

>>> from sympy import *

>>> x=Symbol('x', bool=True)

>>> y=Symbol('y', bool=True)

>>> solve(x & y, x)

which results in NotImplementedError. Then I tried solve(x * y, x) which gave [0] (I don't know what does it mean), solve(x * y = True, x) resulted in a SyntaxError, solve(x * y, True, x) and solve(x & y, True, x) gave an AttributeError. I don't know what else to try!

EDIT (2): I also found this, may be useful!

Answer 1

First, to correct a few things that are just blatently wrong in your question:

• solve solves for algebraic expressions. solve(expr, x) solves the equation expr = 0 for x.

• solve(x | y = False) and so on are invalid syntax. You cannot use = to mean equality in Python. See http://docs.sympy.org/latest/tutorial/gotchas.html#equals-signs (and I recommend reading the rest of that tutorial as well).

• As I mentioned in the answer to another question, Symbol('y', bool=True) does nothing. Symbol('x', something=True) sets the is_something assumption on x, but bool is not a recognized assumption by any part of SymPy. Just use regular Symbol('x') for boolean expressions.

As some commenters noted, what you want is satisfiable, which implements a SAT solver. satisfiable(expr) tells you if expr is satisfiable, that is, if there are values for the variables in expr that make it true. If it is satisfiable, it returns a mapping of such values (called a "model"). If no such mapping exists, i.e., expr is a contradiction, it returns False.

Therefore, satisfiable(expr) is the same as solving for expr = True. If you want to solve for expr = False, you should use satisfiable(~expr) (~ in SymPy means not).

In [5]: satisfiable(x & y)
Out[5]: {x: True, y: True}

In [6]: satisfiable(~(x | y))
Out[6]: {x: False, y: False}

In [7]: satisfiable(x & y & z)
Out[7]: {x: True, y: True, z: True}

Finally, note that satisfiable only returns one solution, because in general this is all you want, whereas finding all the solutions in general is extremely expensive, as there could be as many as 2**n of them, where n is the number of variables in your expression.

If however, you want to find all of them, the usual trick is to append your original expression with ~E, where E is the conjunction of the previous solution. So for example,

In [8]: satisfiable(x ^ y)
Out[8]: {x: True, y: False}

In [9]: satisfiable((x ^ y) & ~(x & ~y))
Out[9]: {x: False, y: True}

The & ~(x & ~y) means that you don't want a solution where x is true and y is false (think of & as adding extra conditions on your solution). Iterating this way, you can generate all solutions.