bitxnorer.java

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

/*
 * BitXnorer.java	1.0 05/04/13
 *
 * Copyright 2004-2005 Positronic Software.
 *
 *
 */

package positronic.satisfiability.elements;

/**
 * An extension of the Problem class which implements a Boolean function. This
 * function has the value false if the BooleanVariables x and y are both true;
 * otherwise it has the value true. The returned function value is found
 * in the IBooleanVariable z.
 *
 * To use this class, one passes BooleanVariables x, y, and z to the
 * constructor. The BitXnorer object produced is a Problem, and one may
 * manipulate it using any of the methods provided by the Problem class.
 *
 * For example, when the Problem instance p defined by
 *
 * Problem p=new BitXnorer(x,y,z);
 *
 * is satisfied, the following truth equation will be satisfied:
 *
 * z == ( x ^ y ) | ( !x ^ !y )
 *
 * @author  Kerry Michael Soileau
 * [e-mail]
 * http://web.wt.net/~ksoileau/index.htm
 * @version 1.0, 05/04/13
 * @see IBooleanVariable
 * @see IClause
 * @see Problem
 */

public class BitXnorer extends Problem implements IProblem
{
  private static final long serialVersionUID = 1L;
  
  public BitXnorer(IBooleanVariable x, IBooleanVariable y, IBooleanVariable z) throws Exception
  {
    this.setClauses(new IClause[]
    {
    	Clause.newClause().or(x).or(y).or(z),
    	Clause.newClause().or(x).orNot(y).orNot(z),
    	Clause.newClause().orNot(x).or(y).orNot(z),
    	Clause.newClause().orNot(x).orNot(y).or(z)
    });
  }
}