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

  • 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.

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


Example usage:

>>> from tt import picosat
>>> # Return None when no solution possible
... picosat.sat_one([[1], [-1]]) is None
>>> # 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]