bitorderer.java

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

/*
 * BitOrderer.java	1.0 05/05/04
 *
 * Copyright 2005 Positronic Software.
 *
 *
 */
 /**
 * An extension of the Problem class which imposes a Boolean relation on two
 * IBooleanVariables.
 *
 * To explain this class, we first define a "sort" relation between two IBooleanVariables as follows:
 * x <= y means that either y==true or (x==false and y==false).
 *
 * Under this definition, the Problem instance p defined by
 *
 * <p><tt>Problem p=new BitOrderer(x,y);</tt></p>
 *
 * is satisfied if and only if the following Boolean relation is satisfied:
 *
 * <p><tt>x <= y</tt></p>
 *
 * meaning that either y==true or (x==false && y==false).
 *
 * @author  Kerry Michael Soileau
 * [e-mail]
 * http://web.wt.net/~ksoileau/index.htm
 * @version 1.0, 05/05/04
 * @see BitFixer
 * @see BooleanLiteralException
 * @see Conjunction
 * @see Disjunction
 * @see IBooleanVariable
 * @see IProblem
 * @see Problem
 */

package positronic.satisfiability.elements;

public class BitOrderer extends Problem implements IProblem
{
  private static final long serialVersionUID = 1L;
  
  public BitOrderer(IBooleanVariable x, IBooleanVariable y) throws Exception
  {
    //must have either y==true or (y==false && x==false)
    IProblem compare=new Disjunction(new BitFixer(y,true),
      new Conjunction(new BitFixer(y,false),new BitFixer(x,false)));
    this.setClauses(compare.getClauses());
  }
}