org.sat4j.pb

Interface IPBSolver

All Superinterfaces:

IProblem, ISolver, RandomAccessModel, Serializable

All Known Subinterfaces:

IPBCDCLSolver<D>

All Known Implementing Classes:

ClausalConstraintsDecorator, ConstraintRelaxingPseudoOptDecorator, LexicoDecoratorPB, LPStringSolver, ManyCorePB, MinCostDecorator, ObjectiveReducerPBSolverDecorator, OPBStringSolver, OptToPBSATAdapter, PBAdapter, PBSolver, PBSolverCautious, PBSolverClause, PBSolverCP, PBSolverDecorator, PBSolverResCP, PBSolverResolution, PBSolverWithImpliedClause, PseudoBitsAdderDecorator, PseudoIteratorDecorator, PseudoOptDecorator, UserFriendlyPBStringSolver, WeightedMaxSatDecorator, XplainPB

public interface IPBSolver
extends ISolver

A solver able to deal with pseudo boolean constraints.

Author:

daniel

Method Summary

Methods

Modifier and Type	Method and Description
IConstr	addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree) Create a pseudo-boolean constraint of the type "at least".
IConstr	addAtLeast(IVecInt literals, IVecInt coeffs, int degree) Create a pseudo-boolean constraint of the type "at least".
IConstr	addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree) Create a pseudo boolean constraint of the type "at most".
IConstr	addAtMost(IVecInt literals, IVecInt coeffs, int degree) Create a pseudo boolean constraint of the type "at most".
IConstr	addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight) Create a pseudo-boolean constraint of the type "subset sum".
IConstr	addExactly(IVecInt literals, IVecInt coeffs, int weight) Create a pseudo-boolean constraint of the type "subset sum".
IConstr	addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d) Create a Pseudo-Boolean constraint of the type "at least n or at most n of those literals must be satisfied"
ObjectiveFunction	getObjectiveFunction() Retrieve the objective function from the solver.
void	setObjectiveFunction(ObjectiveFunction obj) Provide an objective function to the solver.

Methods inherited from interface org.sat4j.specs.ISolver

addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearLearntClauses, expireTimeout, getLogPrefix, getSearchListener, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSolverKeptHot, isVerbose, modelWithInternalVariables, newVar, nextFreeVarId, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, unsatExplanation

Methods inherited from interface org.sat4j.specs.IProblem

findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos, printInfos

Methods inherited from interface org.sat4j.specs.RandomAccessModel

model

Method Detail

addPseudoBoolean

IConstr addPseudoBoolean(IVecInt lits,
                       IVec<BigInteger> coeffs,
                       boolean moreThan,
                       BigInteger d)
                         throws ContradictionException

Create a Pseudo-Boolean constraint of the type "at least n or at most n of those literals must be satisfied"

Parameters:

lits - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

moreThan - true if it is a constraint >= degree, false if it is a constraint <= degree

d - the degree of the cardinality constraint

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the vector of literals is empty or if the constraint is falsified after unit propagation

See Also:

ISolver.removeConstr(IConstr)

addAtMost

IConstr addAtMost(IVecInt literals,
                IVecInt coeffs,
                int degree)
                  throws ContradictionException

Create a pseudo boolean constraint of the type "at most".

Parameters:

literals - a set of literals The vector can be reused since the solver is not supposed to keep a reference to that vector.

coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

degree - the degree of the pseudo-boolean constraint

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the constraint is found trivially unsat.

Since:

2.3.1

See Also:

ISolver.removeConstr(IConstr)

addAtMost

IConstr addAtMost(IVecInt literals,
                IVec<BigInteger> coeffs,
                BigInteger degree)
                  throws ContradictionException

Create a pseudo boolean constraint of the type "at most".

Parameters:

literals - a set of literals The vector can be reused since the solver is not supposed to keep a reference to that vector.

coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

degree - the degree of the pseudo-boolean constraint

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the constraint is found trivially unsat.

Since:

2.3.1

See Also:

ISolver.removeConstr(IConstr)

addAtLeast

IConstr addAtLeast(IVecInt literals,
                 IVecInt coeffs,
                 int degree)
                   throws ContradictionException

Create a pseudo-boolean constraint of the type "at least".

Parameters:

literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

degree - the degree of the pseudo-boolean constraint

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the constraint is found trivially unsat.

Since:

2.3.1

See Also:

ISolver.removeConstr(IConstr)

addAtLeast

IConstr addAtLeast(IVecInt literals,
                 IVec<BigInteger> coeffs,
                 BigInteger degree)
                   throws ContradictionException

Create a pseudo-boolean constraint of the type "at least".

Parameters:

literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

degree - the degree of the pseudo-boolean constraint

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the constraint is found trivially unsat.

Since:

2.3.1

See Also:

ISolver.removeConstr(IConstr)

addExactly

IConstr addExactly(IVecInt literals,
                 IVecInt coeffs,
                 int weight)
                   throws ContradictionException

Create a pseudo-boolean constraint of the type "subset sum".

Parameters:

literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

weight - the number of literals that must be satisfied

Returns:

a reference to the constraint added to the solver. It might return an object representing a group of constraints.

Throws:

ContradictionException - iff the constraint is trivially unsatisfiable.

Since:

2.3.1

addExactly

IConstr addExactly(IVecInt literals,
                 IVec<BigInteger> coeffs,
                 BigInteger weight)
                   throws ContradictionException

Create a pseudo-boolean constraint of the type "subset sum".

Parameters:

literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

weight - the number of literals that must be satisfied

Returns:

a reference to the constraint added to the solver. It might return an object representing a group of constraints.

Throws:

ContradictionException - iff the constraint is trivially unsatisfiable.

Since:

2.3.1

setObjectiveFunction

void setObjectiveFunction(ObjectiveFunction obj)

Provide an objective function to the solver.

Parameters:

obj - the objective function

getObjectiveFunction

ObjectiveFunction getObjectiveFunction()

Retrieve the objective function from the solver.

Returns:

the objective function