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

Class LearnMoreAnalyseConflict

java.lang.Object

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

All Implemented Interfaces:

IAnalyseConflict

public class LearnMoreAnalyseConflict
extends java.lang.Object
implements IAnalyseConflict

Field Summary

Fields

Modifier and Type	Field and Description
static double	ACTIVITYCONFVAR
static double	ACTIVITYGAIN
int	LearnClauseLimit

Constructor Summary

Constructors

Constructor and Description
LearnMoreAnalyseConflict()

Method Summary

Methods

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

Methods inherited from class java.lang.Object

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

Field Detail

ACTIVITYGAIN

public static double ACTIVITYGAIN

ACTIVITYCONFVAR

public static double ACTIVITYCONFVAR

LearnClauseLimit

public int LearnClauseLimit

Constructor Detail

LearnMoreAnalyseConflict

public LearnMoreAnalyseConflict()

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

resolveIfShortsClause2

public void resolveIfShortsClause2(Clause newClause)