org.sat4j.minisat.core
Interface AssertingClauseGenerator

All Known Implementing Classes:
DecisionUIP, FirstUIP

public interface AssertingClauseGenerator

An assertingClauseGenerator is responsible for the creation of an asserting clause during conflict analysis. An asserting clause is a clause that will become unit when the solver will backtrack to the latest decision level, providing a nice way for the solver to backtrack.

Author:
leberre

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.
 

Method Detail

initAnalyze

void initAnalyze()
hook method called before the analysis.


onCurrentDecisionLevelLiteral

void onCurrentDecisionLevelLiteral(int p)
hook method called when a literal from the current decision lelvel is found.

Parameters:
p - the literal in the current decision level

clauseNonAssertive

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.

Parameters:
reason - the reason of the current literal assignment
Returns:
false iff the current clause is assertive


Copyright © 2007 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.