Class RandomSearchSatSolver

java.lang.Object
  RandomSearchSatSolver

All Implemented Interfaces:

SatSolver

public class RandomSearchSatSolver
extends java.lang.Object
implements SatSolver

This is a trivial implementation of SatSolver that simply generates random models and returns the best one when time runs out. You can use this class as a sample when writing your own.

Constructor Summary

RandomSearchSatSolver()
A constructor for this class.

Method Summary

java.lang.String	author() The author of this sat-solver.
java.lang.String	description() A brief description of this sat-solver.
boolean[]	solve(Literal[][] cnf, int num_symbols, Timer timer) This routine attempts to solve the satisfaction problem by trying random models until time runs out and returning the best one.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

RandomSearchSatSolver

public RandomSearchSatSolver()

A constructor for this class.

Method Detail

solve

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

This routine attempts to solve the satisfaction problem by trying random models until time runs out and returning the best one.

Specified by:

solve in interface SatSolver

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

public java.lang.String author()

The author of this sat-solver.

Specified by:

author in interface SatSolver

description

public java.lang.String description()

A brief description of this sat-solver.

Specified by:

description in interface SatSolver