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

tt.satisfiability.picosat.
sat_all
(clauses, assumptions=None)[source]¶ Find all solutions that satisfy 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 interface provided through the
sat_all
method in theBooleanExpression
class.Parameters:  clauses (List[List[
int
]]) – CNF (AND of ORs) clauses; positive integers represent nonnegated terms and negative integers represent negated terms.  assumptions (List[
int
]) – Assumed terms; same negation logic fromclauses
applies here. Note that assumptions cannot be an empty list; leave it asNone
if there are no assumptions to include.
Returns: An iterator of solutions; if no satisfiable solutions exist, the iterator will be empty.
Return type: Iterator[List[
int
]]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.
Here’s an example showing the basic usage:
>>> from tt import picosat >>> for solution in picosat.sat_all([[1], [2, 3, 4], [2, 3]]): ... print(solution) ... [1, 2, 3, 4] [1, 2, 3, 4] [1, 2, 3, 4] [1, 2, 3, 4] [1, 2, 3, 4] [1, 2, 3, 4]
We can cut down on some of the above solutions by including an assumption:
>>> for solution in picosat.sat_all([[1], [2, 3, 4], [2, 3]], ... assumptions=[3]): ... print(solution) ... [1, 2, 3, 4] [1, 2, 3, 4]
 clauses (List[List[

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 interface provided through the
sat_one
method in theBooleanExpression
class.Parameters:  clauses (List[List[
int
]]) – CNF (AND of ORs) clauses; positive integers represent nonnegated terms and negative integers represent negated terms.  assumptions (List[
int
]) – Assumed terms; same negation logic fromclauses
applies here. Note that assumptions cannot be an empty list; leave it asNone
if there are no assumptions to include.
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.
Let’s look at a simple example with no satisfiable solution:
>>> from tt import picosat >>> picosat.sat_one([[1], [1]]) is None True
Here’s an example where a solution exists:
>>> picosat.sat_one([[1, 2, 3], [2, 3], [1, 2], [2, 3], [2]]) [1, 2, 3]
Finally, here’s an example using assumptions:
>>> picosat.sat_one([[1, 2, 3], [2, 3]], assumptions=[1, 3]) [1, 2, 3]
 clauses (List[List[