Interface SatSolver

All Known Implementing Classes:

MySatSolver, RandomSearchSatSolver

public interface SatSolver

This is the interface defining a SatSolver object. Every SatSolver must include a method solve for solving CNF satisfiability problems. In addition, it must include a method returning the "author" of the program, and another method returning a brief description of the algorithm used.

Method Summary

java.lang.String	author() This method should simply return the "author" of this program as you would like it to appear on a class website.
java.lang.String	description() This method should return a very brief (1-3 sentence) description of the algorithm and implementational improvements that are being used, appropriate for posting on the class website.
boolean[]	solve(Literal[][] cnf, int num_symbols, Timer timer) This is the method for solving satifiability problems.

Method Detail

solve

boolean[] solve(Literal[][] cnf,
                int num_symbols,
                Timer timer)

This is the method for solving satifiability problems. Each Literal of the given cnf must include symbols indexed by integers between 0 and num_symbols-1. The method should return a solution in the form of a boolean array of length num_symbols representing an assignment to all the symbols of the given CNF that satisfies as many clauses as possible by when time runs out on the given timer object (or very soon thereafter).

Parameters:

cnf - the given cnf, represented as an array of arrays of Literals

num_symbols - the number of distinct symbols in the cnf

timer - the given timer object

author

java.lang.String author()

This method should simply return the "author" of this program as you would like it to appear on a class website. You can use your real name or a pseudonym of your choice.

description

java.lang.String description()

This method should return a very brief (1-3 sentence) description of the algorithm and implementational improvements that are being used, appropriate for posting on the class website.