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](http://sympy.org/en/index.html) and
[Sage](http://www.sagemath.org/index.html) have symbolic manipulation
capabilities (particularly
[this](http://www.sagemath.org/doc/reference/logic/sage/logic/booleval.html)
and
[this](http://www.sagemath.org/doc/reference/polynomial_rings/sage/rings/polynomial/pbori.html)
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](ftp://ftp.iitb.ac.in/packages/sagemath/doc/en/reference/sat/sat.pdf),
may be useful!


Answer: 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](http://stackoverflow.com/questions/19703284/boolean-operation-with-symbol-in-sympy) 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.

