satisfiabilityApplet.algorithmsAndKBase
Class KBase

java.lang.Object
  extended bysatisfiabilityApplet.algorithmsAndKBase.KBase

public class KBase
extends java.lang.Object

by Catherine Block id# 6319 Date: Sep 6, 2004 Time: 9:02:36 AM CS 180H satisfiabilityApplet.algorithmsAndKBase.KBase is a knowlege base containing CNF clauses.


Constructor Summary
KBase(ViewPanel view)
          Constructor creates a new satisfiabilityApplet.algorithmsAndKBase.KBase
 
Method Summary
 void addSentence(java.lang.Object obj)
          Adds a sentence to the satisfiabilityApplet.algorithmsAndKBase.KBase
 boolean alwaysTrueBF(int[] arr)
          Uses Brute Force algorithm to determine if the conjunction of cnf's in the selected indices are always true.
 void deleteSelectedIndices(int[] arr)
          Delete the CNFs contained in selected indices.
 java.util.ArrayList getPolynomialForm()
           
 java.lang.Object getSelectedIndex(int index)
           
 boolean isSatisfiableBF(int[] arr)
          Uses Brute Force algorithm to determine if the conjunction of cnf's in the selected indices is satisfiable.
 boolean isSatisfiableDPLL(int[] arr)
          Uses DPLL algorithm to determine satisfiability
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

KBase

public KBase(ViewPanel view)
Constructor creates a new satisfiabilityApplet.algorithmsAndKBase.KBase

Parameters:
view - - The satisfiabilityApplet.gui.ViewPanel object that outputs the CNF clauses
Method Detail

addSentence

public void addSentence(java.lang.Object obj)
Adds a sentence to the satisfiabilityApplet.algorithmsAndKBase.KBase

Parameters:
obj - - A CNF sentence to add to the satisfiabilityApplet.algorithmsAndKBase.KBase

getSelectedIndex

public java.lang.Object getSelectedIndex(int index)
                                  throws java.lang.CloneNotSupportedException
Parameters:
index - - The index of a clause contained in the KB
Returns:
The clause contained at the indicated index
Throws:
java.lang.CloneNotSupportedException

deleteSelectedIndices

public void deleteSelectedIndices(int[] arr)
Delete the CNFs contained in selected indices. This will delete any underlying symbols that are only referenced by CNF's being deleted.

Parameters:
arr - An array of selected indices representing the positions of Sentences in items.

getPolynomialForm

public java.util.ArrayList getPolynomialForm()

alwaysTrueBF

public boolean alwaysTrueBF(int[] arr)
                     throws java.lang.Exception
Uses Brute Force algorithm to determine if the conjunction of cnf's in the selected indices are always true.

Parameters:
arr - - An array of indices representing sentences selected in the GUI
Returns:
Throws:
java.lang.Exception

isSatisfiableBF

public boolean isSatisfiableBF(int[] arr)
                        throws java.lang.Exception
Uses Brute Force algorithm to determine if the conjunction of cnf's in the selected indices is satisfiable.

Parameters:
arr - - An array of indices representing sentences selected in the GUI
Returns:
True if the conjunction is satisfiable
Throws:
java.lang.Exception

isSatisfiableDPLL

public boolean isSatisfiableDPLL(int[] arr)
                          throws java.lang.Exception
Uses DPLL algorithm to determine satisfiability

Parameters:
arr -
Returns:
true if the conjunction is satisfiable
Throws:
java.lang.Exception