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 to None, the default one is used. For more information on LP solvers and which default solver is used, see the method solve() of the class MixedIntegerLinearProgram.

  • 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 in lits has abs(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