problemdifferencerdemo.java

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

package positronic.satisfiability.demos;

import positronic.satisfiability.elements.BooleanVariable;
import positronic.satisfiability.elements.Clause;
import positronic.satisfiability.elements.IBooleanVariable;
import positronic.satisfiability.elements.IClause;
import positronic.satisfiability.elements.IProblem;
import positronic.satisfiability.elements.Problem;
import positronic.satisfiability.elements.ProblemDifferencer;

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

    bva[0]=BooleanVariable.getBooleanVariable("x_1");
    bva[1]=BooleanVariable.getBooleanVariable("x_2");
    bva[2]=BooleanVariable.getBooleanVariable("x_3");

    IProblem p1=new Problem(
    		new IClause[]
    		{
    				//new Clause().or(bva[0]).orNot(bva[1]).or(bva[2]),
    				new Clause().orNot(bva[0]).orNot(bva[1]).orNot(bva[2])
    		});
    IProblem p2=new Problem(
    		new IClause[]
    		{
    				new Clause().or(bva[0]).orNot(bva[1]).or(bva[2]),
    				new Clause().orNot(bva[0]).orNot(bva[1]).orNot(bva[2])
    		});
    System.out.println("The first IProblem was\n"+p1);
    System.out.println("The second IProblem was\n"+p2);
    System.out.println("The difference was\n"+new ProblemDifferencer(Problem.unsolvableProblem(),p2));
  }
}