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

Class DefaultAnalyseConflict

java.lang.Object

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

All Implemented Interfaces:

IAnalyseConflict

public class DefaultAnalyseConflict
extends java.lang.Object
implements IAnalyseConflict

Constructor Summary

Constructors

Constructor and Description
DefaultAnalyseConflict()

Method Summary

Methods

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

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

DefaultAnalyseConflict

public DefaultAnalyseConflict()

Method Detail

analyseConflict

public int analyseConflict(Clause conflict)

Description copied from interface: IAnalyseConflict

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

Specified by:

analyseConflict in interface IAnalyseConflict

Returns:

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

init

public void init(CDCL cdcl)

Specified by:

init in interface IAnalyseConflict