clausedemo.java

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

package positronic.satisfiability.demos;

import positronic.satisfiability.elements.*;

public class ClauseDemo
{
  public static void main(String[] args) throws Exception
  {
    IClause[] clause=new IClause[3];
    IBooleanVariable[] bva=new IBooleanVariable[4];

    clause[0] = new Clause();
    clause[1] = new Clause();
    clause[2] = new Clause();

    bva[0]=BooleanVariable.getBooleanVariable("foo30");
    bva[1]=BooleanVariable.getBooleanVariable("foo11");
    bva[2]=BooleanVariable.getBooleanVariable("foo23");
    bva[3]=BooleanVariable.getBooleanVariable("foo83");

    clause[0].orNot(bva[0]);
    clause[0].or(bva[1]);
    clause[0].or(bva[2]);

    clause[1].or(bva[0]);
    clause[1].or(bva[3]);
    clause[1].orNot(bva[2]);

    clause[2].or(bva[1]);
    clause[2].or(bva[3]);
    clause[2].or(bva[2]);

    System.out.println("clause[0].equals(clause[0]) is "+clause[0].equals(clause[0]));
    System.out.println("clause[0].equals(clause[1]) is "+clause[0].equals(clause[1]));
    System.out.println("clause[0].equals(clause[2]) is "+clause[0].equals(clause[2]));

    System.out.println("clause[1].equals(clause[0]) is "+clause[1].equals(clause[0]));
    System.out.println("clause[1].equals(clause[1]) is "+clause[1].equals(clause[1]));
    System.out.println("clause[1].equals(clause[2]) is "+clause[1].equals(clause[2]));

    System.out.println("clause[2].equals(clause[0]) is "+clause[2].equals(clause[0]));
    System.out.println("clause[2].equals(clause[1]) is "+clause[2].equals(clause[1]));
    System.out.println("clause[2].equals(clause[2]) is "+clause[2].equals(clause[2]));

    System.out.println(clause[0]);
    System.out.println(clause[1]);
    System.out.println(clause[2]);

    System.out.println("-----------------------------------");
    System.out.println(clause[0].resolve(bva[1],false));
    System.out.println(clause[1].resolve(bva[1],false));
    System.out.println(clause[2].resolve(bva[1],false));

    System.out.println("-----------------------------------");
    System.out.println(clause[0]);
    IBooleanVariable iv=BooleanVariable.getBooleanVariable("foo23");
    IBooleanLiteral il=BooleanLiteral.getBooleanLiteral(iv,true);
    System.out.println(il);
    IClause newc=clause[0].resolve(iv,false);
    System.out.println(newc);
    IClause newc2=clause[0].resolve(il);
    System.out.println(newc2);
  }
}