satisfiability
¶
Functionality for determining logic satisfiasbility.
satisfiability.picosat
module¶
Python wrapper around the _clibs PicoSAT extension.

tt.satisfiability.picosat.
sat_one
(clauses, assumptions=None)[source]¶ Find a solution that satisfies the specified clauses and assumptions.
This provides a light Python wrapper around the same method in the PicoSAT Cextension. While completely tested and usable, this method is probably not as useful as the
Parameters: Returns: If solution is found, a list of ints representing the terms of the solution; otherwise, if no solution found,
None
.Return type: List[
int
] orNone
Raises:  InvalidArgumentTypeError – If
clauses
is not a list of lists of ints orassumptions
is not a list of ints.  InvalidArgumentValueError – If any literal ints are equal to zero.
Example usage:
>>> from tt import picosat >>> # Return None when no solution possible ... picosat.sat_one([[1], [1]]) is None True >>> # Compute a satisfying solution ... picosat.sat_one([[1, 2, 3], [2, 3], [3]]) [1, 2, 3] >>> # Include assumptions ... picosat.sat_one([[1, 2, 3], [2, 3]], assumptions=[3]) [1, 2, 3]
 InvalidArgumentTypeError – If