mapperdemo1.java

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

package positronic.satisfiability.demos;

import java.util.List;

import positronic.satisfiability.elements.BooleanLiteral;
import positronic.satisfiability.elements.BooleanVariable;
import positronic.satisfiability.elements.Conjunction;
import positronic.satisfiability.elements.IBooleanVariable;
import positronic.satisfiability.elements.IProblem;
import positronic.satisfiability.elements.Mapper;
import positronic.satisfiability.elements.ProblemPair;
import positronic.satisfiability.naturalnumber.INaturalNumber;
import positronic.satisfiability.naturalnumber.NaturalNumber;
import positronic.satisfiability.naturalnumber.NaturalNumberFixer;
import positronic.satisfiability.naturalnumber.NaturalNumberIncrementer;
import positronic.satisfiability.solutions.PartialSolution;
/**
 * <p>Title: MapperDemo1</p>
 * <p>Description: TBS</p>
 * <p>Copyright (c) 2005</p>
 * <p>Company: Positronic Software</p>
 * @author Kerry Michael Soileau
 * @version 1.0
 */

public class MapperDemo1
{
  public static void main(String[] args) throws Exception
  {
    INaturalNumber x=new NaturalNumber("x");
    INaturalNumber y=new NaturalNumber("y");
    INaturalNumber z=new NaturalNumber("z");
    
    IBooleanVariable[] b=new IBooleanVariable[11];
    for(int i=0;i<b.length;i++)
    	b[i]=BooleanVariable.getBooleanVariable("b"+i);
    Mapper map1 = new Mapper(
    		new ProblemPair[]
    		    {
    					new ProblemPair(new NaturalNumberFixer(x,1),new NaturalNumberFixer(y,31)),
    					new ProblemPair(new NaturalNumberFixer(x,2),new NaturalNumberFixer(y,28)),
    					new ProblemPair(new NaturalNumberFixer(x,3),new NaturalNumberFixer(y,31)),
    					new ProblemPair(new NaturalNumberFixer(x,4),new NaturalNumberFixer(y,30)),
    					new ProblemPair(new NaturalNumberFixer(x,5),new NaturalNumberFixer(y,31)),
    					new ProblemPair(new NaturalNumberFixer(x,6),new NaturalNumberFixer(y,30)),
    					new ProblemPair(new NaturalNumberFixer(x,7),new NaturalNumberFixer(y,31)),
    					new ProblemPair(new NaturalNumberFixer(x,8),new NaturalNumberFixer(y,31)),
    					new ProblemPair(new NaturalNumberFixer(x,9),new NaturalNumberFixer(y,30)),
    					new ProblemPair(new NaturalNumberFixer(x,10),new NaturalNumberFixer(y,31)),
    					new ProblemPair(new NaturalNumberFixer(x,11),new NaturalNumberFixer(y,30)),
    					new ProblemPair(new NaturalNumberFixer(x,12),new NaturalNumberFixer(y,31))
    				},
    				b);
    IBooleanVariable[] c=new IBooleanVariable[11];
    for(int i=0;i<c.length;i++)
    	c[i]=BooleanVariable.getBooleanVariable("c"+i);
    Mapper map2 = new Mapper(
    		new ProblemPair[]
    		    {
    					new ProblemPair(new NaturalNumberFixer(z,1),new NaturalNumberFixer(y,31)),
    					new ProblemPair(new NaturalNumberFixer(z,2),new NaturalNumberFixer(y,28)),
    					new ProblemPair(new NaturalNumberFixer(z,3),new NaturalNumberFixer(y,31)),
    					new ProblemPair(new NaturalNumberFixer(z,4),new NaturalNumberFixer(y,30)),
    					new ProblemPair(new NaturalNumberFixer(z,5),new NaturalNumberFixer(y,31)),
    					new ProblemPair(new NaturalNumberFixer(z,6),new NaturalNumberFixer(y,30)),
    					new ProblemPair(new NaturalNumberFixer(z,7),new NaturalNumberFixer(y,31)),
    					new ProblemPair(new NaturalNumberFixer(z,8),new NaturalNumberFixer(y,31)),
    					new ProblemPair(new NaturalNumberFixer(z,9),new NaturalNumberFixer(y,30)),
    					new ProblemPair(new NaturalNumberFixer(z,10),new NaturalNumberFixer(y,31)),
    					new ProblemPair(new NaturalNumberFixer(z,11),new NaturalNumberFixer(y,30)),
    					new ProblemPair(new NaturalNumberFixer(z,12),new NaturalNumberFixer(y,31))
    				},
    				c);
    
    IProblem nni=new NaturalNumberIncrementer(x,z);
    IProblem problem=new Conjunction(nni,map1,map2);
    System.out.println(problem);
    
    List s=PartialSolution.solveList(problem);
    
		if(s!=null && s.size()>0)
    {
      BooleanLiteral.interpret(s);
    	System.out.println("x= "+x);
    	System.out.println("y= "+y);
    	System.out.println("z= "+z);
    	
    	for(int i=0;i<b.length;i++)
    	{
    		System.out.println("b["+i+"]= "+b[i].getValue());
    	}
    }
    else
      System.out.println("No solution.");
  }
}