bitstringlistincrementer.java

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

package positronic.satisfiability.bitstringlist;

import positronic.satisfiability.bitstring.BitStringEqualizer;
import positronic.satisfiability.bitstring.IBitString;
import positronic.satisfiability.elements.Conjunction;
import positronic.satisfiability.elements.Disjunction;
import positronic.satisfiability.elements.IProblem;
import positronic.satisfiability.elements.Problem;
import positronic.satisfiability.exceptions.BitStringListIncrementerException;

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

	public BitStringListIncrementer(IBitStringList X, IBitString I, IBitStringList Y) throws Exception
	{
		if(X==null || Y==null)
      throw new BitStringListIncrementerException("Passed a null IBitStringList to a constructor.");
		if(I==null)
      throw new BitStringListIncrementerException("Passed a null IBitString to a constructor.");
		IProblem problem=new Conjunction(new BitStringListMembershipper(I,Y),
				new BitStringListNonmembershipper(I,X));
		for(int i=0;i<X.size();i++)
		{
			IBitString curr=X.getBitString(i);
			IProblem p=new Disjunction(
					new BitStringListNonmembershipper(curr,Y),
					new BitStringEqualizer(curr,I),
					new BitStringListMembershipper(curr,X)
					);
			problem=new Conjunction(problem,p);
		}
		for(int i=0;i<Y.size();i++)
		{
			IBitString curr=Y.getBitString(i);
			IProblem p=new Disjunction(
					new BitStringListNonmembershipper(curr,Y),
					new BitStringEqualizer(curr,I),
					new BitStringListMembershipper(curr,X)
					);
			problem=new Conjunction(problem,p);
		}
		
		this.setClauses(problem.getClauses());
	}
}

/*package positronic.satisfiability.arrays;

import positronic.satisfiability.elements.Conjunction;
import positronic.satisfiability.elements.Disjunction;
import positronic.satisfiability.elements.IProblem;
import positronic.satisfiability.elements.Problem;
import positronic.satisfiability.exceptions.BitStringListIncrementerException;

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

	public BitStringListIncrementer(IBitStringList X, IBitString I, IBitStringList Y) throws Exception
	{
		if(X==null || Y==null)
      throw new BitStringListIncrementerException("Passed a null IBitStringList to a constructor.");
		if(I==null)
      throw new BitStringListIncrementerException("Passed a null IBitString to a constructor.");
		IProblem problem=null;
		for(int i=0;i<X.size();i++)
		{
			IBitString curr=X.getBitString(i);
			IProblem p1=new Disjunction(
					new BitStringListNonmembershipper(curr,Y),
					new BitStringListMembershipper(curr,X),
					new BitStringEqualizer(curr,I));
			problem=new Conjunction(problem,p1);
			IProblem p2=new Disjunction(
					new BitStringListNonmembershipper(curr,X),
					new BitStringUnequalizer(curr,I));
			problem=new Conjunction(problem,p2);
			IProblem p3=new Disjunction(
					new BitStringListMembershipper(curr,Y),
					new BitStringListNonmembershipper(curr,X));
			IProblem p4=new Disjunction(
					new BitStringListMembershipper(curr,Y),
					new BitStringUnequalizer(curr,I));
			problem=new Conjunction(problem,p3,p4);
		}
		for(int i=0;i<Y.size();i++)
		{
			IBitString curr=Y.getBitString(i);
			IProblem p1=new Disjunction(
					new BitStringListNonmembershipper(curr,Y),
					new BitStringListMembershipper(curr,X),
					new BitStringEqualizer(curr,I));
			problem=new Conjunction(problem,p1);
			IProblem p2=new Disjunction(
					new BitStringListNonmembershipper(curr,X),
					new BitStringUnequalizer(curr,I));
			problem=new Conjunction(problem,p2);
			IProblem p3=new Disjunction(
					new BitStringListMembershipper(curr,Y),
					new BitStringListNonmembershipper(curr,X));
			IProblem p4=new Disjunction(
					new BitStringListMembershipper(curr,Y),
					new BitStringUnequalizer(curr,I));
			problem=new Conjunction(problem,p3,p4);
		}
	
		IBitString curr=I;
		IProblem p1=new Disjunction(
				new BitStringListNonmembershipper(curr,Y),
				new BitStringListMembershipper(curr,X),
				new BitStringEqualizer(curr,I));
		problem=new Conjunction(problem,p1);
		IProblem p2=new Disjunction(
				new BitStringListNonmembershipper(curr,X),
				new BitStringUnequalizer(curr,I));
		problem=new Conjunction(problem,p2);
		IProblem p3=new Disjunction(
				new BitStringListMembershipper(curr,Y),
				new BitStringListNonmembershipper(curr,X));
		IProblem p4=new Disjunction(
				new BitStringListMembershipper(curr,Y),
				new BitStringUnequalizer(curr,I));
		problem=new Conjunction(problem,p3,p4);
		
		this.setClauses(problem.getClauses());
	}
}
*/