Class Formula

java.lang.Object
  Formula

public class Formula
extends java.lang.Object

Formula class holds a vector of clauses, a vector of booleans, a vector of clause numbers, and a vector of integers. The booleans correspond to the clauses,and if they are true or false. The clause numbers are which clauses will be true when certain variables are true. The integers correspond to the number of times each term occurs in the formula.

Constructor Summary

Formula(Formula f)
Constructor that creates a copy of f.

Formula(java.lang.String inputFileName)
Constructor for class Formula.

Method Summary

void	add(Clause c) Add a clause to the formula.
java.util.Vector	getClauses() Returns the vector of clauses.
java.util.Vector	getFormula() Returns the vector of clauses.
java.lang.String	getInputFile()
int	getNumVars()
double[]	getOccurrences() Returns the occurrences of each variable, in the form of a vector.
boolean	hasEmptyClause() Returns true if there is an empty clause.
boolean	hasFalseClause(Assignment partial) Returns false if any clause can't be satisfied given the partial assignment.
boolean	isEmpty() Returns true if the formula is empty.
boolean	satisfied(Assignment partial) Checks to see if the formula is satisfied by the given partial assignment.
void	setIndex(int pos, int clauseNum) Sets a clause number to a spot in the index vector.
void	setOccurred(Assignment pa) Counts the occurrences of each term in the formula.
java.lang.String	toString() Makes the formula into a string.
int	unitClause(Assignment pa) Checks for unit clauses in the formula.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

Formula

public Formula(java.lang.String inputFileName)
        throws java.io.FileNotFoundException

Constructor for class Formula. Initializes the vector of booleans, clauses, lists of clause numbers, and term occurrences.

Parameters:

numClauses - the number of clauses

numVars - the number of variables

Throws:

java.io.FileNotFoundException

Formula

public Formula(Formula f)

Constructor that creates a copy of f. Initializes the vector of booleans, clauses, lists of clause numbers, and term occurrences.

Parameters:

f - is another formula

Method Detail

getNumVars

public int getNumVars()

getInputFile

public java.lang.String getInputFile()

add

public void add(Clause c)

Add a clause to the formula.

Parameters:

c - the clause to be added to the vector of clauses.

setIndex

public void setIndex(int pos,
                     int clauseNum)

Sets a clause number to a spot in the index vector.

Parameters:

pos - the position in the vector.

clauseNum - the clause number to be inserted.

getClauses

public java.util.Vector getClauses()

Returns the vector of clauses.

Returns:

Vector with the list of clauses.

getFormula

public java.util.Vector getFormula()

Returns the vector of clauses.

Returns:

Vector the list of clauses.

isEmpty

public boolean isEmpty()

Returns true if the formula is empty.

Returns:

boolean true if the formula is empty.

hasEmptyClause

public boolean hasEmptyClause()

Returns true if there is an empty clause.

Returns:

boolean true if there is an empty clause.

satisfied

public boolean satisfied(Assignment partial)

Checks to see if the formula is satisfied by the given partial assignment.

Parameters:

partial - the partial assignment to be checked.

Returns:

boolean true if the formula is satisfied.

hasFalseClause

public boolean hasFalseClause(Assignment partial)

Returns false if any clause can't be satisfied given the partial assignment.

Parameters:

partial - the assignment to be checked.

Returns:

boolean true if a clause can't be satisfied.

setOccurred

public void setOccurred(Assignment pa)

Counts the occurrences of each term in the formula. This counting happens each time the solver chooses the next variable. This method sets up the Jeroslaw-Wang heuristic for choosing the next variable.

Parameters:

pa - the current partial assignment.

getOccurrences

public double[] getOccurrences()

Returns the occurrences of each variable, in the form of a vector.

Returns:

Vector the vector of occurrences.

unitClause

public int unitClause(Assignment pa)

Checks for unit clauses in the formula. This is checked against the current partial assignment. Returns a positive number if the variable must be set to true, or a negative number if the variable must be set to false (in order to satisfy the clause). Returns zero if there is no unit clause.

Parameters:

pa - the current partial assignment

Returns:

int the variable in the unit clause, or zero if there is none

toString

public java.lang.String toString()

Makes the formula into a string.

Overrides:

toString in class java.lang.Object

Returns:

String the formula as a string.