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)

Bases: sage.sat.solvers.satsolver.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
add_clause(lits)

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
clauses(filename=None)

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

DIMACS format output:

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

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

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
var(decision=None)

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