org.kahina.logic.sat.insertionmus.iterativ.simpleSAT.analyseConflict

Interface IAnalyseConflict

All Known Implementing Classes:

DefaultAnalyseConflict, DisabledLearnMoreAnalyseConflict, LearnMoreAnalyseConflict

public interface IAnalyseConflict

Method Summary

Methods

Modifier and Type	Method and Description
int	analyseConflict(Clause conflict) resolviert eine Konfliktklausel nach dem 1UIP prinzip.
void	init(CDCL cdcl)

Method Detail

analyseConflict

int analyseConflict(Clause conflict)

resolviert eine Konfliktklausel nach dem 1UIP prinzip. anschliesend wird sie weitmoeglichst vereinfacht. falls waerend diesem vorgang subsumierungen gefunden werden, werden entsprechend Klauseln geloescht.

Returns:

das neue Level (das hoechste level einer belegten Variable die in der aus der Konfliktklausel resolvierenden Klausel enthalten ist)

init

void init(CDCL cdcl)