Class RandomSatisfiedCnfGenerator

java.lang.Object
  RandomSatisfiedCnfGenerator

All Implemented Interfaces:

Generator

public class RandomSatisfiedCnfGenerator
extends java.lang.Object
implements Generator

This Generator generates random satisfiable 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.

Constructor Summary

RandomSatisfiedCnfGenerator(int num_clauses, int num_symbols, int num_literals)
Constructor for this object.

Method Summary

java.lang.String	author() The author of this generator.
java.lang.String	description() A brief description of this generator.
Cnf	getNext() Generates another CNF of the specified form.
static void	main(java.lang.String[] argv) This is a simple main.

Methods inherited from class java.lang.Object

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

Constructor Detail

RandomSatisfiedCnfGenerator

public RandomSatisfiedCnfGenerator(int num_clauses,
                                   int num_symbols,
                                   int num_literals)

Constructor for this object.

Parameters:

num_clauses - number of clauses in constructed CNF

num_symbols - number of symbols (variables) in CNF

num_literals - number of literals per clause

Method Detail

getNext

public Cnf getNext()

Generates another CNF of the specified form.

Specified by:

getNext in interface Generator

author

public java.lang.String author()

The author of this generator.

Specified by:

author in interface Generator

description

public java.lang.String description()

A brief description of this generator.

Specified by:

description in interface Generator

main

public static void main(java.lang.String[] argv)

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.