clausedenierdemo.java

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

package positronic.satisfiability.demos;

import positronic.satisfiability.elements.*;

public class ClauseDenierDemo
{
  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");

    IClause clause=new Clause().or(bva[0]).orNot(bva[1]).or(bva[2]);

    System.out.println("The given clause was "+clause+".");
    System.out.println("The denial of this clause is the following Problem:");
    System.out.println(new ClauseDenier(clause));
    
    System.out.println(new ClauseDenier(null));
    System.out.println(new ClauseDenier(new Clause()));
    System.out.println(new ClauseDenier(Problem.unsolvableProblem().getClause(0)));
  }
}