Source code for tt.satisfiability.picosat

"""Python wrapper around the _clibs PicoSAT extension."""

import os

from tt.errors.arguments import (

if os.environ.get('READTHEDOCS') != 'True':
    from tt._clibs import picosat as _c_picosat
    VERSION = _c_picosat.VERSION

[docs]def 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 :param clauses: CNF (AND of ORs) clauses; positive integers represent non-negated terms and negative integers represent negated terms. :type clauses: List[List[:class:`int <python:int>`]] :param assumptions: Assumed terms; same negation logic from ``clauses`` applies here. :type assumptions: List[:class:`int <python:int>`] :returns: If solution is found, a list of ints representing the terms of the solution; otherwise, if no solution found, ``None``. :rtype: List[:class:`int <python:int>`] or ``None`` :raises InvalidArgumentTypeError: If ``clauses`` is not a list of lists of ints or ``assumptions`` is not a list of ints. :raises InvalidArgumentValueError: If any literal ints are equal to zero. Example usage:: >>> from tt import picosat >>> # Return None when no solution possible ... picosat.sat_one([[1], [-1]]) is None True >>> # 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] """ try: return _c_picosat.sat_one(clauses, assumptions=assumptions) except TypeError as e: raise InvalidArgumentTypeError(str(e)) except ValueError as e: raise InvalidArgumentValueError(str(e))