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

Class CDCL

java.lang.Object

org.kahina.logic.sat.insertionmus.iterativ.simpleSAT.main.CDCL

public class CDCL
extends java.lang.Object

Author:

Paul Seitz

Field Summary

Fields

Modifier and Type	Field and Description
AbstractActivity	activity
java.util.ArrayList<Clause>	addLater
protected Clause	addLaterUnitClause
java.util.ArrayList<Clause>	addUnit
IAnalyseConflict	analyseConflict
ClauseSet	instance
int	lvl
protected IUnitPropagation	propagation
protected boolean	set
java.util.Stack<Variable>	stack

Constructor Summary

Constructors

Constructor and Description
CDCL(ClauseSet set)
CDCL(ClauseSet set, AbstractActivity activity, IUnitPropagation unitPropagation, IAnalyseConflict analyseConflict)

Method Summary

Methods

Modifier and Type	Method and Description
Solution	addNextAndContinue(long timeout, Clause c)
int	computeBacktrackLevel(Clause newClause) Zweithoechste lvl der variablen in newClause
void	removeClause(Clause c)
void	reset() Removes all learned Clauses, sets lvl to 0 but keeps activity values for variables
Clause	resolve(Clause c1, Clause c2) Resolviert zwei Klauseln
Clause	resolve2(Clause c1, Clause newClause, int v)
Clause	resolveC1Begin(Clause c1, Clause c2) Resolviert zwei Klauseln wobei c1.literals[0] negiert in c2.literals vorkommen muss.
void	resolveIfShortsClause(Clause newClause) Fuer jedes literal in der neuen Clausel wird untersucht ob eine Resolution mit dem grund fuer die Variable die Clausel verkleinern wuerde.
void	setValues(int countTill, int clauseLimit, double actReduction, double actGain, double initActGain, double clActGain, int restardValue1, int restardValue2, int restardValue3, double pRestardMultiplikator)
Solution	solve(long timeout)

Methods inherited from class java.lang.Object

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

Field Detail

instance

public ClauseSet instance

stack

public java.util.Stack<Variable> stack

lvl

public int lvl

addLater

public java.util.ArrayList<Clause> addLater

addUnit

public java.util.ArrayList<Clause> addUnit

addLaterUnitClause

protected Clause addLaterUnitClause

activity

public final AbstractActivity activity

propagation

protected final IUnitPropagation propagation

analyseConflict

public final IAnalyseConflict analyseConflict

set

protected boolean set

Constructor Detail

CDCL

public CDCL(ClauseSet set)

CDCL

public CDCL(ClauseSet set,
    AbstractActivity activity,
    IUnitPropagation unitPropagation,
    IAnalyseConflict analyseConflict)

Method Detail

resolve

public Clause resolve(Clause c1,
             Clause c2)

Resolviert zwei Klauseln

Parameters:

c1 -

c2 -

Returns:

removeClause

public void removeClause(Clause c)

resolveC1Begin

public Clause resolveC1Begin(Clause c1,
                    Clause c2)

Resolviert zwei Klauseln wobei c1.literals[0] negiert in c2.literals vorkommen muss.

Parameters:

c1 -

c2 -

Returns:

resolveIfShortsClause

public void resolveIfShortsClause(Clause newClause)

Fuer jedes literal in der neuen Clausel wird untersucht ob eine Resolution mit dem grund fuer die Variable die Clausel verkleinern wuerde.

Parameters:

newClause -

computeBacktrackLevel

public int computeBacktrackLevel(Clause newClause)

Zweithoechste lvl der variablen in newClause

Parameters:

newClause -

Returns:

solve

public Solution solve(long timeout)

addNextAndContinue

public Solution addNextAndContinue(long timeout,
                          Clause c)

resolve2

public Clause resolve2(Clause c1,
              Clause newClause,
              int v)

setValues

public void setValues(int countTill,
             int clauseLimit,
             double actReduction,
             double actGain,
             double initActGain,
             double clActGain,
             int restardValue1,
             int restardValue2,
             int restardValue3,
             double pRestardMultiplikator)

reset

public void reset()

Removes all learned Clauses, sets lvl to 0 but keeps activity values for variables