|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object org.sat4j.minisat.core.Solver
public class Solver
Field Summary | |
---|---|
static org.sat4j.minisat.core.Solver.ISimplifier |
NO_SIMPLIFICATION
|
org.sat4j.minisat.core.Solver.ISimplifier |
SIMPLE_SIMPLIFICATION
|
Constructor Summary | |
---|---|
Solver(AssertingClauseGenerator acg,
LearningStrategy learner,
DataStructureFactory dsf,
IOrder order)
creates a Solver without LearningListener. |
|
Solver(AssertingClauseGenerator acg,
LearningStrategy learner,
DataStructureFactory dsf,
SearchParams params,
IOrder order)
|
Method Summary | |
---|---|
void |
addAllClauses(IVec<IVecInt> clauses)
Create clauses from a set of set of literals. |
IConstr |
addAtLeast(IVecInt literals,
int degree)
Create a cardinality constraint of the type "at least n of those literals must be satisfied" |
IConstr |
addAtMost(IVecInt literals,
int degree)
Create a cardinality constraint of the type "at most n of those literals must be satisfied" |
IConstr |
addClause(IVecInt literals)
Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values. |
IConstr |
addPseudoBoolean(IVecInt literals,
IVec<java.math.BigInteger> coeffs,
boolean moreThan,
java.math.BigInteger degree)
Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied" |
int |
analyze(Constr confl,
Handle<Constr> outLearntRef)
|
boolean |
assume(int p)
|
void |
claBumpActivity(Constr confl)
Propagate activity to a constraint |
int |
decisionLevel()
|
static int |
decode2dimacs(int p)
decode the internal representation of a literal into Dimacs format. |
boolean |
enqueue(int p)
Satisfait un litt? |
boolean |
enqueue(int p,
Constr from)
Put the literal on the queue of assignments to be done. |
DataStructureFactory |
getDSFactory()
|
IConstr |
getIthConstr(int i)
returns the ith constraint in the solver. |
IOrder |
getOrder()
|
IVecInt |
getOutLearnt()
|
java.util.Map<java.lang.String,java.lang.Number> |
getStat()
To obtain a map of the available statistics from the solver. |
SolverStats |
getStats()
|
int |
getTimeout()
Useful to check the internal timeout of the solver. |
ILits |
getVocabulary()
|
boolean |
isSatisfiable()
Check the satisfiability of the set of constraints contained inside the solver. |
boolean |
isSatisfiable(IVecInt assumps)
Check the satisfiability of the set of constraints contained inside the solver. |
void |
learn(Constr c)
|
int[] |
model()
Si un mod? |
boolean |
model(int var)
Provide the truth value of a specific variable in the model. |
int |
nConstraints()
To know the number of constraints currently available in the solver. |
int |
newVar()
Create a new variable in the solver (and thus in the vocabulary). |
int |
newVar(int howmany)
Create howmany variables in the solver (and thus in the
vocabulary). |
int |
nVars()
To know the number of variables used in the solver. |
void |
printStat(java.io.PrintStream out,
java.lang.String prefix)
Display statistics to the given output stream Please use writers instead of stream. |
void |
printStat(java.io.PrintWriter out,
java.lang.String prefix)
Display statistics to the given output writer |
Constr |
propagate()
|
boolean |
removeConstr(IConstr co)
Remove a constraint returned by one of the add method from the solver. |
void |
reset()
Clean up the internal state of the solver. |
void |
setDataStructureFactory(DataStructureFactory dsf)
Change the internatal representation of the contraints. |
void |
setExpectedNumberOfClauses(int nb)
To inform the solver of the expected number of clauses to read. |
void |
setOrder(IOrder h)
|
void |
setSearchListener(SearchListener sl)
|
void |
setSimplifier(org.sat4j.minisat.core.Solver.ISimplifier simp)
|
void |
setTimeout(int t)
To set the internal timeout of the solver. |
boolean |
simplifyDB()
|
java.lang.String |
toString()
|
java.lang.String |
toString(java.lang.String prefix)
Display a textual representation of the solver configuration. |
void |
varBumpActivity(int p)
Update the activity of a variable v. |
Methods inherited from class java.lang.Object |
---|
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait |
Field Detail |
---|
public static final org.sat4j.minisat.core.Solver.ISimplifier NO_SIMPLIFICATION
public final org.sat4j.minisat.core.Solver.ISimplifier SIMPLE_SIMPLIFICATION
Constructor Detail |
---|
public Solver(AssertingClauseGenerator acg, LearningStrategy learner, DataStructureFactory dsf, IOrder order)
acg
- an asserting clause generatorpublic Solver(AssertingClauseGenerator acg, LearningStrategy learner, DataStructureFactory dsf, SearchParams params, IOrder order)
Method Detail |
---|
public void setDataStructureFactory(DataStructureFactory dsf)
dsf
- the internal factorypublic void setSearchListener(SearchListener sl)
public void setTimeout(int t)
ISolver
setTimeout
in interface ISolver
t
- the timeout (in s)public int nConstraints()
IProblem
nConstraints
in interface IProblem
public void learn(Constr c)
learn
in interface Learner
public int decisionLevel()
public int newVar()
ISolver
newVar
in interface ISolver
public int newVar(int howmany)
ISolver
howmany
variables in the solver (and thus in the
vocabulary).
newVar
in interface ISolver
howmany
- number of variables to create
public IConstr addClause(IVecInt literals) throws ContradictionException
ISolver
addClause
in interface ISolver
literals
- a set of literals
ContradictionException
- iff the vector of literals is empty or if it contains
only falsified literals after unit propagationISolver.removeConstr(IConstr)
public boolean removeConstr(IConstr co)
ISolver
removeConstr
in interface ISolver
co
- a constraint returned by one of the add method.
public IConstr addPseudoBoolean(IVecInt literals, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger degree) throws ContradictionException
ISolver
addPseudoBoolean
in interface ISolver
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 >= 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 void addAllClauses(IVec<IVecInt> clauses) throws ContradictionException
ISolver
addAllClauses
in interface ISolver
clauses
- a vector of set (VecInt) of literals in the dimacs format.
The vector can be reused since the solver is not supposed
to keep a reference to that vector.
ContradictionException
- iff the vector of literals is empty or if it contains
only falsified literals after unit propagationISolver.addClause(IVecInt)
public IConstr addAtMost(IVecInt literals, int degree) throws ContradictionException
ISolver
addAtMost
in interface ISolver
literals
- a set of literals
The vector can be reused since the solver is not supposed
to keep a reference to that vector.degree
- the degree of the cardinality constraint
ContradictionException
- iff the vector of literals is empty or if it contains
more than degree satisfied literals after unit propagationISolver.removeConstr(IConstr)
public IConstr addAtLeast(IVecInt literals, int degree) throws ContradictionException
ISolver
addAtLeast
in interface ISolver
literals
- a set of literals.
The vector can be reused since the solver is not supposed
to keep a reference to that vector.degree
- the degree of the cardinality constraint
ContradictionException
- iff the vector of literals is empty or if degree literals are not
remaining unfalsified after unit propagationISolver.removeConstr(IConstr)
public boolean simplifyDB()
public int[] model()
model
in interface IProblem
public boolean enqueue(int p)
enqueue
in interface UnitPropagationListener
p
- le litt?ral
public boolean enqueue(int p, Constr from)
enqueue
in interface UnitPropagationListener
p
- the literal.from
- the reason to propagate that literal, else null
public int analyze(Constr confl, Handle<Constr> outLearntRef)
public void setSimplifier(org.sat4j.minisat.core.Solver.ISimplifier simp)
public static int decode2dimacs(int p)
p
- the literal in internal representation
public void claBumpActivity(Constr confl)
confl
- a constraintpublic void varBumpActivity(int p)
VarActivityListener
p
- a literal (v<<1 or v<<1^1)public Constr propagate()
public boolean assume(int p)
public boolean model(int var)
IProblem
model
in interface IProblem
var
- the variable id in Dimacs format
public boolean isSatisfiable() throws TimeoutException
IProblem
isSatisfiable
in interface IProblem
TimeoutException
public boolean isSatisfiable(IVecInt assumps) throws TimeoutException
IProblem
isSatisfiable
in interface IProblem
assumps
- a set of literals (represented by usual non null integers in
Dimacs format).
TimeoutException
public SolverStats getStats()
public IOrder getOrder()
public void setOrder(IOrder h)
public ILits getVocabulary()
public void reset()
ISolver
reset
in interface ISolver
public int nVars()
IProblem
nVars
in interface IProblem
public DataStructureFactory getDSFactory()
public IVecInt getOutLearnt()
public IConstr getIthConstr(int i)
i
- the constraint number (begins at 0)
public void printStat(java.io.PrintStream out, java.lang.String prefix)
ISolver
printStat
in interface ISolver
prefix
- the prefix to put in front of each lineISolver.printStat(PrintWriter, String)
public void printStat(java.io.PrintWriter out, java.lang.String prefix)
ISolver
printStat
in interface ISolver
prefix
- the prefix to put in front of each linepublic java.lang.String toString(java.lang.String prefix)
ISolver
toString
in interface ISolver
prefix
- the prefix to use on each line.
public java.lang.String toString()
toString
in class java.lang.Object
public int getTimeout()
ISolver
getTimeout
in interface ISolver
public void setExpectedNumberOfClauses(int nb)
ISolver
p cnf
line is read in dimacs formatted input file.
setExpectedNumberOfClauses
in interface ISolver
nb
- the expected number of clauses.public java.util.Map<java.lang.String,java.lang.Number> getStat()
ISolver
getStat
in interface ISolver
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |