|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object org.sat4j.minisat.core.Solver<PBDataStructureFactory> org.sat4j.pb.core.PBSolver org.sat4j.pb.core.PBSolverCP org.sat4j.pb.core.PBSolverWithImpliedClause
public class PBSolverWithImpliedClause
Field Summary |
---|
Fields inherited from class org.sat4j.pb.core.PBSolver |
---|
objectiveFunctionBased, stats |
Fields inherited from class org.sat4j.minisat.core.Solver |
---|
constrs, dsfactory, EXPENSIVE_SIMPLIFICATION, EXPENSIVE_SIMPLIFICATION_WLONLY, glucose, learnedConstraintsDeletionStrategy, learnts, memory_based, NO_SIMPLIFICATION, out, rootLevel, SIMPLE_SIMPLIFICATION, slistener, trail, trailLim, undertimeout, voc |
Constructor Summary | |
---|---|
PBSolverWithImpliedClause(LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf,
IOrder order)
|
Method Summary | |
---|---|
IConstr |
addPseudoBoolean(IVecInt literals,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger degree)
Create a Pseudo-Boolean constraint of the type "at least n or at most n of those literals must be satisfied" |
void |
claBumpActivity(Constr confl)
|
String |
toString(String prefix)
Display a textual representation of the solver configuration. |
Methods inherited from class org.sat4j.pb.core.PBSolverCP |
---|
analyze, analyzeCP, updateNumberOfReducedLearnedConstraints, updateNumberOfReductions |
Methods inherited from class org.sat4j.pb.core.PBSolver |
---|
addAtLeast, addAtLeast, addAtMost, addAtMost, addExactly, addExactly, getObjectiveFunction, setObjectiveFunction |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait |
Methods inherited from interface org.sat4j.minisat.core.ICDCL |
---|
getLogger, getOrder, getRestartStrategy, getSimplifier, setDataStructureFactory, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearner, setLogger, setNeedToReduceDB, setOrder, setRestartStrategy, setSearchParams, setSimplifier, setSimplifier |
Methods inherited from interface org.sat4j.specs.IProblem |
---|
findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, model, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos |
Methods inherited from interface org.sat4j.minisat.core.UnitPropagationListener |
---|
enqueue, enqueue, unset |
Methods inherited from interface org.sat4j.minisat.core.VarActivityListener |
---|
varBumpActivity |
Methods inherited from interface org.sat4j.minisat.core.Learner |
---|
learn |
Constructor Detail |
---|
public PBSolverWithImpliedClause(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)
Method Detail |
---|
public IConstr addPseudoBoolean(IVecInt literals, IVec<BigInteger> coeffs, boolean moreThan, BigInteger degree) throws ContradictionException
IPBSolver
addPseudoBoolean
in interface IPBSolver
addPseudoBoolean
in class PBSolver
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.moreThan
- true if it is a constraint >= degree, false if it is a
constraint <= degreedegree
- the degree of the cardinality constraint
ContradictionException
- iff the vector of literals is empty or if the constraint is
falsified after unit propagationISolver.removeConstr(IConstr)
public String toString(String prefix)
ISolver
toString
in interface ISolver
toString
in class PBSolverCP
prefix
- the prefix to use on each line.
public void claBumpActivity(Constr confl)
outclause
-
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |