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, Timer timer) This is the method for solving satifiability problems.

Method Detail

solve

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

This is the method for solving satifiability problems. This method should return a solution satisfying as many clauses of the given CNF as possible by when time runs out on the given timer object (or very soon thereafter).

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.