bitstringlistuniquerdemo.java

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

package positronic.satisfiability.demos;

import java.util.List;

import positronic.satisfiability.bitstring.BitString;
import positronic.satisfiability.bitstring.IBitString;
import positronic.satisfiability.bitstringlist.BitStringList;
import positronic.satisfiability.bitstringlist.BitStringListFixer;
import positronic.satisfiability.bitstringlist.BitStringListUniquer;
import positronic.satisfiability.bitstringlist.IBitStringList;
import positronic.satisfiability.elements.BooleanLiteral;
import positronic.satisfiability.elements.Conjunction;
import positronic.satisfiability.elements.IProblem;
import positronic.satisfiability.solutions.PartialSolution;

public class BitStringListUniquerDemo/*questionable*/
{
	public static void main(String[] args) throws Exception
	{
		IBitStringList A=new BitStringList("A",new IBitString[]
	  {
	    new BitString("010"),
	    new BitString("110"),
	    new BitString("010"),
	    new BitString("011")
	  });
	
	  IBitStringList B=new BitStringList("B",new IBitString[]
	  {
	  		new BitString("000"),
	  		new BitString("000"),
	      new BitString("000"),
	      new BitString("000")
	  });
	  
	  System.out.println(B);
	
	  IProblem p1=new BitStringListUniquer(A,B);
	  System.out.println(p1);
	  
	  IProblem problem=new Conjunction(
	  		new BitStringListUniquer(A,B),
	  			//new BitStringListSubsetter(B,A),
	  				new BitStringListFixer(A));
	
	  System.out.println(problem);
	
	  List s=PartialSolution.solveList(problem);
		if(s!=null && s.size()>0)
	  {
	    BooleanLiteral.interpret(s);
	    System.out.println("A = "+A);
	    System.out.println("B = "+B);
	  }
	  else
	    System.out.println("No solution.");
	}
}