problemdemo.java

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

package positronic.satisfiability.demos;

import java.util.*;
import positronic.satisfiability.elements.*;
import positronic.satisfiability.naturalnumber.*;
import positronic.satisfiability.solutions.*;

public class ProblemDemo
{
  public static void main(String[] args) throws Exception
  {
    IBooleanVariable b=BooleanVariable.getBooleanVariable("b");

    NaturalNumber X=new NaturalNumber("X");
    NaturalNumber Y=new NaturalNumber("Y");

    //Stipulate that b=false
    BitFixer bf=new BitFixer(b,false);
    //Stipulate that Y=3
    NaturalNumberFixer nnfx=new NaturalNumberFixer(Y,3);

    //nndxy <-> 2X=Y
    NaturalNumberDoubler nndxy=new NaturalNumberDoubler(X,Y);
    //nndyx <-> 2Y=X
    NaturalNumberDoubler nndyx=new NaturalNumberDoubler(Y,X);

    //Stipulate that ptrue = nndxy && nnfx
    IProblem ptrue=new Conjunction(nndxy,nnfx);

    //Stipulate that pfalse = nndyx && nnfx
    IProblem pfalse=new Conjunction(nndyx,nnfx);

    //Stipulate that qq = ptrue || pfalse
    IProblem qq=new Disjunction(ptrue,pfalse,b);

    //Stipulate that pp = qq && bf
    IProblem pp=new Conjunction(qq,bf);

    pp.sort();
    System.out.println(pp);
    List s=PartialSolution.solveList(pp);
		if(s!=null && s.size()>0)
    {
      BooleanLiteral.interpret(s);
    	System.out.println("X= "+X);
    	System.out.println("Y= "+Y);
    }
    else
      System.out.println("No solution.");
    
    Problem p1=new Problem();
    System.out.println(p1);
    IProblem p2=Problem.unsolvableProblem();
    System.out.println(p2);
    IProblem p3=Problem.trivialProblem();
    System.out.println(p3);
  }
}