problems.java

Java版的SAT求解器

/*
 * Problems.java	1.0 04/09/06
 *
 * Copyright 2004-2005 Positronic Software.
 *
 *
 */
package positronic.satisfiability.elements;

import java.util.*;
import positronic.satisfiability.exceptions.*;
import positronic.math.*;

/**
 * An iterator over all possible Problems.
 *
 * To use this class, one passes a collection of BooleanVariables to one of the
 * constructors. The Problems object produced is an Iterator, and one may use its
 * hasNext and next methods to produce all possible problems over the given
 * collection. Each application of the next method produces an instance of the
 * IProblem class; this instance contains a problem over the given collection.
 *
 * @author  Kerry Michael Soileau
 * [e-mail]
 * http://web.wt.net/~ksoileau/index.htm
 * @version 1.0, 04/09/06
 * @see ArrayList
 * @see Collection
 * @see Iterator
 * @see Vector
 */
public class Problems
{
  public Problem[] problem;

  public Problems(Object[] bv) throws BooleanLiteralException
  {
    System.out.println("There are "+bv.length+" BooleanVariables in this example.");
    Clauses cl=new Clauses(bv);
    Object[] clob=cl.toArray();
    System.out.println("This produces "+clob.length+" Clauses.");
    PowerSet ps=new PowerSet(clob);
    int p=(int)Math.pow(2.,clob.length);
    System.out.println("This produces "+p+" Problems.");
    problem=new Problem[p];
    for(int i=0;i<problem.length && ps.hasNext();i++)
    {
      problem[i]=new Problem((ArrayList)ps.next());
      problem[i].sort();
    }
  }
}