savi.alg.sat3
Class Clause

java.lang.Object
  extended by savi.alg.sat3.Clause

public class Clause
extends java.lang.Object

Object representing a clause.


Field Summary
protected  int[] varsIndex
          list of variables index
protected  boolean[] varsNegation
          array of negation for variables
 
Constructor Summary
Clause(int varsCount, int clauseLen)
          Creates a new instance of Clause, generate random clause from parameters.
Clause(java.util.Vector dimacsClause)
          Creates a new instance of Clause from one dimacs format line.
 
Method Summary
 java.lang.String getCnfRepresentation()
          Return dimacs text representation of the clause.
 int getLiteralCount()
          Return number of literals in clause.
 java.lang.String getLiteralStringRepresentation()
          Return text representation of the clause.
 boolean isSatisfact(boolean[] vars)
          Return true if the clause is satisfied vith given variables assignment.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

varsIndex

protected int[] varsIndex
list of variables index


varsNegation

protected boolean[] varsNegation
array of negation for variables

Constructor Detail

Clause

public Clause(int varsCount,
              int clauseLen)
Creates a new instance of Clause, generate random clause from parameters.

Parameters:
varsCount - number of Clauses
clauseLen - number of literals in clause

Clause

public Clause(java.util.Vector dimacsClause)
Creates a new instance of Clause from one dimacs format line. see http:\\www.satlib.org

Parameters:
dimacsClause - vector with numbers representing clause
Method Detail

isSatisfact

public boolean isSatisfact(boolean[] vars)
Return true if the clause is satisfied vith given variables assignment.

Parameters:
vars - variables assignment
Returns:
true if clause is satisfact

getLiteralCount

public int getLiteralCount()
Return number of literals in clause.

Returns:
number of literals

getLiteralStringRepresentation

public java.lang.String getLiteralStringRepresentation()
Return text representation of the clause. This represenatation is printed to user.

Returns:
text representation

getCnfRepresentation

public java.lang.String getCnfRepresentation()
Return dimacs text representation of the clause.

Returns:
text represenation of the clause.