CnfUtil.java 0100664 0073245 0000275 00000003564 07741435675 0014066 0 ustar 00schapire cs302 0000443 0000006 /** This class includes several static methods which may be useful in
* processing CNF formulas. A CNF is represented as an array of
* arrays of Literals, where each of the component arrays
* represents a disjunction of literals.
*/
public class CnfUtil {
/** Returns one plus the largest index of any symbol referenced by the
* given CNF.
*/
public static int getNumSymbols(Literal[][] cnf) {
int max = 0;
for (int i = 0; i < cnf.length; i++)
for (int j = 0; j < cnf[i].length; j++)
if (cnf[i][j].symbol > max)
max = cnf[i][j].symbol;
return max + 1;
}
/** Converts a given CNF to a multi-line string representation
* suitable for printing.
*/
public static String cnfToString(Literal[][] cnf) {
String s = "";
for (int i = 0; i < cnf.length; i++) {
for (int j = 0; j < cnf[i].length; j++)
s += " " + (cnf[i][j].sign ? "+" : "-") + cnf[i][j].symbol;
s += "\n";
}
return s;
}
/** Converts a given model (represented by a boolean array) to a
* string representation suitable for printing.
*/
public static String modelToString(boolean[] model) {
String s = "";
for (int i = 0; i < model.length; i++)
s += " " + (model[i] ? "+" : "-");
return s;
}
/** Returns true if the given model satisfies the given
* clause.
*/
public static boolean isClauseSat(Literal[] clause, boolean[] model) {
for (int j = 0; j < clause.length; j++)
if (model[clause[j].symbol] == clause[j].sign)
return true;
return false;
}
/** Returns the number of clauses of the given CNF not satisfied
* by the given model.
*/
public static int numClauseUnsat(Literal[][] cnf, boolean[] model) {
int num_not_satd = 0;
for (int i = 0; i < cnf.length; i++)
if (!isClauseSat(cnf[i], model))
num_not_satd++;
return num_not_satd;
}
}
DimacsFileGenerator.java 0100664 0073245 0000275 00000007076 07745120602 0016354 0 ustar 00schapire cs302 0000443 0000006 import java.util.*;
import java.io.*;
/** A Generator that simply reads a file representing a CNF
* in the style used in the DIMACS implementation challenge.
* (Note that these files must be uncompressed before using here.)
* Each time getNext is called, this same CNF is returned.
* This class also includes a main method for testing.
*/
public class DimacsFileGenerator implements Generator {
Literal[][] cnf;
/** Constructor for this generator.
* @param file_name name of file containing DIMACS CNF description
*/
public DimacsFileGenerator(String file_name)
throws FileNotFoundException, IOException
{
BufferedReader in;
String line;
Stack s = new Stack( );
Literal literal = new Literal( );
try
{
in = new BufferedReader(new FileReader(file_name));
} catch (FileNotFoundException e)
{
System.err.print("File "+file_name+" not found.\n");
throw e;
}
int i = 0;
while( true )
{
try
{
line = in.readLine();
} catch (IOException e)
{
System.err.println("Error reading file "+file_name);
throw e;
}
if (line == null)
break;
line = line.trim( );
String[] words = line.split("\\s");
if (words[0].equals("c"))
continue;
if (words[0].equals("p"))
{
if (!words[1].equals("cnf"))
System.err.println("expect cnf after p in file " + file_name);
int num_clauses = Integer.parseInt(words[3]);
cnf = new Literal[num_clauses][];
}
else if (!line.equals(""))
{
for (int j = 0; j < words.length; j++)
{
int var = Integer.parseInt(words[j]);
if( var == 0 )
{
cnf[i] = new Literal[ s.size( ) ];
int k = 0;
while( ! s.empty( ) )
{
cnf[i][k] = ( Literal ) s.pop( );
k++;
}
i++;
s = new Stack( );
break;
}
literal = new Literal( );
literal.sign = (var > 0);
literal.symbol = (var < 0 ? -var : var) - 1;
s.push( literal );
}
}
}
}
/** Returns the CNF read in from the named DIMACS file. */
public Literal[][] getNext()
{
return cnf;
}
/** This is a simple main which runs MySatSolver
* on the CNF stored in the file named in the first argument
* within the time limit specified by the second argument.
*/
public static void main(String[] argv)
throws FileNotFoundException, IOException
{
String file_name = "";
int time_limit = 0;
try
{
file_name = argv[0];
time_limit = Integer.parseInt(argv[1]);
if( time_limit == -1 )
time_limit = 3600;
} catch (Exception e)
{
System.err.println("Arguments: ");
return;
}
Generator gen = new DimacsFileGenerator(file_name);
SatSolver sat = new MySatSolver();
Literal[][] cnf = gen.getNext();
System.out.println("cnf:");
System.out.println(CnfUtil.cnfToString(cnf));
Timer timer = new Timer(time_limit * 1000);
boolean[] model = sat.solve(cnf, timer);
System.out.println("elapsed time= " + timer.getTimeElapsed());
int num_unsat = CnfUtil.numClauseUnsat(cnf, model);
System.out.println("num_unsat= " + num_unsat);
System.out.println("model: " +
CnfUtil.modelToString(model));
}
}
Generator.java 0100664 0073245 0000275 00000000436 07741435677 0014445 0 ustar 00schapire cs302 0000443 0000006 /** The interface for a CNF Generator. Each time the
* getNext method is called, a new CNF is generated and
* returned.
*/
public interface Generator {
/** This method returns a new CNF formula each time it is called. */
public Literal[][] getNext();
}
Literal.java 0100664 0073245 0000275 00000000370 07741435677 0014110 0 ustar 00schapire cs302 0000443 0000006 /** An object of this class represents a literal (signed symbol) */
public class Literal {
/** sign of the literal: true = unnegated, false = negated */
public boolean sign;
/** index of proposition symbol */
public int symbol;
}
MyGenerator.java 0100664 0073245 0000275 00000001212 07741435700 0014727 0 ustar 00schapire cs302 0000443 0000006 import java.util.*;
/** This is just a template of the MyGenerator class that
* must be turned in.
*/
public class MyGenerator implements Generator {
/** Must have a constructor taking no arguments. (You may have
* other constructors that you use for your experiments, but this
* is the constructor that will be used as part of the class
* implementation challenge.)
*/
public MyGenerator() {
// fill in initialization code here
}
/** This is the method that generates CNF formulas each time it is
* called.
*/
public Literal[][] getNext() {
// fill in generation code here
}
}
implements Generator {
/** Must have a constructor taking no arguments. (You may have
* other constructors that you use for your experiments, but this
* is the constructor that will be used as part of the class
* implementation challenge.)
*/
public MyGenerator() {
// fill in initialization code here
}
/** This is the method that gMySatSolver.java 0100664 0073245 0000275 00000002757 07741435700 0014742 0 ustar 00schapire cs302 0000443 0000006 import java.util.*;
/** This is a dummy version of MySatSolver that simply
* generates random models and returns the best one when time runs
* out. You can use this class as a template for your own.
*/
public class MySatSolver implements SatSolver {
private Random random; // a random number generator
/** A constructor for this class. You must include a constructor
* such as this one taking no arguments. (You may have other
* constructors that you use for your experiments, but this is the
* constructor that will be used as part of the class
* implementation challenge.)
*/
public MySatSolver() {
random = new Random();
}
/** This dummy routine attempts to solve the satisfaction problem
* by trying random models until time runs out and returning the
* best one.
*/
public boolean[] solve(Literal[][] cnf, Timer timer) {
boolean[] model = new boolean[CnfUtil.getNumSymbols(cnf)];
boolean[] best_model = new boolean[CnfUtil.getNumSymbols(cnf)];
int best_num_not_satd = cnf.length + 1;
int num_not_satd;
while(timer.getTimeRemaining() >= 0) {
for (int i = 0; i < model.length; i++)
model[i] = random.nextBoolean();
num_not_satd = CnfUtil.numClauseUnsat(cnf, model);
if (num_not_satd < best_num_not_satd) {
if (num_not_satd == 0)
return model;
best_num_not_satd = num_not_satd;
for (int i = 0; i < model.length; i++)
best_model[i] = model[i];
}
}
return best_model;
}
}
RandomCnfGenerator.java 0100664 0073245 0000275 00000006000 07741435701 0016212 0 ustar 00schapire cs302 0000443 0000006 import java.util.*;
/** This Generator generates random CNF formulas of a fixed
* size over a fixed number of symbols and with a fixed number of
* literals per clause. This class also includes a main
* method for testing.
*/
public class RandomCnfGenerator implements Generator {
private int num_clauses; // number of clauses
private int num_symbols; // number of symbols
private int num_literals; // number of literals per clause
private Random random; // random number generator
/** Constructor for this object.
* @param num_clauses number of clauses in constructed CNF
* @param num_symbols number of symbols (variables) in CNF
* @param num_literals number of literals per clause
*/
public RandomCnfGenerator(int num_clauses, int num_symbols, int num_literals) {
random = new Random();
this.num_clauses = num_clauses;
this.num_symbols = num_symbols;
this.num_literals = num_literals;
}
/** Generates another CNF of the specified form. */
public Literal[][] getNext() {
Literal[][] cnf = new Literal[num_clauses][num_literals];
for (int i = 0; i < num_clauses; i++) {
for (int j = 0; j < num_literals; j++) {
cnf[i][j] = new Literal();
cnf[i][j].sign = random.nextBoolean();
cnf[i][j].symbol = random.nextInt(num_symbols);
}
}
return cnf;
}
/** This is a simple main. It generates a random CNF
* formula with number of clauses, number of symbols and number of
* literals per clause specified by the first three arguments.
* Once generated, MySatSolver is called to try to solve
* the CNF within the time limit specified by the fourth argument.
* This process is repeated the number of times specified by the
* fifth argument.
*/
public static void main(String[] argv) {
int num_clauses = 0;
int num_symbols = 0;
int num_literals = 0;
int time_limit = 0;
int num_reps = 0;
try {
num_clauses = Integer.parseInt(argv[0]);
num_symbols = Integer.parseInt(argv[1]);
num_literals = Integer.parseInt(argv[2]);
time_limit = Integer.parseInt(argv[3]);
num_reps = Integer.parseInt(argv[4]);
}
catch (Exception e) {
System.err.println("Arguments: ");
return;
}
Generator gen = new RandomCnfGenerator(num_clauses,
num_symbols,
num_literals);
SatSolver sat = new MySatSolver();
for (int r = 0; r < num_reps; r++) {
Literal[][] cnf = gen.getNext();
System.out.println("--------------------------");
System.out.println("cnf:");
System.out.println(CnfUtil.cnfToString(cnf));
Timer timer = new Timer(time_limit * 1000);
boolean[] model = sat.solve(cnf, timer);
System.out.println("elapsed time= " + timer.getTimeElapsed());
int num_unsat = CnfUtil.numClauseUnsat(cnf, model);
System.out.println("num_unsat= " + num_unsat);
System.out.println("model: " +
CnfUtil.modelToString(model));
}
}
}
SatSolver.java 0100664 0073245 0000275 00000000731 07741435701 0014423 0 ustar 00schapire cs302 0000443 0000006 /** This is the interface defining a SatSolver object. Every
* SatSolver must include a method solve for solving CNF
* satisfiability problems.
*/
public interface SatSolver {
/** This is the method for solving satifiability problems. This
* method should return something by when time runs out on the
* given timer object (or very soon thereafter).
*/
public boolean[] solve(Literal[][] cnf, Timer timer);
}
Timer.java 0100664 0073245 0000275 00000002045 07741435702 0013562 0 ustar 00schapire cs302 0000443 0000006 import java.util.*;
/** An object in this class acts as a timer, indicating both how much
* time has elapsed from the time the object was created, as well as
* how much time remains until the end of a specified period.
*/
public class Timer {
private long start_time;
private long end_time;
/** This constructor begins a timer which will run for a period
* specified by the max_time parameter.
* @param max_time timer duration in milliseconds
*/
public Timer(long max_time) {
start_time = System.currentTimeMillis();
end_time = start_time + max_time;
}
/** Returns the time (in milliseconds) that has elapsed since the
* creation of this object.
*/
public long getTimeElapsed() {
return (System.currentTimeMillis() - start_time);
}
/** Returns the time (in milliseconds) that remains until the
* timer object reaches the end of the period specified at its
* creation.
*/
public long getTimeRemaining() {
return (end_time - System.currentTimeMillis());
}
}