sat
Class SATProblem

java.lang.Object
  extended by sat.SATProblem
All Implemented Interfaces:
Problem
public class SATProblem
extends java.lang.Object
implements Problem

This class is used to capture an instance of the k-SAT problem.

See Also:
Problem

Field Summary
 int C
          # Clauses.
 java.lang.String errorMessage
          If there's an error in the problem instance, a message is written here.
 int K
          K = #literals/clause.
 int[][] literals
          This 2D array is used to store the actual clauses.
 int N
          # Variables.
 int T
          T=1 if we do NOT allow the same variable appearing more than once in a clause.
 java.lang.String topMessage
           
 
Constructor Summary
SATProblem(boolean noParameters)
           
SATProblem(int K, int N, int C, int T, int[][] literals)
          Problem-instance creators should use this constructor.
 
Method Summary
 java.lang.String getErrorMessage()
          Retrieve error message about an invalid problem.
 void readFromFile(java.io.File f)
          Read the problem in plain text from the given file.
 java.lang.String toString()
          Returns a problem description summary.
 void writeToFile(java.io.File f)
          Write the problem in plain text to the given file.
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

K

public int K
K = #literals/clause.

N

public int N
# Variables.

C

public int C
# Clauses.

T

public int T
T=1 if we do NOT allow the same variable appearing more than once in a clause.

literals

public int[][] literals
This 2D array is used to store the actual clauses. First, we'll use variables x_1, ..., x_N. NOTE: there's no zero, so that there's no confusion with the default array values. literals[c][k] corresponds to clause c and k-th variable in the c-th clause. Consider an example with c=3: literals[3][0] = -6 literals[3][1] = 7 literals[3][2] = 5 literals[3][3] = -8 Here, x6 appears in complement form, then x7 regular, then x5, and then x8 in complemented form.

errorMessage

public java.lang.String errorMessage
If there's an error in the problem instance, a message is written here.

topMessage

public java.lang.String topMessage
Constructor Detail

SATProblem

public SATProblem(boolean noParameters)

SATProblem

public SATProblem(int K,
                  int N,
                  int C,
                  int T,
                  int[][] literals)
Problem-instance creators should use this constructor.

Parameters:
K - an int value
N - an int value
C - an int value
T - an int value
literals - an int[][] value
Method Detail

writeToFile

public void writeToFile(java.io.File f)
Description copied from interface: Problem
Write the problem in plain text to the given file.

Specified by:
writeToFile in interface Problem
Parameters:
f - a File value

readFromFile

public void readFromFile(java.io.File f)
Description copied from interface: Problem
Read the problem in plain text from the given file.

Specified by:
readFromFile in interface Problem
Parameters:
f - a File value

toString

public java.lang.String toString()
Description copied from interface: Problem
Returns a problem description summary.

Specified by:
toString in interface Problem
Overrides:
toString in class java.lang.Object
Returns:
a String value

getErrorMessage

public java.lang.String getErrorMessage()
Description copied from interface: Problem
Retrieve error message about an invalid problem.

Specified by:
getErrorMessage in interface Problem
Returns:
a String value