org.sat4j.minisat.uip
Class DecisionUIP

java.lang.Object
  extended by org.sat4j.minisat.uip.DecisionUIP
All Implemented Interfaces:
java.io.Serializable, AssertingClauseGenerator

public class DecisionUIP
extends java.lang.Object
implements AssertingClauseGenerator, java.io.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.
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, 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