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 the BooleanExpression 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 from clauses applies here. Note that assumptions cannot be an empty list; leave it as None if there are no assumptions to include. An iterator of solutions; if no satisfiable solutions exist, the iterator will be empty. Iterator[List[int]] InvalidArgumentTypeError – If clauses is not a list of lists of ints or assumptions 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([, [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([, [2, 3, 4], [2, 3]],
...                                 assumptions=[-3]):
...     print(solution)
...
[1, 2, -3, 4]
[1, 2, -3, -4]
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 the BooleanExpression 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 from clauses applies here. Note that assumptions cannot be an empty list; leave it as None if there are no assumptions to include. If solution is found, a list of ints representing the terms of the solution; otherwise, if no solution found, None. List[int] or None InvalidArgumentTypeError – If clauses is not a list of lists of ints or assumptions 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]]) 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]