savi.alg.sat3
Class Formula

java.lang.Object
  extended by savi.alg.sat3.Formula
Direct Known Subclasses:
WeightedFormula

public class Formula
extends java.lang.Object

Class representing boolean formula in CNF.


Field Summary
protected  Clause[] clauses
          list of clauses in formula
protected  int varsCount
          number of variables in formula
 
Constructor Summary
Formula(java.io.BufferedReader br)
          Creates a new instance of Formula, read it from stream (expecting stream with DIMACS format).
Formula(int countClauses, int varsCount)
          Creates a new instance of Formula, randomly generate clauses from given parameters.
 
Method Summary
 int clausesCount()
          Return count of clauses.
 Formula clone()
          Creates and returns a copy of this object.
 int countSatisfactClauses(boolean[] vars)
          Return number of satisfied clauses.
 Clause[] getClauses()
          Return number of clauses.
 boolean isSatisfact(boolean[] vars)
          Return true if formula is satisfied with given variables assignment.
 double percentualSatisfact(boolean[] vars)
          Return percentual satisfaction of the formula with given variables assignment. 0 means no one clause is satisfied, 1 means formula is satisfied
protected  void readFromStream(java.io.BufferedReader br)
          Read formula from stream (expecting stream with DIMACS format).
 void reduceNumberOfClauses(double finalPercent)
          Reduce number of clauses in the formula.
 int varsCount()
          Return count of variables.
 
Methods inherited from class java.lang.Object
equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

clauses

protected Clause[] clauses
list of clauses in formula


varsCount

protected int varsCount
number of variables in formula

Constructor Detail

Formula

public Formula(int countClauses,
               int varsCount)
Creates a new instance of Formula, randomly generate clauses from given parameters.

Parameters:
countClauses - number of clauses in formula
varsCount - number of variables in formula

Formula

public Formula(java.io.BufferedReader br)
        throws WrongInputFormulaData
Creates a new instance of Formula, read it from stream (expecting stream with DIMACS format).

Parameters:
br - stream with buffer reader
Throws:
WrongInputFormulaData - syntax error exception
Method Detail

isSatisfact

public boolean isSatisfact(boolean[] vars)
Return true if formula is satisfied with given variables assignment.

Parameters:
vars - variables assignment
Returns:
true if formula is satisfied

percentualSatisfact

public double percentualSatisfact(boolean[] vars)
Return percentual satisfaction of the formula with given variables assignment. 0 means no one clause is satisfied, 1 means formula is satisfied

Parameters:
vars - variables assignment
Returns:
fraction of clauses satisfaction

countSatisfactClauses

public int countSatisfactClauses(boolean[] vars)
Return number of satisfied clauses.

Parameters:
vars - variables assignment
Returns:
number of satisfied clauses

varsCount

public int varsCount()
Return count of variables.

Returns:
count of variables

clausesCount

public int clausesCount()
Return count of clauses.

Returns:
count of variables

reduceNumberOfClauses

public void reduceNumberOfClauses(double finalPercent)
                           throws WrongFormulaException
Reduce number of clauses in the formula.

Parameters:
finalPercent - percentual count, how many clauses should remain
Throws:
WrongFormulaException - the formula is reduced too many

readFromStream

protected void readFromStream(java.io.BufferedReader br)
                       throws WrongInputFormulaData
Read formula from stream (expecting stream with DIMACS format).

Parameters:
br - stream with buffer reader
Throws:
WrongInputFormulaData - syntax error exception

getClauses

public Clause[] getClauses()
Return number of clauses.

Returns:
number of clauses

clone

public Formula clone()
Creates and returns a copy of this object.

Overrides:
clone in class java.lang.Object
Returns:
deep copy of Formula object