problem.java

Java版的SAT求解器

/*
 * Problem.java	1.3 05/11/30
 *
 * Copyright 2004-2005 Positronic Software.
 *
 *
 */

package positronic.satisfiability.elements;

import java.io.File;
import java.io.FileOutputStream;
import java.io.PrintStream;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Iterator;
import java.util.List;
import java.util.Map;

import positronic.math.EquivalenceRelation;
import positronic.satisfiability.naturalnumber.NaturalNumber;

/**
 * A class which represents a collection of IClause objects, and which amounts
 * to a satisfiability problem. Problem is essentially a ArrayList of IClause
 * objects, and additionally provides several useful methods for combining
 * Problem objects, especially performing logical operations such as
 * <tt>and</tt> and <tt>or</tt> on such objects.
 *
 * This class is the superclass of numerous generic satisfiability problems.
 *
 * @author  Kerry Michael Soileau
 * <blockquote><pre>
 * [e-mail]
 * http://web.wt.net/~ksoileau/index.htm
 * </pre></blockquote>
 * @version 1.3, 05/10/07
 * @see IClause
 * @see IBooleanVariable
 * @see IBooleanLiteral
 * @see NaturalNumber
 * @see BitAnder
 * @see BitEqualityIndicator
 * @see BitEqualizer
 * @see BitFixer
 * @see BitInequalityIndicator
 * @see BitNoter
 * @see BitOrer
 * @see BitXorer
 */

public class Problem extends ArrayList implements IProblem
{
	private static int problemCount;
  private static final long serialVersionUID = 1L;
  private static PrintStream stream = System.out;

	public static IProblem newProblem()
	{
	  return (IProblem)new Problem();
	}

	public static IProblem randomProblem(IBooleanVariable[] bv, int n) throws Exception
	{
	  Problem p=new Problem();
	  for(int i=0;i<n;i++)
	    p.addClause(Clause.randomClause(bv));
	  for(int i=0;i<p.numberOfClauses();i++)
	    if(p.getClause(i).isEmpty())
	      p.removeClause(i);
	  //p.sortClauses();
	  return p;
	}

  public static IProblem trivialProblem()
  {
  	return new Problem(new IClause[]{null});
  }

  public static IProblem unsolvableProblem()
	{
	  return new Problem(new IClause[]{new Clause()});
	}

  /**
	 * Constructs an empty Problem, that is, an instance of Problem which contains
	 * no IClauses.
	 */
  public Problem()
  {
  }

  /**
	 * Constructs an instance of Problem which contains the IClauses found in the
	 * parameter v.
	 * @param v the ArrayList of IClauses to comprise the instance of Problem.
	 */
	public Problem(ArrayList v)
	{
	  if(v!=null)
	  {
	    for(int i=0;i<v.size();i++)
	    {
	      Object o=v.get(i);
	      if(o instanceof IClause)
	      {
	        IClause c=(IClause)o;
	        this.addClause(c);
	      }
	    }
	  }
	}
	
	/**
	 * Constructs an instance of Problem which contains the IClauses found in the
	 * parameter clause.
	 * @param clause the array of IClauses to comprise the instance of Problem.
	 */
	public Problem(IClause[] clause)
	{
	  this.setClauses(clause);
	}

  public Problem(IProblem iproblem)
	{
	  this.setClauses(iproblem.getClauses());
	}

  public boolean addClause(IClause c)
  {
  	if(c==null)
  		return false;
    if(!this.contains(c))
    {
      super.add(c);
      return true;
    }
    else
      return false;
  }

  public void addClause(IClause[] c)
  {
    if(c==null || c.length==0) return;
    for(int i=0;i<c.length;i++)
      this.addClause(c[i]);
  }

  public IProblem and(IProblem p)
  {
    return new Conjunction(new IProblem[]{p,this});
  }

  /*
  public void sort()
  {
    Object[] ary=this.toArray();
    Arrays.sort(ary);
    IClause[] iary=new IClause[ary.length];
    for(int i=0;i<iary.length;i++)
      iary[i]=(IClause)ary[i];
    this.setClauses(iary);
  }
  */

  public EquivalenceRelation buildEquivalenceRelation()
  {
    EquivalenceRelation e=new EquivalenceRelation();

    for(int i=0;i<this.numberOfClauses();i++)
    {
      Object[] objary=this.getClause(i).getBooleanVariables();
      for(int j=0;j<objary.length;j++)
        for(int k=0;k<objary.length;k++)
          e.add(objary[j],objary[k]);
    }
    return e;
  }

  public Object clone()
  {
    Object[] cobj=this.getClauses();
    IClause[] clauses=new IClause[cobj.length];
    for(int i=0;i<cobj.length;i++)
      clauses[i]=(IClause)(cobj[i]);
    IProblem res=new Problem(clauses);
    return res;
  }

  public IProblem combineSinglyMatchingClauses() throws Exception
  {
  	int psize=this.size();
  	IProblem ret=Problem.newProblem();
  	for(int i=0;i<psize;i++)
  	{
  		IClause clausei=this.getClause(i);
  		boolean newclausecreated=false;
  		for(int j=0;j<psize;j++)
  		{
  			IClause clausej=this.getClause(j);
  			IBooleanLiteral diff=clausei.differsSinglyFrom(clausej);
  			if(diff!=null)
  			{
  				IClause newclause=(IClause)clausei.clone();
  				newclause.remove(diff);
  				ret.addClause(newclause);
  				newclausecreated=true;
  			}
  		}
  		if(!newclausecreated) ret.addClause(clausei);
  	}
  	return ret;
  }

  public boolean contains(IClause c)
  {
    if(c==null)
      return false;
    for(int i=0;i<this.numberOfClauses();i++)
      if(this.getClause(i).equals(c))
        return true;
    return false;
  }

  public boolean containsAnEmptyClause()
  {
    for(int i=0;i<this.numberOfClauses();i++)
      if(this.getClause(i).isEmpty())
        return true;
    return false;
  }

  public IProblem eliminateComplementaryPairClauses() throws Exception
  {
    IProblem dup=Problem.newProblem();
    for(int i=0;i<this.numberOfClauses();i++)
    {
    	//Get the ith clause in the IProblem p
      IClause c=this.getClause(i);
      boolean removeClause=false;
      //Iterate through the IClause, looking for complementary IBooleanLiterals
      for(int j=0;j<c.size();j++)
      {
        IBooleanLiteral ib=c.getLiteralAt(j);
        if(!c.contains(ib.complement()))//Detected no complementary IBooleanLiterals
          continue;//Continue searching the IClause
        removeClause=true;//Detected a pair of complementary IBooleanLiterals
        break;
      }
      if(!removeClause)//No complementary IBooleanLiterals were found in the IClause
        dup.addClause(c);//Add the IClause to the IProblem dup
    }
    return dup;
  }

  public boolean equals(Object p)
  {
    if(!(p instanceof List))
      return false;
    if(this.containsAll((List)p) && ((List)p).containsAll(this))
      return true;
    return false;
  }

  public ArrayList getBooleanVariables() throws Exception
  {
    ArrayList hs=new ArrayList();
    for(int i=0;i<this.numberOfClauses();i++)
      if(this.getClause(i)!=null)
      	this.getClause(i).getBooleanVariables((List)hs);
    return hs;
  }

  public IClause getClause(int n)
  {
    return (IClause)(super.get(n));
  }

  public IClause[] getClauses()
  {
    IClause[] clauses=new IClause[super.size()];
    for(int i=0;i<clauses.length;i++)
      clauses[i]=(IClause)(super.get(i));
    return clauses;
  }

  public PrintStream getStream() {
    return stream;
  }

  public boolean isEmpty()
  {
    return (this.numberOfClauses()==0);
  }

  public boolean isSatisfied()
  {
    for(int i=0;i<this.numberOfClauses();i++)
      if(!this.getClause(i).isSatisfied())
        return false;
    return true;
  }

  public IBooleanVariable newBooleanVariable() throws Exception
  {
    return BooleanVariable.getBooleanVariable();
  }

  public int numberOfClauses()
  {
    return super.size();
  }

  public int occurrences(IBooleanLiteral bl) throws Exception
  {
    int count=0;
    for (int i = 0; i < this.numberOfClauses(); i++)
    {
      IClause c=this.getClause(i);
      for(int j=0;j<c.size();j++)
      {
        IBooleanLiteral bq=c.getLiteralAt(j);
        if(bl.equals(bq))
          count++;
      }
    }
    return count;
  }

  public IProblem or(IProblem pfalse, IBooleanVariable b) throws Exception
  {
    return new Disjunction(this,pfalse,b);
  }

  public void removeAllClauses()
  {
    super.clear();
    //super.removeAll(super);
  }

  public void removeClause(int n)
  {
    super.remove(n);
  }

  public IProblem resolve(IBooleanVariable b, boolean value) throws Exception
  {
    IClause[] c=new IClause[this.numberOfClauses()];
    for(int i=0;i<this.numberOfClauses();i++)
      c[i]=this.getClause(i).resolve(b,value);
    IProblem ret=Problem.newProblem();
    ret.setClauses(c);
    return ret;
  }

  public IProblem resolve(List ib) throws Exception
  {
    IProblem res=(IProblem)this.clone();
    for(int i=0;i<res.numberOfClauses();i++)
    {
      IClause c=res.getClause(i);
      for(int j=0;j<ib.size();j++)
      {
        IBooleanLiteral ibcurr=(IBooleanLiteral)ib.get(j);
        IClause newcl=c.resolve(ibcurr.getBooleanVariable(),!ibcurr.isBarred());
        res.setClause(i,newcl);
      }
    }
    return res;
  }

  public void setClause(int n, IClause cl)
  {
    super.set(n,cl);
  }

  public void setClauses(IClause[] cl)
  {
    this.removeAllClauses();
    if(cl!=null)
    	for(int i=0;i<cl.length;i++)
    		this.addClause(cl[i]);
  }

  public void setStream(PrintStream stream) {
    Problem.stream = stream;
  }

  public void sort()
  {
    IClause[] ary=(IClause[])this.toArray(new IClause[0]);
    Arrays.sort(ary);
    this.setClauses(ary);
  }
  
  public IProblem substitute(IBooleanVariable b, boolean value) throws Exception
  {
    ArrayList h=new ArrayList();
    for(int i=0;i<this.numberOfClauses();i++)
    {
      IClause cr=(this.getClause(i)).resolve(b,value);
      if(cr!=null && !(cr.isMemberOf(h)))
        h.add(cr);
    }
    //IProblem res=new Problem(new IClause[h.size()]);
    IProblem res=new Problem();
    Iterator it=h.iterator();
    int i=0;
    while(it.hasNext())
    {
      res.addClause((IClause)(it.next()));
      i++;
    }
    if(res.numberOfClauses()>0)
      return res;
    else
      return null;
  }
  
  public IProblem substitute(Map h) throws Exception
  {
    for(int i=0;i<this.numberOfClauses();i++)
    {
      IClause c=this.getClause(i);
      c.substitute(h);
    }
    return this;
  }

  /*public IProblem reduceComplements(IBooleanVariable b) throws Exception
  {
    IBooleanLiteral blbarred=BooleanLiteral.getBooleanLiteral(b,true);
    IBooleanLiteral blunbarred=BooleanLiteral.getBooleanLiteral(b,false);
    int barred=this.occurrences(blbarred);
    int unbarred=this.occurrences(blunbarred);
    IProblem res=(IProblem)this.clone();
    if(barred<unbarred)
    {
      for(int i=0;i<res.size();i++)
      {
        IClause clause=this.getClause(i);
        if(clause.contains(blbarred))
        {
          clause.remove(blbarred);
          clause.add(blunbarred);
        }
      }
    }
    return res;
  }

  public Problem reduceComplements() throws Exception
  {
    Problem res=(Problem)this.clone();
    IBooleanVariable[] bools=(IBooleanVariable[])res.getBooleanVariables().toArray(new IBooleanVariable[0]);
    for(int i=0;i<bools.length;i++)
      res.reduceComplements(bools[i]);
    return res;
  }*/

  /*
  public ArrayList signature()
  {
    IClause[] sig=this.getClauses();
    ArrayList curr=new ArrayList();
    for(int i=0;i<sig.length;i++)
    {
      IClause cli=sig[i];
      for(int j=0;j<cli.size();j++)
        curr.add(new Integer(cli.size()));
    }
    Collections.sort(curr);
    return curr;
  }
  */

  public IProblem substitute(Object[] b) throws Exception
  {
    IProblem res=(IProblem)this.clone();
    for(int i=0;i<res.numberOfClauses();i++)
    {
      IClause c=res.getClause(i);
      IClause newc=(IClause)c.clone();
      for(int j=0;j<b.length;j++)
      {
        if(newc==null)break;
        newc=newc.resolve((IBooleanLiteral)b[j]);
        //System.out.println("BL="+b[j]+" i="+i+" newc="+newc);
      }
      res.setClause(i,newc);
    }
    return res;
  }
  
  public long toFile(String s)
  {
    File f=new File(s);
    PrintStream fos=null;
    try
    {
      f.createNewFile();
      fos=new PrintStream(new FileOutputStream(f));
      fos.println(this.toString());
      fos.close();
    }
    catch(Exception err)
    {
      err.printStackTrace();
    }

    return f.length();
  }
  
  /*public static IProblem combineSinglyMatchingClauses(IProblem prob)
  {
    if(prob!=null)
    {
    	int psize=prob.size();
    	IProblem ret=prob.newProblem();
    	for(int i=0;i<psize;i++)
    	{
    		IClause clausei=prob.getClause(i);
    		boolean newclausecreated=false;
    		for(int j=0;j<psize;j++)
    		{
    			IClause clausej=prob.getClause(j);
    			IBooleanLiteral diff=clausei.differsSinglyFrom(clausej);
    			if(diff!=null)
    			{
    				IClause newclause=(IClause)clausei.clone();
    				newclause.remove(diff);
          	ret.addClause(newclause);
          	newclausecreated=true;
    			}
    		}
    		if(!newclausecreated) ret.addClause(clausei);
    	}
    	return ret;
    }
    return null;
  }*/
  
  public String toString()
  {
    String res="***************************************";
    //res+="\n*** IProblem@"+hashCode();
    res+="\n*** IProblem-"+ problemCount++ ;
    res+="\n***************************************";
    for(int i=0;i<this.numberOfClauses();i++)
    {
      if(this.getClause(i)!=null)
        res+="\n*** "+"\t"+this.getClause(i).toString();
      else
        res+="\n*** "+"\t"+"null";
    }
    res+="\n***************************************";
    return res;
  }
  
  public IProblem toThreeSatProblem() throws Exception
  {
  	if(this.size()==0)
  		return this;
  	IProblem problem=null;
  	if(this.getClause(0)!=null)
  		problem=((Clause)this.getClause(0)).ThreeSATProblem();
  	for(int i=1;i<this.size();i++)
  		if(this.getClause(i)!=null)
  			problem=new Conjunction(problem,((Clause)this.getClause(i)).ThreeSATProblem());
  	return problem;
  }
  
  /*
  <?xml version="1.0" encoding="UTF-8" ?>
  <!ELEMENT Literal EMPTY >
  <!ATTLIST Literal variable NMTOKEN #REQUIRED >
  <!ATTLIST Literal barred ( false | true ) #REQUIRED >
  <!ELEMENT Problem ( Clause+ ) >
  <!ELEMENT Clause ( Literal+ ) >
  */
  public String toXML()
  {
    String res="<Problem>\n";
    for(int i=0;i<this.numberOfClauses();i++)
    {
      res+="\t<Clause>\n";
      Object[] obary=(this.getClause(i)).toArray();
      for(int j=0;j<obary.length;j++)
      {
        IBooleanLiteral b=(IBooleanLiteral)(obary[j]);
        res+="\t\t<Literal variable=\""+b.getBooleanVariable().getName()+"\" barred=\"";
        if(b.isBarred())
          res+="true\"/>\n";
        else
          res+="false\"/>\n";
      }
      res+="\t</Clause>\n";
    }
    res+="</Problem>";
    return res;
  }
  
  public long toXML(String filename)
  {
    File f=new File(filename);
    PrintStream fos=null;
    try
    {
      f.createNewFile();
      fos=new PrintStream(new FileOutputStream(f));
      fos.println(this.toXML());
      fos.close();
    }
    catch(Exception err)
    {
      err.printStackTrace();
    }

    return f.length();
  }
}