naturalnumberadder.java

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

package positronic.satisfiability.naturalnumber;

import positronic.satisfiability.elements.*;
 /**
 * An extension of the Problem class which implements an adder of two
 * NaturalNumbers.
 *
 * In one way to use this class, one passes INaturalNumber X, INaturalNumber Y,
 * INaturalNumber Z and INaturalNumber C to the appropriate constructor. The
 * NaturalNumberAdder 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
 *
 * <p><tt>Problem p = new NaturalNumberAdder(X,Y,Z,C);</tt></p>
 *
 * is satisfied, the following truth equation will be satisfied:
 *
 * <p><tt>Z == X + Y</tt></p>
 *
 * and the carry bits will be found in C.
 *
 * If the carry bits are of no interest, one may instead write
 *
 * <p><tt>Problem p = new NaturalNumberAdder(X,Y,Z);</tt></p>
 *
 * @author  Kerry Michael Soileau
 * <blockquote><pre>
 * [e-mail]
 * http://web.wt.net/~ksoileau/index.htm
 * </pre></blockquote>
 * @version 1.2, 05/03/08
 * @see IBooleanVariable
 * @see IClause
 * @see IProblem
 * @see Problem
 */


public class NaturalNumberAdder extends Problem implements IProblem
{
    /**
     * 
     */
    private static final long serialVersionUID = 1L;
  public NaturalNumberAdder(INaturalNumber X, INaturalNumber Y, INaturalNumber Z, INaturalNumber C) throws Exception
  {
    IProblem p=new TwoBitAdder(Y.getBooleanVariable(0),X.getBooleanVariable(0),Z.getBooleanVariable(0),C.getBooleanVariable(0));
    for(int i=1;i<INaturalNumber.LENGTH;i++)
      p=new Conjunction(p,new ThreeBitAdder(C.getBooleanVariable(i-1),Y.getBooleanVariable(i),X.getBooleanVariable(i),Z.getBooleanVariable(i),C.getBooleanVariable(i)));
    for(int i=INaturalNumber.LENGTH;i<INaturalNumber.LENGTH;i++)
      p=new Conjunction(p,new TwoBitAdder(C.getBooleanVariable(i-1),Y.getBooleanVariable(i),Z.getBooleanVariable(i),C.getBooleanVariable(i)));
    this.setClauses(p.getClauses());
  }

  public NaturalNumberAdder(INaturalNumber X, INaturalNumber Y, INaturalNumber Z) throws Exception
  {
    this(X,Y,Z,new NaturalNumber());
  }
}