org.sat4j.minisat.uip
Class FirstUIP

java.lang.Object
  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.
java.lang.String	toString()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, 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

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object