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); verbosityprop_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
inlits
hasabs(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 tofilename
in DIMACS format
OUTPUT:
If
filename
isNone
then a list oflits
is returned, wherelits
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