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!

Hardhearted

And what is wrong with the solutions you found? What have you tried? We must not do your evaluation work. – Thymelaeaceous

OK, I found this stating use of Boolean variables, but solution of equations are found here, but how to connect this two? solve assumes that RHS is 0, but here how can I put True or False? – Hardhearted

I think you want to use satisfiable not solve for boolean expressions as per this link. – Taciturnity

@Taciturnity this link is better. 0.6.7 is a very old version of SymPy. – Stem

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.

Stem

And if satisfiable ends up being too slow for you, check out other SAT solvers which are written in C. picosat for instance may be useful. It will require you to formulate your problem in a more rudimentary way (so-called DIMACS cnf form), but such solvers will return a solution almost instantly even for quite large problems. – Stem

And I should mention that picosat has Python bindings, called pycosat. – Stem

Great! One thing I would like to add, I found that only one solution is sufficient for my purpose. – Hardhearted

Good thing. Otherwise, it might take a very long time to solve your problem. – Stem

Surprisingly, satisfiable doesn't always solve for all of the variables. satisfiable(Eq(3*A-B,7) & Eq(2*A+3*B,1)) gives {Eq(2*A + 3*B, 1): True, Eq(3*A - B, 7): True}, but it doesn't solve for A and B. – Icily

@AndersonGreen satisfiable only does boolean satisfiability. It isn't an SMT solver. If you want to solve equations, use solve. – Stem

Answer 2

I think I got it (though use of it is still unclear).

Hardhearted