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, verbose=None, integrality_tolerance=0)

Bases: sage.sat.solvers.satsolver.SatSolver

Initializes the instance

INPUT:

  • solver – (default: None) Specify a Mixed Integer Linear Programming (MILP) solver to be used. If set to None, the default one is used. For more information on MILP 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.

  • integrality_tolerance – parameter for use with MILP solvers over an inexact base ring; see MixedIntegerLinearProgram.get_values().

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