naturalnumberfactorerdemo.java

来自「Java版的SAT求解器」· Java 代码 · 共 58 行

package positronic.satisfiability.demos;

/**
 * <p>Title: TBS</p>
 * <p>Description: TBS</p>
 * <p>Copyright: Copyright (c) 2005</p>
 * <p>Company: Positronic Software</p>
 * @author Kerry Michael Soileau
 * @version 1.0
 */
import positronic.satisfiability.elements.BooleanVariable;
import positronic.satisfiability.elements.Conjunction;
import positronic.satisfiability.elements.IProblem;
import positronic.satisfiability.naturalnumber.INaturalNumber;
import positronic.satisfiability.naturalnumber.NaturalNumber;
import positronic.satisfiability.naturalnumber.NaturalNumberFactorer;
import positronic.satisfiability.naturalnumber.NaturalNumberFixer;
import positronic.satisfiability.solutions.PartialSolution;
import positronic.util.ArrayListSet;

public class NaturalNumberFactorerDemo
{
  public static void main(String[] args) throws Exception
  {
    INaturalNumber X=new NaturalNumber("X");
    INaturalNumber Y=new NaturalNumber("Y");
    INaturalNumber Z=new NaturalNumber("Z");

    NaturalNumberFixer bnnfz=new NaturalNumberFixer(Z,4L);
    NaturalNumberFactorer NaturalNumberFactorer1 = new NaturalNumberFactorer(X,Y,Z);

    IProblem p=new Conjunction(bnnfz,NaturalNumberFactorer1);
    
    BooleanVariable.listVariables();
    System.out.println(p);
    PartialSolution foo=new PartialSolution(new ArrayListSet(),p);
    System.out.println(foo);
    PartialSolution foo2=foo.processSingletons();
    System.out.println(foo2);
    PartialSolution foo3=foo2.combineSinglyMatchingClauses1Pass();
    System.out.println(foo3);
    PartialSolution foo4=foo3.processSingletons();
    System.out.println("After processing singletons again..."+foo4);
    PartialSolution foo5=foo4.combineSinglyMatchingClauses1Pass();
    System.out.println(foo5);
    PartialSolution foo6=foo5.processSingletons();
    foo6.getProblem().sort();
    System.out.println("After processing singletons again..."+foo6);
    PartialSolution foo7=foo6.processEquivalences();
    System.out.println("After processing equivalences..."+foo7);

    PartialSolution res=PartialSolution.prettyGoodSolver(p);
    System.out.println(res);
    java.util.List list=PartialSolution.solveList(res.getProblem());
    System.out.println(list);
    System.out.println("Finis");
  }
}