naturalnumberorderer.java

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

package positronic.satisfiability.naturalnumber;

import positronic.satisfiability.elements.BitFixer;
import positronic.satisfiability.elements.Conjunction;
import positronic.satisfiability.elements.IProblem;
import positronic.satisfiability.elements.Problem;

public class NaturalNumberOrderer extends Problem implements IProblem
{
	private static final long serialVersionUID = 1L;
	
	private static int nNOCount;

	public NaturalNumberOrderer(INaturalNumber X, INaturalNumber Y) throws Exception
	{
		//X<=Y
		//There exists Z such that Y=X+Z
		INaturalNumber C=new NaturalNumber("NaturalNumberOrderer-"+ nNOCount++);
		IProblem p1=new NaturalNumberAdder(X,new NaturalNumber("NaturalNumberOrderer-"+ nNOCount++),Y,C);
		//Constrain overflow bit
		IProblem p2=new BitFixer(C.getBooleanVariable(INaturalNumber.LENGTH-1),false);
		this.setClauses(new Conjunction(p1,p2).getClauses());
	}
}