bitordererdemo.java

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

package positronic.satisfiability.demos;

import positronic.satisfiability.elements.*;
import positronic.satisfiability.solutions.*;

public class BitOrdererDemo
{
  public static void main(String[] args) throws Exception
  {
    // Create the BooleanVariables:
    IBooleanVariable x=BooleanVariable.getBooleanVariable("x");
    IBooleanVariable y=BooleanVariable.getBooleanVariable("y");

    // Construct the object that implements the constraint x <= y :
    IProblem bitOrderer1 = new BitOrderer(x,y);
    System.out.println(bitOrderer1);

    // Constrain the values of x and y :
    IProblem bfx1=new BitFixer(x,true);
    IProblem bfy1=new BitFixer(y,false);

    //Combine the constraints into a Problem object :
    IProblem p1=new Conjunction(bitOrderer1,bfx1,bfy1);
    System.out.println(p1);
    //Find a solution to the Problem object :
    java.util.List v1=PartialSolution.solveList(p1);
    System.out.println(v1);
  }
}