bitstringlistintersector.java

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

/*
 * BitStringListIntersector.java	1.0 05/10/20
 *
 * Copyright 2005 Positronic Software.
 *
 *
 */

package positronic.satisfiability.bitstringlist;

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.BitStringListException;

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

  public BitStringListIntersector(IBitStringList T,IBitStringList A,IBitStringList B) throws Exception
  {
    if(T==null || A==null || B==null)
      throw new BitStringListException("Passed null IBitStringList to BitStringListIntersecter constructor.");

    IProblem problem=null;
    for(int i=0;i<A.size();i++)
    {
      IBitString curr=A.getBitString(i);
      IProblem notInT=new BitStringListNonmembershipper(curr,T);
      IProblem inA=new BitStringListMembershipper(curr,A);
      IProblem inB=new BitStringListMembershipper(curr,B);
      IProblem notInA=new BitStringListNonmembershipper(curr,A);
      IProblem notInB=new BitStringListNonmembershipper(curr,B);
      IProblem inT=new BitStringListMembershipper(curr,T);
      problem=new Conjunction(
      		new IProblem[]
      		{
      				problem,
      				new Disjunction(notInT,inA),
      				new Disjunction(notInT,inB),
      				new Disjunction(notInA,inT),
      				new Disjunction(notInB,inT)
      		});
    }
    for(int i=0;i<B.size();i++)
    {
      IBitString curr=B.getBitString(i);
      IProblem notInT=new BitStringListNonmembershipper(curr,T);
      IProblem inA=new BitStringListMembershipper(curr,A);
      IProblem inB=new BitStringListMembershipper(curr,B);
      IProblem notInA=new BitStringListNonmembershipper(curr,A);
      IProblem notInB=new BitStringListNonmembershipper(curr,B);
      IProblem inT=new BitStringListMembershipper(curr,T);
      problem=new Conjunction(
      		new IProblem[]
      		{
      				problem,
      				new Disjunction(notInT,inA),
      				new Disjunction(notInT,inB),
      				new Disjunction(notInA,inT),
      				new Disjunction(notInB,inT)
      		});
    }
    this.setClauses(problem.getClauses());
  }
}