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