org.sat4j.minisat.uip
Class FirstUIP

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

public class FirstUIP
extends java.lang.Object
implements AssertingClauseGenerator, java.io.Serializable

FirstUIP scheme introduced in Chaff. Here the generator stops when a syntactical criteria is met: only one literal in the current decision level appears in the generated clause. The computation is done by counting the literals appearing in the current decision level and decrementing that counter when a resolution step is done.

Author:
leberre
See Also:
Serialized Form

Constructor Summary
FirstUIP()
           
 
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

FirstUIP

public FirstUIP()
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