satisfiability

Functionality for determining logic satisfiasbility.

satisfiability.picosat module

Python wrapper around the _clibs PicoSAT extension.

tt.satisfiability.picosat.sat_all(clauses, assumptions=None)

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.

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 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([[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]

tt.satisfiability.picosat.sat_one(clauses, assumptions=None)

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.

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] or None

Raises:

• 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], [-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]