bitanderdemo.java

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

package positronic.satisfiability.demos;

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

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

    // Construct the object that implements the constraint x & y = z :
    IProblem bitAnder1 = new BitAnder(x,y,z);
    System.out.println(bitAnder1);

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

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

    // false & true = z has solution z = false:
    IProblem p2=new Conjunction(bitAnder1,new BitFixer(x,false),new BitFixer(y,true));
    System.out.println(p2);
    java.util.List v2=PartialSolution.solveList(p2);
    System.out.println(v2);

    // true & false = z has solution z = false:
    IProblem p3=new Conjunction(bitAnder1,new BitFixer(x,true),new BitFixer(y,false));
    System.out.println(p3);
    java.util.List v3=PartialSolution.solveList(p3);
    System.out.println(v3);

    // true & true = z has solution z = true:
    IProblem p4=new Conjunction(bitAnder1,new BitFixer(x,true),new BitFixer(y,true));
    System.out.println(p4);
    java.util.List v4=PartialSolution.solveList(p4);
    System.out.println(v4);

    // true & y = true has solution y = true:
    IProblem p5=new Conjunction(bitAnder1,new BitFixer(x,true),new BitFixer(z,true));
    System.out.println(p5);
    java.util.List v5=PartialSolution.solveList(p5);
    System.out.println(v5);

    // true & y = false has solution y = false:
    IProblem p6=new Conjunction(bitAnder1,new BitFixer(x,true),new BitFixer(z,false));
    System.out.println(p6);
    java.util.List v6=PartialSolution.solveList(p6);
    System.out.println(v6);
    BooleanLiteral.interpret(PartialSolution.solveList(p6));
    System.out.println("----!------------");
    System.out.println("x = "+x.getValue());
    System.out.println("y = "+y.getValue());
    System.out.println("z = "+z.getValue());

    // false & y = true has no solution:
    IProblem p7=new Conjunction(bitAnder1,new BitFixer(x,false),new BitFixer(z,true));
    System.out.println(p7);
    java.util.List v7=PartialSolution.solveList(p7);
    System.out.println(v7);
    
    //System.out.println(p1.toXML());
  }
}