org.sat4j.tools

Class RupSearchListener<S extends ISolverService>

java.lang.Object

org.sat4j.tools.SearchListenerAdapter<S>

org.sat4j.tools.RupSearchListener<S>

Type Parameters:

S - a solver service

All Implemented Interfaces:

java.io.Serializable, SearchListener<S>

public class RupSearchListener<S extends ISolverService>
extends SearchListenerAdapter<S>

Output an unsat proof using the reverse unit propagation (RUP) format.

Since:

2.3.4

Author:

daniel

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
RupSearchListener(java.lang.String filename)

Method Summary

Modifier and Type	Method and Description
void	end(Lbool result) End the search.
void	init(S solverService) Provide access to the solver's controllable interface.
void	learn(IConstr c) learning a new clause
void	learnUnit(int p) learn a new unit clause (a literal)

Methods inherited from class org.sat4j.tools.SearchListenerAdapter

adding, assuming, backjump, backtracking, beginLoop, cleaning, conflictFound, conflictFound, delete, propagating, restarting, solutionFound, start

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

RupSearchListener

public RupSearchListener(java.lang.String filename)

Method Detail

init

public void init(S solverService)

Description copied from interface: SearchListener

Provide access to the solver's controllable interface.

Specified by:

init in interface SearchListener<S extends ISolverService>

Overrides:

init in class SearchListenerAdapter<S extends ISolverService>

Parameters:

solverService - a way to safely control the solver.

end

public void end(Lbool result)

Description copied from interface: SearchListener

End the search.

Specified by:

end in interface SearchListener<S extends ISolverService>

Overrides:

end in class SearchListenerAdapter<S extends ISolverService>

Parameters:

result - the result of the search.

learn

public void learn(IConstr c)

Description copied from interface: SearchListener

learning a new clause

Specified by:

learn in interface SearchListener<S extends ISolverService>

Overrides:

learn in class SearchListenerAdapter<S extends ISolverService>

learnUnit

public void learnUnit(int p)

Description copied from interface: SearchListener

learn a new unit clause (a literal)

Specified by:

learnUnit in interface SearchListener<S extends ISolverService>

Overrides:

learnUnit in class SearchListenerAdapter<S extends ISolverService>

Parameters:

p - a literal in Dimacs format.