naturalnumbermultiplier.java

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

package positronic.satisfiability.naturalnumber;

/**
 * <p>Title: NaturalNumberMultiplier</p>
 * <p>Description: TBS</p>
 * <p>Copyright (c) 2005</p>
 * <p>Company: Positronic Software</p>
 * @author Kerry Michael Soileau
 * @version 1.0
 */
import positronic.satisfiability.elements.*;

public class NaturalNumberMultiplier extends Problem implements IProblem
{
  private static final long serialVersionUID = 1L;
  
  public NaturalNumberMultiplier(INaturalNumber X, INaturalNumber Y, INaturalNumber Z) throws Exception
  {
    if(INaturalNumber.LENGTH==1)
    {
      NaturalNumberBitMultiply p=new NaturalNumberBitMultiply(X.getBooleanVariable(0),Y,Z);
      this.setClauses(p.getClauses());
    }
    if(INaturalNumber.LENGTH>=2)
    {
      //P
      INaturalNumber[] P=new INaturalNumber[INaturalNumber.LENGTH];
      for(int i=0;i<INaturalNumber.LENGTH;i++)
        P[i]=new NaturalNumber("P["+i+"]");
      NaturalNumberBitMultiply[] qbs=new NaturalNumberBitMultiply[INaturalNumber.LENGTH];
      for(int i=0;i<INaturalNumber.LENGTH;i++)
        qbs[i]=new NaturalNumberBitMultiply(X.getBooleanVariable(i),Y,P[i]);
      //D
      INaturalNumber[] D=new INaturalNumber[INaturalNumber.LENGTH-1];
      for(int i=0;i<INaturalNumber.LENGTH-1;i++)
        D[i]=new NaturalNumber("D["+i+"]");
      NaturalNumberDoubler[] tdblr=new NaturalNumberDoubler[INaturalNumber.LENGTH-1];
      INaturalNumber[] S=new INaturalNumber[INaturalNumber.LENGTH-2];
      for(int i=0;i<INaturalNumber.LENGTH-2;i++)
        S[i]=new NaturalNumber("S["+i+"]");
      for(int i=0;i<INaturalNumber.LENGTH-2;i++)
        tdblr[i]=new NaturalNumberDoubler(S[i],D[i]);
      tdblr[INaturalNumber.LENGTH-2]=new NaturalNumberDoubler(P[INaturalNumber.LENGTH-1],D[INaturalNumber.LENGTH-2]);
      //S
      NaturalNumberAdder[] waddr=new NaturalNumberAdder[INaturalNumber.LENGTH-2];
      for(int i=0;i<INaturalNumber.LENGTH-2;i++)
        waddr[i]=new NaturalNumberAdder(P[i+1],D[i+1],S[i]);
      NaturalNumberAdder zaddr=new NaturalNumberAdder(P[0],D[0],Z);

      IProblem qbsc=new Conjunction(qbs);
      IProblem tdblrc=new Conjunction(tdblr);
      IProblem waddrc=new Conjunction(waddr);
      IProblem p=new Conjunction(new IProblem[]{qbsc,tdblrc,waddrc,zaddr});

      this.setClauses(p.getClauses());
    }
  }
}