partialsolution.java

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

/**
 * <p>Title: TBS</p>
 * <p>Description: TBS</p>
 * <p>Copyright (c) 2005</p>
 * <p>Company: Positronic Software</p>
 * @author Kerry Michael Soileau
 * @version 1.0
 */
package positronic.satisfiability.solutions;

import java.util.ArrayList;
import java.util.List;
import java.util.Map;
import java.util.Stack;

import positronic.math.EquivalenceRelation;
import positronic.satisfiability.elements.BooleanLiteral;
import positronic.satisfiability.elements.Certificate;
import positronic.satisfiability.elements.Conjunction;
import positronic.satisfiability.elements.IBooleanLiteral;
import positronic.satisfiability.elements.IBooleanVariable;
import positronic.satisfiability.elements.ICertificate;
import positronic.satisfiability.elements.IClause;
import positronic.satisfiability.elements.IProblem;
import positronic.satisfiability.elements.Problem;
import positronic.satisfiability.exceptions.PartialSolutionException;
import positronic.util.ArrayListSet;


public class PartialSolution extends Certificate implements ICertificate
{
  public static Split bestSplit(IProblem prob) throws Exception
  {
    double bestMeasure=Double.MAX_VALUE;
    ArrayList bestSplit=null;
    IBooleanVariable bestBoolean=null;
    ArrayList vb=prob.getBooleanVariables();
    if(vb==null || vb.size()==0)
      return null;
    for(int i=0;i<vb.size();i++)
    {
      IBooleanVariable boo=(IBooleanVariable)vb.get(i);
      ArrayList split=split(prob,boo);
      int a=((ArrayList)split.get(0)).size();
      int b=((ArrayList)split.get(1)).size();
      int c=((ArrayList)split.get(2)).size();
      double measure=a+b+2*c;
      if(measure<bestMeasure)
      {
        bestBoolean=boo;
        bestSplit=split;
        bestMeasure=measure;
      }
    }

    return new Split(bestBoolean,new Problem((ArrayList)(bestSplit.get(0)))
    ,new Problem((ArrayList)(bestSplit.get(1))),new Problem((ArrayList)(bestSplit.get(2))));
  }
  public static PartialSolution prettyGoodSolver(IProblem problem) throws Exception
  {
    PartialSolution partialSolution=new PartialSolution(new ArrayListSet(),problem);
    PartialSolution partialSolution2=partialSolution.processSingletons();
    PartialSolution partialSolution3=partialSolution2.combineSinglyMatchingClauses1Pass();
    PartialSolution partialSolution4=partialSolution3.processSingletons();
    PartialSolution partialSolution5=partialSolution4.combineSinglyMatchingClauses1Pass();
    PartialSolution partialSolution6=partialSolution5.processSingletons();
    if(partialSolution6.getProblem()!=null)
      partialSolution6.getProblem().sort();
    PartialSolution partialSolution7=partialSolution6.processEquivalences();
    return partialSolution7;
  }

  public static PartialSolution singletonSqueezeSolve(IProblem p) throws Exception
  {
    PartialSolution ps=new PartialSolution(new ArrayListSet(),p);
    int oldsize=Integer.MIN_VALUE;
    while(oldsize<ps.getBooleanLiterals().size())
    {
      oldsize=ps.getBooleanLiterals().size();
      ps.eliminateSingletons();
      if(ps.getProblem()==null) break;
      ps.setProblem(ps.getProblem().combineSinglyMatchingClauses());
    }//end while
    if(ps.getProblem()==null) return ps;
    else
    {
      ps.processEquivalences();

      ps.eliminateComplementaryPairClauses();

      System.out.println("Presented to divide and conquer:");
      System.out.println(ps);
      ArrayList v=ps.divideAndConquer();
      ArrayList bl=ps.getBooleanLiterals();
      for(int i=0;i<v.size();i++)
        if(bl!=null)
          bl.add((IBooleanLiteral)v.get(i));
        else
          bl=v;
      ps.setProblem(null);
      return ps;
    }//end else
  }

  public static IBooleanLiteral[] solve(IProblem prob) throws Exception
  {
    List l=PartialSolution.solveList(prob);
    if(l!=null)
    {
      IBooleanLiteral[] res=new IBooleanLiteral[l.size()];
      for(int i=0;i<l.size();i++)
        res[i]=(IBooleanLiteral)l.get(i);
      return res;
    }
    else return null;
  }

  public static List solveList(IProblem prob) throws Exception
  {
  	if(prob==null || prob.isEmpty())
  		throw new PartialSolutionException("Null or empty IProblem was passed to method solveList.");
  	else
  	{
  		ArrayListSet solution=new ArrayListSet();
  		PartialSolution p=new PartialSolution(solution,prob);
  		return p.divideAndConquer();
  	}
  }

  public static ArrayList split(IProblem prob,IBooleanVariable b) throws Exception
  {
    ArrayList occursUnbarred=new ArrayList();
    ArrayList occursBarred=new ArrayList();
    ArrayList doesNotOccur=new ArrayList();
    IBooleanLiteral bUnbarred=BooleanLiteral.getBooleanLiteral(b,false);
    IBooleanLiteral bBarred=BooleanLiteral.getBooleanLiteral(b,true);
    for(int i=0;i<prob.numberOfClauses();i++)
    {
      IClause c=prob.getClause(i);
      if(c.contains(bUnbarred))
      {
        occursUnbarred.add(c);
        continue;
      }
      if(c.contains(bBarred))
      {
        occursBarred.add(c);
        continue;
      }
      doesNotOccur.add(c);
    }
    ArrayList ret=new ArrayList();
    ret.add(occursUnbarred);
    ret.add(occursBarred);
    ret.add(doesNotOccur);
    return ret;
  }
  
  private Map equations;
  private IProblem problem;

  public PartialSolution(ArrayListSet booleanLiterals,IProblem p)
  {
    super.setBooleanLiterals(booleanLiterals);
    this.setProblem(p);
  }

  public PartialSolution combineSinglyMatchingClauses1Pass() throws Exception
  {
    if(this.getProblem()!=null)
    {
      IProblem res=this.getProblem().combineSinglyMatchingClauses();
      this.setProblem(res);
    }
    return this;
  }

  public ArrayList divideAndConquer() throws Exception
  {
    ArrayList arl=divideAndConquer1();
    this.setBooleanLiterals((ArrayListSet)arl);
    return arl;
  }
  
  public ArrayList divideAndConquer1() throws Exception
  {
  	if(this.getProblem()!=null)
    {
      ProblemStack s=new ProblemStack();
      s.push(this);
      s.numberOfClauses+=this.getProblem().numberOfClauses();

      while(!s.empty())
      {
        PartialSolution ps=(PartialSolution)(s.pop());
        s.numberOfClauses-=ps.getProblem().numberOfClauses();

        ArrayList booleanLiterals=(ArrayList)(ps.getBooleanLiterals());
        Split split=PartialSolution.bestSplit(ps.getProblem());
        if(split!=null)
        {
          IBooleanVariable splitBooleanVariable=split.getBooleanVariable();
          IProblem absentProblem=split.getAbsent();
          IProblem unbarred=new Conjunction(split.getUnbarred().substitute(splitBooleanVariable,false),absentProblem);
          if(unbarred!=null && !unbarred.containsAnEmptyClause())
          {
            ArrayListSet v=(ArrayListSet)(booleanLiterals.clone());
            v.add(BooleanLiteral.getBooleanLiteral(splitBooleanVariable,true));

            if(unbarred.isEmpty())
              return v;
            else
            {
              PartialSolution par=new PartialSolution(v,unbarred);
              s.push(par);
              s.numberOfClauses+=par.getProblem().numberOfClauses();
            }
          }
          IProblem barred=new Conjunction(split.getBarred().substitute(splitBooleanVariable,true),absentProblem);
          if(barred!=null && !barred.containsAnEmptyClause())
          {
            ArrayListSet v=(ArrayListSet)(booleanLiterals.clone());
            v.add(BooleanLiteral.getBooleanLiteral(splitBooleanVariable,false));
            if(barred.isEmpty())
              return v;
            else
            {
              PartialSolution par=new PartialSolution(v,barred);
              s.push(par);
              s.numberOfClauses+=par.getProblem().numberOfClauses();
            }
          }
        }//end if
      }//end while
    }
    return null;
  }

  public void eliminateComplementaryPairClauses() throws Exception
  {
  	this.setProblem(this.getProblem().eliminateComplementaryPairClauses());
  }

  public PartialSolution eliminateOneSingleton() throws Exception
  {
    IProblem pp=this.getProblem();
    if(pp==null) return this;
    ArrayListSet gbl=(ArrayListSet)(super.getBooleanLiterals());
    for(int i=0;i<pp.numberOfClauses();i++)
    {
      IClause c=pp.getClause(i);
      if(c.isSingleton())
      {
        IBooleanLiteral ib=c.getLiteralAt(0);
        gbl.add(ib);
        IProblem md=pp.substitute(ib.getBooleanVariable(),!ib.isBarred());
        return new PartialSolution(gbl,md);
      }
    }
    return this;
  }

  public void eliminateSingletons() throws Exception
  {
    int oldsize=Integer.MIN_VALUE;
    while(super.getBooleanLiterals().size()>oldsize /*&& this.getProblem()!=null*/)
    {
      oldsize=super.getBooleanLiterals().size();
      PartialSolution res=this.eliminateOneSingleton();
      this.setProblem(res.getProblem());
      this.setBooleanLiterals(res.getBooleanLiterals());
    }
  }

  public boolean expressEquivalence(IClause c1, IClause c2) throws Exception
  {
    if(c1==null) return false;
    if(c1.size()!=2 || c2.size()!=2) return false;
    for(int i=0;i<c1.size();i++)
    {
      IBooleanLiteral ibl=c1.getLiteralAt(i).complement();
      if(!c2.contains(ibl))
        return false;
    }
    return true;
  }

  public java.util.Map getEquations()
  {
    return equations;
  }

  public IProblem getProblem()
  {
    return this.problem;
  }

  public PartialSolution processEquivalences() throws Exception
  {
    IProblem pp=this.getProblem();
    if(pp!=null)
    {
    EquivalenceRelation equiv=new EquivalenceRelation();
    for(int i=0;i<pp.numberOfClauses();i++)
    {
      IClause ci=pp.getClause(i);
      for(int j=0;j<pp.numberOfClauses();j++)
      {
        IClause cj=pp.getClause(j);
        if(expressEquivalence(cj,ci))
          if(!ci.getLiteralAt(0).equals((IBooleanLiteral)(cj.getLiteralAt(1))))
            equiv.add(ci.getLiteralAt(0),cj.getLiteralAt(1));
      }//end for
    }//end for

    Map q=this.getEquations();
    if(q==null)
      this.setEquations(equiv.toHashMap());
    else
      q.putAll(equiv.toHashMap());
    
    pp.substitute(this.getEquations());

    this.eliminateComplementaryPairClauses();
    }
    return this;
  }

  public PartialSolution processSingletons() throws Exception
  {
    if(this.getProblem()!=null)
    {
    	if(this.getProblem().size()==0) return this;
    	PartialSolution ps;
    	while(true)
    	{
    		int s=this.getProblem().size();
    		ps=eliminateOneSingleton();
    		if(ps.getProblem()==null) break;
    		if(ps.getProblem().size()==s) break;
    		this.setProblem(ps.getProblem());
    	}
    	return ps;
    }
    return this;
  }

  public void setEquations(java.util.Map equations)
  {
    this.equations = equations;
  }

  public void setProblem(IProblem p)
  {
    this.problem=p;
  }

}//end PartialSolution class definition

class ProblemStack extends Stack
{
  private static final long serialVersionUID = 1L;
  public int numberOfClauses;
}

class Split
{
  private static int splitCount;
  private IProblem absent;
  private IProblem barred;
  private IBooleanVariable booleanVariable;
  private IProblem unBarred;

  public Split(IBooleanVariable booleanVariable,IProblem unBarred,IProblem barred,IProblem absent)
  {
    this.booleanVariable=booleanVariable;
    this.unBarred=unBarred;
    this.barred=barred;
    this.absent=absent;
  }

  public IProblem getAbsent()
  {
    return this.absent;
  }

  public IProblem getBarred()
  {
    return this.barred;
  }

  public IBooleanVariable getBooleanVariable()
  {
    return this.booleanVariable;
  }

  public IProblem getUnbarred()
  {
    return this.unBarred;
  }

  public String toString()
  {
    String ret="Split "+ splitCount++ ;
    ret+="\nBoolean Variable: "+this.booleanVariable;
    ret+="\nunBarred IProblem: "+unBarred;
    ret+="\nbarred IProblem: "+barred;
    ret+="\nabsent IProblem: "+absent;
    return ret;
  }
}