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)¶ Bases:
sage.sat.solvers.satsolver.SatSolver
Initializes the instance
INPUT:
solver
– (default:None
) Specify a Linear Program (LP) solver to be used. If set toNone
, the default one is used. For more information on LP 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.
EXAMPLES:
sage: S=SAT(solver="LP"); S an ILP-based SAT Solver
-
add_clause
(lits)¶ Add a new clause to set of clauses.
INPUT:
lits
- a tuple of integers != 0
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(labels=False): ....: u,v = u+1,v+1 ....: S.add_clause((u,v)) ....: S.add_clause((-u,-v))
-
nvars
()¶ Return the number of variables.
EXAMPLES:
sage: S=SAT(solver="LP"); S an ILP-based SAT Solver sage: S.var() 1 sage: S.var() 2 sage: S.nvars() 2
-
var
()¶ Return a new variable.
EXAMPLES:
sage: S=SAT(solver="LP"); S an ILP-based SAT Solver sage: S.var() 1