|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
public interface SearchListener
Interface to the solver main steps. Useful for integrating search visualization or debugging. (that class moved from org.sat4j.minisat.core in earlier version of SAT4J).
Method Summary | |
---|---|
void |
adding(int p)
adding forced variable (conflict driven assignment) |
void |
assuming(int p)
decision variable |
void |
backjump(int backjumpLevel)
The solver is asked to backjump to a given decision level. |
void |
backtracking(int p)
backtrack on a decision variable |
void |
beginLoop()
starts a propagation |
void |
conflictFound(IConstr confl,
int dlevel,
int trailLevel)
a conflict has been found. |
void |
conflictFound(int p)
a conflict has been found while propagating values. |
void |
delete(int[] clause)
delete a clause |
void |
end(Lbool result)
End the search. |
void |
learn(IConstr c)
learning a new clause |
void |
propagating(int p,
IConstr reason)
Unit propagation |
void |
restarting()
The solver restarts the search. |
void |
solutionFound()
a solution is found. |
void |
start()
Start the search. |
Method Detail |
---|
void assuming(int p)
p
- void propagating(int p, IConstr reason)
p
- reason
- TODOvoid backtracking(int p)
p
- void adding(int p)
void learn(IConstr c)
c
- void delete(int[] clause)
void conflictFound(IConstr confl, int dlevel, int trailLevel)
confl
- TODOdlevel
- TODOtrailLevel
- TODOvoid conflictFound(int p)
p
- the conflicting value.void solutionFound()
void beginLoop()
void start()
void end(Lbool result)
result
- the result of the search.void restarting()
void backjump(int backjumpLevel)
backjumpLevel
-
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |