Solve SAT problems Integer Linear Programming¶
The class defined here is a SatSolver
that
solves its instance using MixedIntegerLinearProgram
. Its performance
can be expected to be slower than when using
CryptoMiniSat
.
- class sage.sat.solvers.sat_lp.SatLP(solver=None, verbose=0, *, integrality_tolerance=0.001)[source]¶
Bases:
SatSolver
Initialize the instance.
INPUT:
solver
– (default:None
) specify a Mixed Integer Linear Programming (MILP) solver to be used. If set toNone
, the default one is used. For more information on MILP solvers and which default solver is used, see the methodsolve
of the classMixedIntegerLinearProgram
.verbose
– integer (default: 0); sets the level of verbosity of the LP solver. Set to 0 by default, which means quiet.integrality_tolerance
– parameter for use with MILP solvers over an inexact base ring; seeMixedIntegerLinearProgram.get_values()
EXAMPLES:
sage: S=SAT(solver='LP'); S an ILP-based SAT Solver
>>> from sage.all import * >>> S=SAT(solver='LP'); S an ILP-based SAT Solver
- add_clause(lits)[source]¶
Add a new clause to set of clauses.
INPUT:
lits
– 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: S=SAT(solver='LP'); S an ILP-based SAT Solver sage: for u,v in graphs.CycleGraph(6).edges(sort=False, labels=False): ....: u,v = u+1,v+1 ....: S.add_clause((u,v)) ....: S.add_clause((-u,-v))
>>> from sage.all import * >>> S=SAT(solver='LP'); S an ILP-based SAT Solver >>> for u,v in graphs.CycleGraph(Integer(6)).edges(sort=False, labels=False): ... u,v = u+Integer(1),v+Integer(1) ... S.add_clause((u,v)) ... S.add_clause((-u,-v))