PicoSAT Solver#

This solver relies on the pycosat Python bindings to PicoSAT.

The pycosat package should be installed on your Sage installation.

AUTHORS:

  • Thierry Monteil (2018): initial version.

class sage.sat.solvers.picosat.PicoSAT(verbosity=0, prop_limit=0)[source]#

Bases: SatSolver

PicoSAT Solver.

INPUT:

  • verbosity – an integer between 0 and 2 (default: 0); verbosity

  • prop_limit – an integer (default: 0); the propagation limit

EXAMPLES:

sage: from sage.sat.solvers.picosat import PicoSAT
sage: solver = PicoSAT()                           # optional - pycosat

>>> from sage.all import *
>>> from sage.sat.solvers.picosat import PicoSAT
>>> solver = PicoSAT()                           # optional - pycosat
add_clause(lits)[source]#

Add a new clause to set of clauses.

INPUT:

  • lits – a tuple of nonzero integers

Note

If any element e in lits has abs(e) greater than the number of variables generated so far, then new variables are created automatically.

EXAMPLES:

sage: from sage.sat.solvers.picosat import PicoSAT
sage: solver = PicoSAT()                       # optional - pycosat
sage: solver.add_clause((1, -2 , 3))           # optional - pycosat

>>> from sage.all import *
>>> from sage.sat.solvers.picosat import PicoSAT
>>> solver = PicoSAT()                       # optional - pycosat
>>> solver.add_clause((Integer(1), -Integer(2) , Integer(3)))           # optional - pycosat
clauses(filename=None)[source]#

Return original clauses.

INPUT:

  • filename – (optional) if given, clauses are written to filename in DIMACS format

OUTPUT:

If filename is None then a list of lits is returned, where lits is a list of literals.

If filename points to a writable file, then the list of original clauses is written to that file in DIMACS format.

EXAMPLES:

sage: from sage.sat.solvers.picosat import PicoSAT
sage: solver = PicoSAT()                       # optional - pycosat
sage: solver.add_clause((1,2,3,4,5,6,7,8,-9))  # optional - pycosat
sage: solver.clauses()                         # optional - pycosat
[[1, 2, 3, 4, 5, 6, 7, 8, -9]]

>>> from sage.all import *
>>> from sage.sat.solvers.picosat import PicoSAT
>>> solver = PicoSAT()                       # optional - pycosat
>>> solver.add_clause((Integer(1),Integer(2),Integer(3),Integer(4),Integer(5),Integer(6),Integer(7),Integer(8),-Integer(9)))  # optional - pycosat
>>> solver.clauses()                         # optional - pycosat
[[1, 2, 3, 4, 5, 6, 7, 8, -9]]

DIMACS format output:

sage: # optional - pycosat
sage: from sage.sat.solvers.picosat import PicoSAT
sage: solver = PicoSAT()
sage: solver.add_clause((1, 2, 4))
sage: solver.add_clause((1, 2, -4))
sage: fn = tmp_filename()
sage: solver.clauses(fn)
sage: print(open(fn).read())
p cnf 4 2
1 2 4 0
1 2 -4 0

>>> from sage.all import *
>>> # optional - pycosat
>>> from sage.sat.solvers.picosat import PicoSAT
>>> solver = PicoSAT()
>>> solver.add_clause((Integer(1), Integer(2), Integer(4)))
>>> solver.add_clause((Integer(1), Integer(2), -Integer(4)))
>>> fn = tmp_filename()
>>> solver.clauses(fn)
>>> print(open(fn).read())
p cnf 4 2
1 2 4 0
1 2 -4 0
<BLANKLINE>
nvars()[source]#

Return the number of variables.

Note that for compatibility with DIMACS convention, the number of variables corresponds to the maximal index of the variables used.

EXAMPLES:

sage: from sage.sat.solvers.picosat import PicoSAT
sage: solver = PicoSAT()                       # optional - pycosat
sage: solver.nvars()                           # optional - pycosat
0

>>> from sage.all import *
>>> from sage.sat.solvers.picosat import PicoSAT
>>> solver = PicoSAT()                       # optional - pycosat
>>> solver.nvars()                           # optional - pycosat
0

If a variable with intermediate index is not used, it is still considered as a variable:

sage: solver.add_clause((1,-2,4))              # optional - pycosat
sage: solver.nvars()                           # optional - pycosat
4

>>> from sage.all import *
>>> solver.add_clause((Integer(1),-Integer(2),Integer(4)))              # optional - pycosat
>>> solver.nvars()                           # optional - pycosat
4
var(decision=None)[source]#

Return a new variable.

INPUT:

  • decision – ignored; accepted for compatibility with other solvers

EXAMPLES:

sage: from sage.sat.solvers.picosat import PicoSAT
sage: solver = PicoSAT()                       # optional - pycosat
sage: solver.var()                             # optional - pycosat
1

sage: solver.add_clause((-1,2,-4))             # optional - pycosat
sage: solver.var()                             # optional - pycosat
5

>>> from sage.all import *
>>> from sage.sat.solvers.picosat import PicoSAT
>>> solver = PicoSAT()                       # optional - pycosat
>>> solver.var()                             # optional - pycosat
1

>>> solver.add_clause((-Integer(1),Integer(2),-Integer(4)))             # optional - pycosat
>>> solver.var()                             # optional - pycosat
5