org.sat4j.minisat.uip
Class DecisionUIP

java.lang.Object
  org.sat4j.minisat.uip.DecisionUIP

All Implemented Interfaces:

Serializable, AssertingClauseGenerator

public final class DecisionUIP
extends Object
implements AssertingClauseGenerator, Serializable

Decision UIP scheme for building an asserting clause. This is one of the simplest way to build an asserting clause: the generator stops when it meets a decision variable (a literal with no reason). Note that this scheme cannot be used for general constraints, since decision variables are not necessarily UIP in the pseudo boolean case.

Author:

leberre

See Also:

Serialized Form

Constructor Summary

DecisionUIP()

Method Summary

boolean	clauseNonAssertive(IConstr reason) method indicating if an asserting clause has been built. note that this method is called right after a resolution step is finished.
void	initAnalyze() hook method called before the analysis.
void	onCurrentDecisionLevelLiteral(int p) hook method called when a literal from the current decision lelvel is found.
String	toString()

Methods inherited from class java.lang.Object

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

Constructor Detail

DecisionUIP

public DecisionUIP()

Method Detail

initAnalyze

public void initAnalyze()

Description copied from interface: AssertingClauseGenerator

hook method called before the analysis.

Specified by:

initAnalyze in interface AssertingClauseGenerator

onCurrentDecisionLevelLiteral

public void onCurrentDecisionLevelLiteral(int p)

Description copied from interface: AssertingClauseGenerator

hook method called when a literal from the current decision lelvel is found.

Specified by:

onCurrentDecisionLevelLiteral in interface AssertingClauseGenerator

Parameters:

p - the literal in the current decision level

clauseNonAssertive

public boolean clauseNonAssertive(IConstr reason)

Description copied from interface: AssertingClauseGenerator

method indicating if an asserting clause has been built. note that this method is called right after a resolution step is finished.

Specified by:

clauseNonAssertive in interface AssertingClauseGenerator

Parameters:

reason - the reason of the current literal assignment

Returns:

false iff the current clause is assertive

toString

public String toString()

Overrides:

toString in class Object