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 C-extension. 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