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 C-extension. 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 non-negated 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 C-extension. 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 non-negated 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[