org.sat4j.minisat.core
Interface LearnedConstraintsDeletionStrategy

All Superinterfaces:

Serializable

public interface LearnedConstraintsDeletionStrategy
extends Serializable

Strategy for cleaning the database of learned clauses.

Author:

leberre

Method Summary

ConflictTimer	getTimer()
void	init()
void	onClauseLearning(Constr outLearnt) Hook method called when a new clause has just been derived during conflict analysis.
void	onConflictAnalysis(Constr reason) Hook method called on constraints participating to the conflict analysis.
void	onPropagation(Constr from) Hook method called when a unit clause is propagated thanks to from.
void	reduce(IVec<Constr> learnedConstrs) Hook method called when the solver wants to reduce the set of learned clauses.

Method Detail

init

void init()

getTimer

ConflictTimer getTimer()

reduce

void reduce(IVec<Constr> learnedConstrs)

Hook method called when the solver wants to reduce the set of learned clauses.

Parameters:

learnedConstrs -

onClauseLearning

void onClauseLearning(Constr outLearnt)

Hook method called when a new clause has just been derived during conflict analysis.

Parameters:

outLearnt -

onConflictAnalysis

void onConflictAnalysis(Constr reason)

Hook method called on constraints participating to the conflict analysis.

Parameters:

reason -

onPropagation

void onPropagation(Constr from)

Hook method called when a unit clause is propagated thanks to from.

Parameters:

from -