clause.java

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

/*
 * Clause.java	1.01 05/04/22
 *
 * Copyright 2004-2005 Positronic Software.
 *
 *
 */

package positronic.satisfiability.elements;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Iterator;
import java.util.List;
import java.util.Map;

import positronic.satisfiability.exceptions.ClauseException;

/**
 * A class which represents a satisfiability clause. IClause is essentially an
 * ArrayList of IBooleanLiteral objects, and additionally provides several useful
 * methods for manipulating and evaluating the truth value of a clause.
 *
 * @author  Kerry Michael Soileau
 * <blockquote><pre>
 * [e-mail]
 * http://web.wt.net/~ksoileau/index.htm
 * </pre></blockquote>
 * @version 1.01, 05/04/22
 * @see IClause
 * @see ArrayList
 * @see Comparable
 * @see IBooleanLiteral
 * @see IBooleanVariable
 * @see Iterator
 */
public class Clause extends ArrayList implements IClause
{
  private static final long serialVersionUID = 1L;

  public static Clause newClause()
  {
    return new Clause();
  }
  
  public static IClause randomClause(IBooleanVariable[] bv) throws Exception
  {
    IClause ret=Clause.newClause();
    int number=bv.length;
    for(int i=0;i<number;i++)
    {
      double r=Math.random();
      int choice=(int)(3*r);
      if(choice==0) ;
      if(choice==1) ret.add(BooleanLiteral.getBooleanLiteral(bv[i],false));
      if(choice==2) ret.add(BooleanLiteral.getBooleanLiteral(bv[i],true));
    }
    return ret;
  }
  
  public boolean add(IBooleanLiteral b) throws Exception
  {
  	if(b==null)
  		throw new ClauseException("A null IBooleanLiteral was passed to the add method.");
    if(!this.contains(b))
    {
      super.add(b);
      return true;
    }
    else
      return false;
  }

  public void addLiteral(IBooleanLiteral bl) throws Exception
  {
  	if(bl==null)
  		throw new ClauseException("Null IBooleanLiteral was passed to addLiteral method.");
    this.add(bl);
  }

  public Object clone()
  {
  	try
		{
			return this.duplicate();
		} 
  	catch (Exception e)
		{
			System.out.println("Attempt failed to use method clone.");
			e.printStackTrace();
			return null;
		}
  }

  //sorts on size first.
  //if clauses have same size, compare "lowest" BooleanLiteral of each clause
  public int compareTo(IClause o) throws Exception
  {
  	if(o==null)
  		throw new ClauseException("A null Object was passed to the compareTo method.");
    
    int d=super.size()-((ArrayList)o).size();
    if(d!=0)
      return d;
    else
    {
      Object[] thisIt=this.toArray();
      Arrays.sort(thisIt);
      IBooleanLiteral thisFirst=(IBooleanLiteral)(thisIt[0]);
      Object[] oIt=((IClause)o).toArray();
      Arrays.sort(oIt);
      IBooleanLiteral oFirst=(IBooleanLiteral)(oIt[0]);
      return thisFirst.compareTo(oFirst);
    }
  }

  public int compareTo(Object o)
  {
  	try
		{
			return compareTo((IClause)o);
		} 
  	catch (Exception e)
		{
			System.out.println("The compareTo method failed on Object "+o+".");
			e.printStackTrace();
			return Integer.MAX_VALUE;
		}
  }

  public boolean contains(IBooleanLiteral bl) throws Exception
  {
  	if(bl==null)
  		throw new ClauseException("A null IBooleanLiteral was passed to the contains method.");
    Iterator it=this.iterator();
    while(it.hasNext())
    {
      Object obj=it.next();
      IBooleanLiteral blc=(IBooleanLiteral)obj;
      if(blc.equals(bl))
        return true;
    }
    return false;
  }

  public IBooleanLiteral differsSinglyFrom(IClause c) throws Exception
  {
    if(c==null) return null;
    if(this.size()!=c.size()) return null;
    IClause dminusc=this.minus(c);
    if(dminusc.size()!=1) return null;
    IClause cminusd=c.minus(this);
    if(cminusd.size()!=1) return null;
    IBooleanLiteral dminuscbl=dminusc.getLiteralAt(0);
    IBooleanVariable dminuscbv=dminuscbl.getBooleanVariable();
    IBooleanVariable cminusdbv=cminusd.getLiteralAt(0).getBooleanVariable();
    if(!dminuscbv.equals(cminusdbv)) return null;
    return dminuscbl;
  }
  
  /**
   * An IClause A dominates B if every IBooleanLiteral in A can be found in B. In that 
   * case, 
   * A & B <--> A.
   * Practically speaking, if A dominates B, then B is redundant and may be deleted from
   * any IProblem which includes the IClause A.
   * @throws Exception 
   */
  public boolean dominates(IClause clause) throws Exception
  {
    if(clause==null) return true;
    if(this.isEmpty()) return true; //An empty IClause dominates every other IClause
    //if(this.size()>clause.size()) return false;
    for(int i=0;i<this.size();i++)
      if(!clause.contains(this.getLiteralAt(i))) return false;
    return true;
  }

  public Object duplicate() throws Exception
  {
    IClause cl=new Clause();
    for(int i=0;i<this.size();i++)
      cl.add(this.getLiteralAt(i));
    return cl;
  }

  public boolean equals(IClause o) throws Exception
  {
  	if(o==null)
  		throw new ClauseException("Null IClause was passed to method equals.");
  	if (o == this)
      return true;
  	//if (!(o instanceof IClause))
    //  return false;
  	
    

    //if(this.size()!=((ArrayList)o).size())
    //  return false;

    /*for(int i=0;i<this.size();i++)
    {
      if(!this.contains(((IClause)o).getLiteralAt(i)))
        return false;
    }*/
    
    IClause ic=(IClause)o;
    if(!((IClause)this).dominates(ic))
    	return false;
    if(!ic.dominates((IClause)this))
    	return false;
    return true;
  }
  
  public boolean evaluate()
  {
    Iterator it=this.iterator();

    while(it.hasNext())
      if(((IBooleanLiteral)(it.next())).evaluate())
        return true;

    return false;
  }
  
  
  public Object[] getBooleanVariables()
  {
    ArrayList res=new ArrayList();
    Object[] bl=this.toArray();
    for(int i=0;i<bl.length;i++)
      res.add(((IBooleanLiteral)bl[i]).getBooleanVariable());

    return res.toArray();
  }


  public void getBooleanVariables(List hs) throws Exception
  {
  	if(hs==null)
  		throw new ClauseException("A null List was passed to the getBooleanVariables method.");
    
    Object[] bl=this.toArray();
    for(int i=0;i<bl.length;i++)
      hs.add(((IBooleanLiteral)bl[i]).getBooleanVariable());
  }

  public IBooleanLiteral getLiteralAt(int n) throws Exception
  {
  	if(n<0)
  		throw new ClauseException("A negative number was passed to getLiteralAt method.");
    return (IBooleanLiteral)(super.get(n));
  }

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

  public boolean isMemberOf(List h) throws Exception
  {
  	if(h==null)
  		throw new ClauseException("A null List was passed to isMemberOf method.");
    Iterator it=h.iterator();
    while(it.hasNext())
    {
      Object obj=it.next();
      IClause curr=(IClause)obj;
      if(curr.equals(this))
        return true;
    }
    return false;
  }

  public boolean isSatisfied()
  {
    return this.evaluate();
  }

  public boolean isSensitiveTo(IBooleanVariable bv) throws ClauseException
  {
  	if(bv==null)
  		throw new ClauseException("A null IBooleanVariable was passed to isSensitiveTo method.");
  	
    Iterator it=this.iterator();

    while(it.hasNext())
    {
      IBooleanLiteral bl=(IBooleanLiteral)(it.next());
      if(bv.equals(bl.getBooleanVariable()))
      {
        boolean startValue=this.evaluate();
        bv.setValue(!bv.getValue());
        boolean endValue=this.evaluate();
        bv.setValue(!bv.getValue());
        if(startValue!=endValue)
          return true;
      }
    }
    return false;
  }

  public boolean isSingleton()
  {
    return(this.size()==1);
  }

  public Iterator iterator()
  {
    return super.iterator();
  }

  public IClause minus(IClause o) throws Exception
  {
    //if (o == this)
    //  return new Clause();
    //if (!(o instanceof IClause))
    //  return this;
  	if(o==null)
  		throw new ClauseException("Null IClause was passed to minus method.");
    
    IClause ret=(IClause)this.clone();
    for(int i=0;i<o.size();i++)
      ret.remove(o.getLiteralAt(i));
    return ret;
  }

  public IClause or(IBooleanVariable bv) throws Exception
  {
  	if(bv==null)
  		throw new ClauseException("A null IBooleanVariable was passed to the or method.");
    
    this.addLiteral(BooleanLiteral.getBooleanLiteral(bv,false));
    return this;
  }

  public IClause orNot(IBooleanVariable bv) throws Exception
  {
  	if(bv==null)
  		throw new ClauseException("A null IBooleanVariable was passed to the orNot method.");
    
    this.addLiteral(BooleanLiteral.getBooleanLiteral(bv,true));
    return this;
  }

  public boolean remove(IBooleanLiteral b)
  {
  	return super.remove(b);
  }

  public Object remove(int i)
  {
  	return super.remove(i);
  }

  public IClause resolve(IBooleanLiteral ib) throws Exception
  {
  	if(ib==null)
  		throw new ClauseException("Null IBooleanLiteral was passed to resolve method.");
    
    return this.resolve(ib.getBooleanVariable(),!ib.isBarred());
  }

  // An empty IClause ={} cannot be satisfied.
  // A null IClause =null is satisfied trivially.
  public IClause resolve(IBooleanVariable b, boolean value) throws Exception
  {
  	if(b==null)
  		throw new ClauseException("Null IBooleanVariable was passed to resolve method.");
    IClause c=(IClause)(this.clone());
    Iterator it=this.iterator();
    while(it.hasNext())
    {
      Object obj=it.next();
      IBooleanLiteral bl=(IBooleanLiteral)obj;
      if(bl.getBooleanVariable().equals(b))
        if(bl.isBarred()==value)
          c.remove(bl);
        else
        {
          c=null;
          break;
        }
    }
    return c;
    /*
    if(!(c.isEmpty()))
      return c;
    else
      return null;
    */
  }
  
  public int size()
  {
  	return super.size();
  }
  
  public IClause substitute(Map h) throws Exception
  {
  	if(h==null)
  		throw new ClauseException("Null java.util.Map was passed to substitute method.");
    
    boolean didsomething=true;
    while(didsomething)
    {
      didsomething=false;
      for(int i=0;i<this.size();i++)
      {
        IBooleanLiteral ib=this.getLiteralAt(i);
        Object tr=h.get(ib);
        if(tr!=null && tr instanceof IBooleanLiteral && !((IBooleanLiteral)tr).equals(ib))
        {
          //System.out.println("Substituting "+(IBooleanLiteral)tr+" for "+this.get(i));
          this.remove(i);
          this.add((IBooleanLiteral)tr);
          didsomething=true;
        }
      }
    }
    return this;
  }
  
  public IClause substitute(Map h, IClause c) throws Exception
  {
  	if(h==null)
  		throw new ClauseException("Null java.util.Map was passed to substitute method.");
    
    boolean didsomething=true;
    while(didsomething)
    {
      didsomething=false;
      for(int i=0;i<c.size();i++)
      {
        IBooleanLiteral ib=c.getLiteralAt(i);
        Object tr=h.get(ib);
        if(tr!=null && tr instanceof IBooleanLiteral && !((IBooleanLiteral)tr).equals(ib))
        {
          //System.out.println("Substituting "+(IBooleanLiteral)tr+" for "+this.get(i));
          c.remove(i);
          c.add((IBooleanLiteral)tr);
          didsomething=true;
        }
      }
    }
    return this;
  }
  
  /*public static boolean dominates(IClause c, IClause d)
  {
    if(d.size()>=c.size()) return false;
    for(int i=0;i<d.size();i++)
    {
      IBooleanLiteral curr=d.getLiteralAt(i);
      if(!c.contains(curr)) return false;
    }
    return true;
  }*/
  
  /*public static IBooleanLiteral differsSinglyFrom(IClause c, IClause d)
  {
    if(c==null) return null;
    if(d.size()!=c.size()) return null;
    IClause dminusc=d.minus(c);
    if(dminusc.size()!=1) return null;
    IClause cminusd=c.minus(d);
    if(cminusd.size()!=1) return null;
    IBooleanLiteral dminuscbl=dminusc.getLiteralAt(0);
    IBooleanVariable dminuscbv=dminuscbl.getBooleanVariable();
    IBooleanVariable cminusdbv=cminusd.getLiteralAt(0).getBooleanVariable();
    if(!dminuscbv.equals(cminusdbv)) return null;
    return dminuscbl;
  }*/
  
  public IProblem ThreeSATProblem() throws Exception
  {
  	if(this.size()<4)
  		return (IProblem)(new Problem(new IClause[]{this}));
  	
  	Clause left=new Clause();
  	left.add(this.getLiteralAt(0));
  	left.add(this.getLiteralAt(1));
  	Clause right=new Clause();
  	for(int i=2;i<this.size();i++)
  	{
  		right.add(this.getLiteralAt(i));
  	}
  	IBooleanVariable bv=BooleanVariable.getBooleanVariable();
  	IBooleanLiteral blunbarred=BooleanLiteral.getBooleanLiteral(bv,false);
  	IBooleanLiteral blbarred=BooleanLiteral.getBooleanLiteral(bv,true);
  	left.add(blunbarred);
  	right.add(blbarred);
  	IProblem problem=new Conjunction(left.ThreeSATProblem(),right.ThreeSATProblem());
  	return problem;
  }

  //Implementation-specific methods

  public Object[] toArray()
  {
    return super.toArray();
  }

  public Object[] toSortedArray()
  {
    Object[] obj=this.toArray();
    Arrays.sort(obj);
    return obj;
  }

  public String toString()
  {
    String res="{";
    Object[] obj=this.toSortedArray();
    for(int j=0;j<obj.length;j++)
        res+=obj[j];
    return res+"}";
  }

  //End Implementation-specific methods
}