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

Class Clause

java.lang.Object

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

public class Clause
extends java.lang.Object

Author:

Paul Seitz

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	Clause.ClauseState

Field Summary

Fields

Modifier and Type	Field and Description
java.util.ArrayList<java.lang.Integer>	literals

Constructor Summary

Constructors

Constructor and Description
Clause(java.util.ArrayList<java.lang.Integer> literals, Variable[] variables)
Clause(java.util.List<java.lang.Integer> literals)

Method Summary

Methods

Modifier and Type	Method and Description
void	delBoolHeur(Variable[] variables)
int	getUnassigned(Variable[] variables)
int	getUnassignedIndex(Variable[] variables)
int	initUnknownWatched(Variable[] variables) Initiates the watched variables when it is unknown if there are free variables
Clause.ClauseState	initWatch(Variable[] variables) Initialisiert die watched literals
boolean	isTautology() Testet ob diese Klausel eine Tautologie ist
void	remove(Variable[] variables)
Clause.ClauseState	reWatch(Variable[] variables, java.util.ArrayList<Clause> removeLater) Sucht ein neues watched literal fuer diese Klausel
Clause.ClauseState	reWatch(Variable[] variables, java.util.Iterator<Clause> it)
void	setBoolHeur(Variable[] variables)
void	setWatched(Variable[] variables) Setzt die watched literals auf eine unbelegte variable und die variable mit dem hoechsten lvl vb.: Es ist genau eine Variable unbelegt
void	setWatchedToUnsigned(Variable[] variables) Setzt die watched literals auf zwei unbelegte variablen vb.: es sind 2 unbelegte variablen vorhanden
boolean	testSat(Variable[] variables)
void	testWatchedLiterals(Variable[] variables)
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

literals

public final java.util.ArrayList<java.lang.Integer> literals

Constructor Detail

Clause

public Clause(java.util.ArrayList<java.lang.Integer> literals,
      Variable[] variables)

Clause

public Clause(java.util.List<java.lang.Integer> literals)

Method Detail

setBoolHeur

public void setBoolHeur(Variable[] variables)

delBoolHeur

public void delBoolHeur(Variable[] variables)

getUnassigned

public int getUnassigned(Variable[] variables)

getUnassignedIndex

public int getUnassignedIndex(Variable[] variables)

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

initWatch

public Clause.ClauseState initWatch(Variable[] variables)

Initialisiert die watched literals

Parameters:

variables - - der aktuelle Variablenvektor

Returns:

Den Status der Initialisierung (EMPTY, UNIT oder SUCCESS)

reWatch

public Clause.ClauseState reWatch(Variable[] variables,
                         java.util.ArrayList<Clause> removeLater)

Sucht ein neues watched literal fuer diese Klausel

Parameters:

variables - - der aktuelle Variablenvektor

lit - - das Literal, das belegt wurde

removeLater -

Returns:

den Status der Suche (SUCCESS, EMPTY, SAT oder UNIT) during this process the clause could have 3 watched literals, they should be removed by another function.

isTautology

public boolean isTautology()

Testet ob diese Klausel eine Tautologie ist

setWatched

public void setWatched(Variable[] variables)

Setzt die watched literals auf eine unbelegte variable und die variable mit dem hoechsten lvl vb.: Es ist genau eine Variable unbelegt

initUnknownWatched

public int initUnknownWatched(Variable[] variables)

Initiates the watched variables when it is unknown if there are free variables

Parameters:

variables -

Returns:

-1 if the new clause is a unit clause,-2 if the new clause is sat, Integer.MaxValue if no bagjump is needed, else the needed backjumplvl

setWatchedToUnsigned

public void setWatchedToUnsigned(Variable[] variables)

Setzt die watched literals auf zwei unbelegte variablen vb.: es sind 2 unbelegte variablen vorhanden

testWatchedLiterals

public void testWatchedLiterals(Variable[] variables)

testSat

public boolean testSat(Variable[] variables)

reWatch

public Clause.ClauseState reWatch(Variable[] variables,
                         java.util.Iterator<Clause> it)

remove

public void remove(Variable[] variables)