techniques.PL
Class CNF

java.lang.Object
  |
  +--techniques.PL.CNF

public final class CNF
extends java.lang.Object

A set of utilities for dealing with propositional logic sentences in conjunctive normal form (CNF).


Constructor Summary
CNF()
           
 
Method Summary
static boolean coinFlip()
          Returns true with probability 0.5.
static void main(java.lang.String[] args)
          A command-line accessible version of the randInstance() method.
static Conjunction parse(java.io.File infile)
          Parses a textfile into a Conjunction.
static Conjunction parse(java.lang.String sentence)
          Parses a String into a Conjunction.
static java.lang.String randDisjunction()
          Returns a disjunction of three literals chosen by randLiteral()
static java.lang.String randInstance(int numClauses)
          Returns a randomly generated 3-SAT instance, as a String.
static int randInt(int a, int b)
          returns a random integer between a and b, inclusive.
static java.lang.String randLiteral()
          Returns a random literal, as a string.
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

CNF

public CNF()
Method Detail

parse

public static Conjunction parse(java.lang.String sentence)
Parses a String into a Conjunction. This Parser does very little error checking. Unparsable sentences will either produce garbage or a runtime Exception. Whitespace is insignificant.

parse

public static Conjunction parse(java.io.File infile)
Parses a textfile into a Conjunction. If there is an IO Error, this method will print an error message and returns null. Otherwise, this Parser does very little error checking. Unparsable sentences will either produce garbage or a runtime Exception. Whitespace in the file is insignificant.

main

public static void main(java.lang.String[] args)
A command-line accessible version of the randInstance() method. It takes one mandatory and one optional argument. The first argument is a real number indicating the ratio of clauses to variables in the returned instance. The second (optional) argument is a filename in which to write the results. If no second argument is supplied, the sentence will be sent to standard out.

For example:

% java techniques.PL.CNF 2.2 mysentence.cnf

will result in a sentence with 57 clauses (about 2.2*26), written to a file named mysentence.cnf. See randInstance() for more documentation.


randInstance

public static java.lang.String randInstance(int numClauses)
Returns a randomly generated 3-SAT instance, as a String. All sentences are drawn from a world of 26 variables, A-Z. numClauses is the number of disjunctive clauses to generate.

randDisjunction

public static java.lang.String randDisjunction()
Returns a disjunction of three literals chosen by randLiteral()

randLiteral

public static java.lang.String randLiteral()
Returns a random literal, as a string. The variable of the literal is drawn uniformly from 'A'-'Z', and negated with probability 0.5.

coinFlip

public static boolean coinFlip()
Returns true with probability 0.5.

randInt

public static int randInt(int a,
                          int b)
returns a random integer between a and b, inclusive.