org.sat4j.pb_2.3.0.v20110329

16:49:47.932 INFO  jd.cli.Main - Decompiling org.sat4j.pb_2.3.0.v20110329.jar
package org.sat4j.pb;

import java.math.BigInteger;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;

public abstract interface IPBSolver
  extends ISolver
{
  public abstract IConstr addPseudoBoolean(IVecInt paramIVecInt, IVec<BigInteger> paramIVec, boolean paramBoolean, BigInteger paramBigInteger)
    throws ContradictionException;
  
  public abstract void setObjectiveFunction(ObjectiveFunction paramObjectiveFunction);
  
  public abstract ObjectiveFunction getObjectiveFunction();
}

/* Location:
 * Qualified Name:     org.sat4j.pb.IPBSolver
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j.pb;

import java.io.PrintWriter;
import org.sat4j.AbstractLauncher;
import org.sat4j.AbstractOptimizationLauncher;
import org.sat4j.ExitCode;
import org.sat4j.core.ASolverFactory;
import org.sat4j.pb.reader.OPBReader2006;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ISolver;

public class LanceurPseudo2005
  extends AbstractOptimizationLauncher
{
  ASolverFactory<IPBSolver> factory;
  private static final long serialVersionUID = 1L;
  protected ObjectiveFunction obfct;
  
  public LanceurPseudo2005()
  {
    this(SolverFactory.instance());
  }
  
  LanceurPseudo2005(ASolverFactory<IPBSolver> paramASolverFactory)
  {
    factory = paramASolverFactory;
  }
  
  public static void main(String[] paramArrayOfString)
  {
    LanceurPseudo2005 localLanceurPseudo2005 = new LanceurPseudo2005();
    localLanceurPseudo2005.run(paramArrayOfString);
    System.exit(localLanceurPseudo2005.getExitCode().value());
  }
  
  protected Reader createReader(ISolver paramISolver, String paramString)
  {
    return new OPBReader2006((IPBSolver)paramISolver);
  }
  
  protected ISolver configureSolver(String[] paramArrayOfString)
  {
    if (paramArrayOfString.length > 1) {
      localObject = (IPBSolver)factory.createSolverByName(paramArrayOfString[0]);
    } else {
      localObject = (IPBSolver)factory.defaultSolver();
    }
    Object localObject = new PseudoOptDecorator((IPBSolver)localObject);
    if (paramArrayOfString.length == 3) {
      ((IPBSolver)localObject).setTimeout(Integer.valueOf(paramArrayOfString[1]).intValue());
    }
    out.println(((ISolver)localObject).toString("c "));
    return (ISolver)localObject;
  }
  
  public void usage()
  {
    out.println("java -jar sat4j-pb.jar [solvername [timeout]] instancename.opb");
    showAvailableSolvers(SolverFactory.instance());
  }
  
  protected String getInstanceName(String[] paramArrayOfString)
  {
    assert ((paramArrayOfString.length == 1) || (paramArrayOfString.length == 2) || (paramArrayOfString.length == 3));
    if (paramArrayOfString.length == 0) {
      return null;
    }
    return paramArrayOfString[(paramArrayOfString.length - 1)];
  }
}

/* Location:
 * Qualified Name:     org.sat4j.pb.LanceurPseudo2005
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j.pb;

import org.sat4j.AbstractLauncher;
import org.sat4j.ExitCode;
import org.sat4j.core.ASolverFactory;
import org.sat4j.pb.reader.OPBReader2010;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ISolver;

public class LanceurPseudo2007
  extends LanceurPseudo2005
{
  private static final long serialVersionUID = 1L;
  
  public LanceurPseudo2007() {}
  
  public LanceurPseudo2007(ASolverFactory<IPBSolver> paramASolverFactory)
  {
    super(paramASolverFactory);
  }
  
  protected Reader createReader(ISolver paramISolver, String paramString)
  {
    return new OPBReader2010((IPBSolver)paramISolver);
  }
  
  public static void main(String[] paramArrayOfString)
  {
    LanceurPseudo2007 localLanceurPseudo2007 = new LanceurPseudo2007();
    if ((paramArrayOfString.length == 0) || (paramArrayOfString.length > 3))
    {
      localLanceurPseudo2007.usage();
      return;
    }
    localLanceurPseudo2007.run(paramArrayOfString);
    System.exit(localLanceurPseudo2007.getExitCode().value());
  }
}

/* Location:
 * Qualified Name:     org.sat4j.pb.LanceurPseudo2007
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j.pb;

import java.io.PrintWriter;
import java.util.Collection;
import org.sat4j.AbstractLauncher;
import org.sat4j.ExitCode;
import org.sat4j.pb.reader.OPBEclipseReader2007;
import org.sat4j.pb.tools.XplainPB;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.TimeoutException;

public class LanceurPseudo2007Eclipse
  extends LanceurPseudo2007
{
  XplainPB quickxplain;
  private static final long serialVersionUID = 1L;
  
  protected ISolver configureSolver(String[] paramArrayOfString)
  {
    if (paramArrayOfString.length > 1) {
      localObject = (IPBSolver)SolverFactory.instance().createSolverByName(paramArrayOfString[0]);
    } else {
      localObject = SolverFactory.newDefault();
    }
    quickxplain = new XplainPB((IPBSolver)localObject);
    Object localObject = new PseudoOptDecorator(quickxplain);
    if (paramArrayOfString.length == 3) {
      ((IPBSolver)localObject).setTimeout(Integer.valueOf(paramArrayOfString[1]).intValue());
    }
    out.println(((ISolver)localObject).toString("c "));
    return (ISolver)localObject;
  }
  
  protected Reader createReader(ISolver paramISolver, String paramString)
  {
    return new OPBEclipseReader2007((IPBSolver)paramISolver);
  }
  
  public static void main(String[] paramArrayOfString)
  {
    LanceurPseudo2007Eclipse localLanceurPseudo2007Eclipse = new LanceurPseudo2007Eclipse();
    if ((paramArrayOfString.length == 0) || (paramArrayOfString.length > 2))
    {
      localLanceurPseudo2007Eclipse.usage();
      return;
    }
    localLanceurPseudo2007Eclipse.run(paramArrayOfString);
    System.exit(localLanceurPseudo2007Eclipse.getExitCode().value());
  }
  
  protected void displayAnswer()
  {
    super.displayAnswer();
    ExitCode localExitCode = getExitCode();
    if (localExitCode == ExitCode.UNSATISFIABLE) {
      try
      {
        Collection localCollection = quickxplain.explain();
        log("Explanation for inconsistency: " + localCollection);
      }
      catch (TimeoutException localTimeoutException)
      {
        log("Timeout ! Need more time to complete");
      }
    }
  }
}

/* Location:
 * Qualified Name:     org.sat4j.pb.LanceurPseudo2007Eclipse
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j.pb;

import org.sat4j.specs.IConstr;

final class OPBStringSolver$1
  implements IConstr
{
  public int size()
  {
    throw new UnsupportedOperationException("Fake IConstr");
  }
  
  public boolean learnt()
  {
    throw new UnsupportedOperationException("Fake IConstr");
  }
  
  public double getActivity()
  {
    throw new UnsupportedOperationException("Fake IConstr");
  }
  
  public int get(int paramInt)
  {
    throw new UnsupportedOperationException("Fake IConstr");
  }
}

/* Location:
 * Qualified Name:     org.sat4j.pb.OPBStringSolver.1
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j.pb;

import java.math.BigInteger;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.IteratorInt;
import org.sat4j.specs.TimeoutException;
import org.sat4j.tools.DimacsStringSolver;

public class OPBStringSolver
  extends DimacsStringSolver
  implements IPBSolver
{
  private static final String FAKE_I_CONSTR_MSG = "Fake IConstr";
  private static final long serialVersionUID = 1L;
  private int indxConstrObj;
  private int nbOfConstraints;
  private ObjectiveFunction obj;
  private boolean inserted = false;
  private static final IConstr FAKE_CONSTR = new IConstr()
  {
    public int size()
    {
      throw new UnsupportedOperationException("Fake IConstr");
    }
    
    public boolean learnt()
    {
      throw new UnsupportedOperationException("Fake IConstr");
    }
    
    public double getActivity()
    {
      throw new UnsupportedOperationException("Fake IConstr");
    }
    
    public int get(int paramAnonymousInt)
    {
      throw new UnsupportedOperationException("Fake IConstr");
    }
  };
  
  public OPBStringSolver() {}
  
  public OPBStringSolver(int paramInt)
  {
    super(paramInt);
  }
  
  public boolean isSatisfiable(IVecInt paramIVecInt)
    throws TimeoutException
  {
    IteratorInt localIteratorInt = paramIVecInt.iterator();
    while (localIteratorInt.hasNext())
    {
      int i = localIteratorInt.next();
      if (i > 0) {
        getOut().append("+1 x" + i + " >= 1 ;\n");
      } else {
        getOut().append("-1 x" + -i + " >= 0 ;\n");
      }
      nbOfConstraints += 1;
    }
    throw new TimeoutException();
  }
  
  public boolean isSatisfiable(IVecInt paramIVecInt, boolean paramBoolean)
    throws TimeoutException
  {
    return super.isSatisfiable(paramIVecInt, paramBoolean);
  }
  
  public IConstr addPseudoBoolean(IVecInt paramIVecInt, IVec<BigInteger> paramIVec, boolean paramBoolean, BigInteger paramBigInteger)
    throws ContradictionException
  {
    StringBuffer localStringBuffer = getOut();
    assert (paramIVecInt.size() == paramIVec.size());
    nbOfConstraints += 1;
    int i;
    if (paramBoolean)
    {
      for (i = 0; i < paramIVecInt.size(); i++)
      {
        localStringBuffer.append(paramIVec.get(i));
        localStringBuffer.append(" x");
        localStringBuffer.append(paramIVecInt.get(i));
        localStringBuffer.append(" ");
      }
      localStringBuffer.append(">= ");
      localStringBuffer.append(paramBigInteger);
      localStringBuffer.append(" ;\n");
    }
    else
    {
      for (i = 0; i < paramIVecInt.size(); i++)
      {
        localStringBuffer.append(((BigInteger)paramIVec.get(i)).negate());
        localStringBuffer.append(" x");
        localStringBuffer.append(paramIVecInt.get(i));
        localStringBuffer.append(" ");
      }
      localStringBuffer.append(">= ");
      localStringBuffer.append(paramBigInteger.negate());
      localStringBuffer.append(" ;\n");
    }
    return FAKE_CONSTR;
  }
  
  public void setObjectiveFunction(ObjectiveFunction paramObjectiveFunction)
  {
    obj = paramObjectiveFunction;
  }
  
  public IConstr addAtLeast(IVecInt paramIVecInt, int paramInt)
    throws ContradictionException
  {
    StringBuffer localStringBuffer = getOut();
    nbOfConstraints += 1;
    IteratorInt localIteratorInt = paramIVecInt.iterator();
    while (localIteratorInt.hasNext()) {
      localStringBuffer.append("+1 x" + localIteratorInt.next() + " ");
    }
    localStringBuffer.append(">= " + paramInt + " ;\n");
    return FAKE_CONSTR;
  }
  
  public IConstr addAtMost(IVecInt paramIVecInt, int paramInt)
    throws ContradictionException
  {
    StringBuffer localStringBuffer = getOut();
    nbOfConstraints += 1;
    IteratorInt localIteratorInt = paramIVecInt.iterator();
    while (localIteratorInt.hasNext()) {
      localStringBuffer.append("-1 x" + localIteratorInt.next() + " ");
    }
    localStringBuffer.append(">= " + -paramInt + " ;\n");
    return FAKE_CONSTR;
  }
  
  public IConstr addClause(IVecInt paramIVecInt)
    throws ContradictionException
  {
    StringBuffer localStringBuffer = getOut();
    nbOfConstraints += 1;
    IteratorInt localIteratorInt = paramIVecInt.iterator();
    while (localIteratorInt.hasNext())
    {
      int i = localIteratorInt.next();
      if (i > 0) {
        localStringBuffer.append("+1 x" + i + " ");
      } else {
        localStringBuffer.append("+1 ~x" + -i + " ");
      }
    }
    localStringBuffer.append(">= 1 ;\n");
    return FAKE_CONSTR;
  }
  
  public String getExplanation()
  {
    return null;
  }
  
  public void setListOfVariablesForExplanation(IVecInt paramIVecInt) {}
  
  public String toString()
  {
    StringBuffer localStringBuffer1 = getOut();
    if (!inserted)
    {
      StringBuffer localStringBuffer2 = new StringBuffer();
      localStringBuffer2.append("* #variable= ");
      localStringBuffer2.append(nVars());
      localStringBuffer2.append(" #constraint= ");
      localStringBuffer2.append(nbOfConstraints);
      localStringBuffer2.append(" \n");
      if (obj != null)
      {
        localStringBuffer2.append("min: ");
        localStringBuffer2.append(obj);
        localStringBuffer2.append(" ;\n");
      }
      localStringBuffer1.insert(indxConstrObj, localStringBuffer2.toString());
      inserted = true;
    }
    return localStringBuffer1.toString();
  }
  
  public String toString(String paramString)
  {
    return "OPB output solver";
  }
  
  public int newVar(int paramInt)
  {
    StringBuffer localStringBuffer = getOut();
    setNbVars(paramInt);
    indxConstrObj = localStringBuffer.length();
    localStringBuffer.append("\n");
    return paramInt;
  }
  
  public void setExpectedNumberOfClauses(int paramInt) {}
  
  public ObjectiveFunction getObjectiveFunction()
  {
    return obj;
  }
  
  public int nConstraints()
  {
    return nbOfConstraints;
  }
}

/* Location:
 * Qualified Name:     org.sat4j.pb.OPBStringSolver
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j.pb;

import java.io.Serializable;
import java.math.BigInteger;
import org.sat4j.core.ReadOnlyVec;
import org.sat4j.core.ReadOnlyVecInt;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;

public class ObjectiveFunction
  implements Serializable
{
  private static final long serialVersionUID = 1L;
  private final IVec<BigInteger> coeffs;
  private final IVecInt vars;
  
  public ObjectiveFunction(IVecInt paramIVecInt, IVec<BigInteger> paramIVec)
  {
    vars = new ReadOnlyVecInt(paramIVecInt);
    coeffs = new ReadOnlyVec(paramIVec);
  }
  
  public BigInteger calculateDegree(int[] paramArrayOfInt)
  {
    BigInteger localBigInteger1 = BigInteger.ZERO;
    for (int i = 0; i < vars.size(); i++)
    {
      BigInteger localBigInteger2 = (BigInteger)coeffs.get(i);
      if (varInModel(vars.get(i), paramArrayOfInt)) {
        localBigInteger1 = localBigInteger1.add(localBigInteger2);
      } else if ((localBigInteger2.signum() < 0) && (!varInModel(-vars.get(i), paramArrayOfInt))) {
        localBigInteger1 = localBigInteger1.add(localBigInteger2);
      }
    }
    return localBigInteger1;
  }
  
  private boolean varInModel(int paramInt, int[] paramArrayOfInt)
  {
    for (int i = 0; i < paramArrayOfInt.length; i++) {
      if (paramInt == paramArrayOfInt[i]) {
        return true;
      }
    }
    return false;
  }
  
  public IVec<BigInteger> getCoeffs()
  {
    return coeffs;
  }
  
  public IVecInt getVars()
  {
    return vars;
  }
  
  public String toString()
  {
    StringBuffer localStringBuffer = new StringBuffer();
    IVecInt localIVecInt = getVars();
    IVec localIVec = getCoeffs();
    for (int j = 0; j < localIVecInt.size(); j++)
    {
      BigInteger localBigInteger = (BigInteger)localIVec.get(j);
      int i = localIVecInt.get(j);
      if (i < 0)
      {
        i = -i;
        localBigInteger = localBigInteger.negate();
      }
      localStringBuffer.append((localBigInteger.signum() < 0 ? "" : "+") + localBigInteger + " x" + i + " ");
    }
    return localStringBuffer.toString();
  }
}

/* Location:
 * Qualified Name:     org.sat4j.pb.ObjectiveFunction
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j.pb;

import java.io.PrintStream;
import org.sat4j.core.VecInt;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IOptimizationProblem;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.TimeoutException;

public class OptToPBSATAdapter
  extends PBSolverDecorator
{
  private static final long serialVersionUID = 1L;
  IOptimizationProblem problem;
  boolean modelComputed = false;
  private final IVecInt assumps = new VecInt();
  private long begin;
  
  public OptToPBSATAdapter(IOptimizationProblem paramIOptimizationProblem)
  {
    super((IPBSolver)paramIOptimizationProblem);
    problem = paramIOptimizationProblem;
  }
  
  public boolean isSatisfiable()
    throws TimeoutException
  {
    modelComputed = false;
    assumps.clear();
    begin = System.currentTimeMillis();
    if (problem.hasNoObjectiveFunction()) {
      return modelComputed = problem.isSatisfiable();
    }
    return problem.admitABetterSolution();
  }
  
  public boolean isSatisfiable(boolean paramBoolean)
    throws TimeoutException
  {
    return isSatisfiable();
  }
  
  public boolean isSatisfiable(IVecInt paramIVecInt, boolean paramBoolean)
    throws TimeoutException
  {
    return isSatisfiable(paramIVecInt);
  }
  
  public boolean isSatisfiable(IVecInt paramIVecInt)
    throws TimeoutException
  {
    modelComputed = false;
    assumps.clear();
    paramIVecInt.copyTo(assumps);
    begin = System.currentTimeMillis();
    if (problem.hasNoObjectiveFunction()) {
      return modelComputed = problem.isSatisfiable(paramIVecInt);
    }
    return problem.admitABetterSolution(paramIVecInt);
  }
  
  public int[] model()
  {
    if (modelComputed) {
      return problem.model();
    }
    try
    {
      assert (problem.admitABetterSolution(assumps));
      assert (!problem.hasNoObjectiveFunction());
      do
      {
        problem.discardCurrentSolution();
        if (isVerbose()) {
          System.out.println(getLogPrefix() + "Current objective function value: " + problem.getObjectiveValue() + "(" + (System.currentTimeMillis() - begin) / 1000.0D + "s)");
        }
      } while (problem.admitABetterSolution(assumps));
    }
    catch (TimeoutException localTimeoutException)
    {
      if (isVerbose()) {
        System.out.println(getLogPrefix() + "Solver timed out after " + (System.currentTimeMillis() - begin) / 1000.0D + "s)");
      }
    }
    catch (ContradictionException localContradictionException) {}
    modelComputed = true;
    return problem.model();
  }
  
  public boolean model(int paramInt)
  {
    if (!modelComputed) {
      model();
    }
    return problem.model(paramInt);
  }
  
  public String toString(String paramString)
  {
    return paramString + "Optimization to Pseudo Boolean adapter\n" + super.toString(paramString);
  }
  
  public boolean isOptimal()
  {
    return problem.isOptimal();
  }
}

/* Location:
 * Qualified Name:     org.sat4j.pb.OptToPBSATAdapter
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j.pb;

import java.math.BigInteger;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.sat4j.tools.SolverDecorator;

public class PBSolverDecorator
  extends SolverDecorator<IPBSolver>
  implements IPBSolver
{
  private static final long serialVersionUID = 1L;
  
  public PBSolverDecorator(IPBSolver paramIPBSolver)
  {
    super(paramIPBSolver);
  }
  
  public IConstr addPseudoBoolean(IVecInt paramIVecInt, IVec<BigInteger> paramIVec, boolean paramBoolean, BigInteger paramBigInteger)
    throws ContradictionException
  {
    return ((IPBSolver)decorated()).addPseudoBoolean(paramIVecInt, paramIVec, paramBoolean, paramBigInteger);
  }
  
  public void setObjectiveFunction(ObjectiveFunction paramObjectiveFunction)
  {
    ((IPBSolver)decorated()).setObjectiveFunction(paramObjectiveFunction);
  }
  
  public ObjectiveFunction getObjectiveFunction()
  {
    return ((IPBSolver)decorated()).getObjectiveFunction();
  }
}

/* Location:
 * Qualified Name:     org.sat4j.pb.PBSolverDecorator
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j.pb;

import java.io.FileNotFoundException;
import java.io.IOException;
import java.io.PrintStream;
import java.math.BigInteger;
import org.sat4j.core.VecInt;
import org.sat4j.pb.reader.OPBReader2007;
import org.sat4j.reader.ParseFormatException;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.IProblem;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.TimeoutException;
import org.sat4j.tools.GateTranslator;
import org.sat4j.tools.SolverDecorator;

public class PseudoBitsAdderDecorator
  extends SolverDecorator<IPBSolver>
  implements IPBSolver
{
  private static final long serialVersionUID = 1L;
  private ObjectiveFunction objfct;
  private final GateTranslator gator;
  private final IPBSolver solver;
  private IVecInt bitsLiterals;
  private IVecInt fixedLiterals;
  
  public PseudoBitsAdderDecorator(IPBSolver paramIPBSolver)
  {
    super(paramIPBSolver);
    gator = new GateTranslator(paramIPBSolver);
    solver = paramIPBSolver;
  }
  
  public void setObjectiveFunction(ObjectiveFunction paramObjectiveFunction)
  {
    objfct = paramObjectiveFunction;
  }
  
  public boolean isSatisfiable()
    throws TimeoutException
  {
    return isSatisfiable(VecInt.EMPTY);
  }
  
  public boolean isSatisfiable(IVecInt paramIVecInt)
    throws TimeoutException
  {
    if (objfct == null) {
      return gator.isSatisfiable(paramIVecInt);
    }
    System.out.println("c Original number of variables and constraints");
    System.out.println("c #vars: " + gator.nVars() + " #constraints: " + gator.nConstraints());
    bitsLiterals = new VecInt();
    System.out.println("c Creating optimization constraints ....");
    try
    {
      gator.optimisationFunction(objfct.getVars(), objfct.getCoeffs(), bitsLiterals);
    }
    catch (ContradictionException localContradictionException)
    {
      return false;
    }
    System.out.println("c ... done. " + bitsLiterals);
    System.out.println("c New number of variables and constraints");
    System.out.println("c #vars: " + gator.nVars() + " #constraints: " + gator.nConstraints());
    fixedLiterals = new VecInt(bitsLiterals.size());
    VecInt localVecInt = new VecInt(paramIVecInt.size() + bitsLiterals.size());
    int i = bitsLiterals.size() - 1;
    while (i >= 0)
    {
      paramIVecInt.copyTo(localVecInt);
      fixedLiterals.copyTo(localVecInt);
      localVecInt.push(-bitsLiterals.get(i));
      for (int j = i - 1; j >= 0; j--) {
        localVecInt.push(bitsLiterals.get(j));
      }
      System.out.println("c assumptions " + localVecInt);
      boolean bool = gator.isSatisfiable(localVecInt, true);
      if (bool)
      {
        fixedLiterals.push(-bitsLiterals.get(i--));
        BigInteger localBigInteger = objfct.calculateDegree(gator.model());
        System.out.println("o " + localBigInteger);
        System.out.println("c current objective value with fixed lits " + fixedLiterals);
      }
      else
      {
        fixedLiterals.push(bitsLiterals.get(i--));
        System.out.println("c unsat. fixed lits " + fixedLiterals);
      }
      localVecInt.clear();
    }
    assert (fixedLiterals.size() == bitsLiterals.size());
    paramIVecInt.copyTo(localVecInt);
    fixedLiterals.copyTo(localVecInt);
    return gator.isSatisfiable(localVecInt);
  }
  
  public static void main(String[] paramArrayOfString)
  {
    PseudoBitsAdderDecorator localPseudoBitsAdderDecorator = new PseudoBitsAdderDecorator(SolverFactory.newDefault());
    localPseudoBitsAdderDecorator.setVerbose(false);
    OPBReader2007 localOPBReader2007 = new OPBReader2007(localPseudoBitsAdderDecorator);
    long l1 = System.currentTimeMillis();
    try
    {
      IProblem localIProblem = localOPBReader2007.parseInstance(paramArrayOfString[0]);
      if (localIProblem.isSatisfiable())
      {
        System.out.println("s OPTIMUM FOUND");
        System.out.println("v " + localOPBReader2007.decode(localIProblem.model()));
        if (objfct != null) {
          System.out.println("c objective function=" + objfct.calculateDegree(gator.model()));
        }
      }
      else
      {
        System.out.println("s UNSAT");
      }
    }
    catch (FileNotFoundException localFileNotFoundException)
    {
      localFileNotFoundException.printStackTrace();
    }
    catch (ParseFormatException localParseFormatException)
    {
      localParseFormatException.printStackTrace();
    }
    catch (IOException localIOException)
    {
      localIOException.printStackTrace();
    }
    catch (ContradictionException localContradictionException)
    {
      System.out.println("s UNSAT");
      System.out.println("c trivial inconsistency");
    }
    catch (TimeoutException localTimeoutException)
    {
      System.out.println("s UNKNOWN");
    }
    long l2 = System.currentTimeMillis();
    System.out.println("c Total wall clock time: " + (l2 - l1) / 1000.0D + " seconds");
  }
  
  public IConstr addPseudoBoolean(IVecInt paramIVecInt, IVec<BigInteger> paramIVec, boolean paramBoolean, BigInteger paramBigInteger)
    throws ContradictionException
  {
    return solver.addPseudoBoolean(paramIVecInt, paramIVec, paramBoolean, paramBigInteger);
  }
  
  public ObjectiveFunction getObjectiveFunction()
  {
    return objfct;
  }
}

/* Location:
 * Qualified Name:     org.sat4j.pb.PseudoBitsAdderDecorator
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j.pb;

import org.sat4j.core.VecInt;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVecInt;

public class PseudoIteratorDecorator
  extends PseudoOptDecorator
{
  private static final long serialVersionUID = 1L;
  
  public PseudoIteratorDecorator(IPBSolver paramIPBSolver)
  {
    super(paramIPBSolver);
  }
  
  public void discardCurrentSolution()
    throws ContradictionException
  {
    int[] arrayOfInt1 = super.model();
    VecInt localVecInt = new VecInt(arrayOfInt1.length);
    int[] arrayOfInt2 = arrayOfInt1;
    int i = arrayOfInt2.length;
    for (int j = 0; j < i; j++)
    {
      int k = arrayOfInt2[j];
      localVecInt.push(-k);
    }
    addClause(localVecInt);
  }
}

/* Location:
 * Qualified Name:     org.sat4j.pb.PseudoIteratorDecorator
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j.pb;

import java.math.BigInteger;
import org.sat4j.core.VecInt;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.IOptimizationProblem;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.TimeoutException;

public class PseudoOptDecorator
  extends PBSolverDecorator
  implements IOptimizationProblem
{
  private static final long serialVersionUID = 1L;
  private ObjectiveFunction objfct;
  private BigInteger objectiveValue;
  private int[] prevmodel;
  private boolean[] prevfullmodel;
  private IConstr previousPBConstr;
  private boolean isSolutionOptimal;
  
  public PseudoOptDecorator(IPBSolver paramIPBSolver)
  {
    super(paramIPBSolver);
  }
  
  public boolean isSatisfiable()
    throws TimeoutException
  {
    return isSatisfiable(VecInt.EMPTY);
  }
  
  public boolean isSatisfiable(boolean paramBoolean)
    throws TimeoutException
  {
    return isSatisfiable(VecInt.EMPTY, paramBoolean);
  }
  
  public boolean isSatisfiable(IVecInt paramIVecInt, boolean paramBoolean)
    throws TimeoutException
  {
    boolean bool = super.isSatisfiable(paramIVecInt, true);
    if (bool)
    {
      prevmodel = super.model();
      prevfullmodel = new boolean[nVars()];
      for (int i = 0; i < nVars(); i++) {
        prevfullmodel[i] = ((IPBSolver)decorated()).model(i + 1);
      }
    }
    else if (previousPBConstr != null)
    {
      ((IPBSolver)decorated()).removeConstr(previousPBConstr);
      previousPBConstr = null;
    }
    return bool;
  }
  
  public boolean isSatisfiable(IVecInt paramIVecInt)
    throws TimeoutException
  {
    return isSatisfiable(paramIVecInt, true);
  }
  
  public void setObjectiveFunction(ObjectiveFunction paramObjectiveFunction)
  {
    objfct = paramObjectiveFunction;
    ((IPBSolver)decorated()).setObjectiveFunction(paramObjectiveFunction);
  }
  
  public boolean admitABetterSolution()
    throws TimeoutException
  {
    return admitABetterSolution(VecInt.EMPTY);
  }
  
  public boolean admitABetterSolution(IVecInt paramIVecInt)
    throws TimeoutException
  {
    try
    {
      isSolutionOptimal = false;
      boolean bool = super.isSatisfiable(paramIVecInt, true);
      if (bool)
      {
        prevmodel = super.model();
        prevfullmodel = new boolean[nVars()];
        for (int i = 0; i < nVars(); i++) {
          prevfullmodel[i] = ((IPBSolver)decorated()).model(i + 1);
        }
        if (objfct != null) {
          calculateObjective();
        }
      }
      else
      {
        isSolutionOptimal = true;
        if (previousPBConstr != null)
        {
          ((IPBSolver)decorated()).removeConstr(previousPBConstr);
          previousPBConstr = null;
        }
      }
      return bool;
    }
    catch (TimeoutException localTimeoutException)
    {
      if (previousPBConstr != null)
      {
        ((IPBSolver)decorated()).removeConstr(previousPBConstr);
        previousPBConstr = null;
      }
      throw localTimeoutException;
    }
  }
  
  public boolean hasNoObjectiveFunction()
  {
    return objfct == null;
  }
  
  public boolean nonOptimalMeansSatisfiable()
  {
    return true;
  }
  
  public Number calculateObjective()
  {
    if (objfct == null) {
      throw new UnsupportedOperationException("The problem does not contain an objective function");
    }
    objectiveValue = objfct.calculateDegree(prevmodel);
    return objectiveValue;
  }
  
  public void discardCurrentSolution()
    throws ContradictionException
  {
    if (previousPBConstr != null) {
      super.removeSubsumedConstr(previousPBConstr);
    }
    if ((objfct != null) && (objectiveValue != null)) {
      previousPBConstr = super.addPseudoBoolean(objfct.getVars(), objfct.getCoeffs(), false, objectiveValue.subtract(BigInteger.ONE));
    }
  }
  
  public void reset()
  {
    previousPBConstr = null;
    super.reset();
  }
  
  public int[] model()
  {
    return prevmodel;
  }
  
  public boolean model(int paramInt)
  {
    return prevfullmodel[(paramInt - 1)];
  }
  
  public String toString(String paramString)
  {
    return paramString + "Pseudo Boolean Optimization\n" + super.toString(paramString);
  }
  
  public Number getObjectiveValue()
  {
    return objectiveValue;
  }
  
  public void discard()
    throws ContradictionException
  {
    discardCurrentSolution();
  }
  
  public void forceObjectiveValueTo(Number paramNumber)
    throws ContradictionException
  {
    super.addPseudoBoolean(objfct.getVars(), objfct.getCoeffs(), false, (BigInteger)paramNumber);
  }
  
  public boolean isOptimal()
  {
    return isSolutionOptimal;
  }
}

/* Location:
 * Qualified Name:     org.sat4j.pb.PseudoOptDecorator
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j.pb;

import org.sat4j.core.ASolverFactory;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.IPhaseSelectionStrategy;
import org.sat4j.minisat.learning.ClauseOnlyLearning;
import org.sat4j.minisat.learning.MiniSATLearning;
import org.sat4j.minisat.learning.NoLearningButHeuristics;
import org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy;
import org.sat4j.minisat.orders.RSATPhaseSelectionStrategy;
import org.sat4j.minisat.orders.UserFixedPhaseSelectionStrategy;
import org.sat4j.minisat.orders.VarOrderHeap;
import org.sat4j.minisat.restarts.ArminRestarts;
import org.sat4j.minisat.restarts.MiniSATRestarts;
import org.sat4j.pb.constraints.AbstractPBDataStructureFactory;
import org.sat4j.pb.constraints.CompetMinHTmixedClauseCardConstrDataStructureFactory;
import org.sat4j.pb.constraints.CompetResolutionMinPBLongMixedWLClauseCardConstrDataStructure;
import org.sat4j.pb.constraints.CompetResolutionPBLongMixedHTClauseCardConstrDataStructure;
import org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure;
import org.sat4j.pb.constraints.CompetResolutionPBMixedHTClauseCardConstrDataStructure;
import org.sat4j.pb.constraints.CompetResolutionPBMixedWLClauseCardConstrDataStructure;
import org.sat4j.pb.constraints.PBMaxClauseAtLeastConstrDataStructure;
import org.sat4j.pb.constraints.PBMaxClauseCardConstrDataStructure;
import org.sat4j.pb.constraints.PBMaxDataStructure;
import org.sat4j.pb.constraints.PBMinClauseCardConstrDataStructure;
import org.sat4j.pb.constraints.PBMinDataStructure;
import org.sat4j.pb.constraints.PuebloPBMinClauseAtLeastConstrDataStructure;
import org.sat4j.pb.constraints.PuebloPBMinClauseCardConstrDataStructure;
import org.sat4j.pb.constraints.PuebloPBMinDataStructure;
import org.sat4j.pb.core.PBDataStructureFactory;
import org.sat4j.pb.core.PBSolverCP;
import org.sat4j.pb.core.PBSolverCautious;
import org.sat4j.pb.core.PBSolverClause;
import org.sat4j.pb.core.PBSolverResCP;
import org.sat4j.pb.core.PBSolverResolution;
import org.sat4j.pb.core.PBSolverWithImpliedClause;
import org.sat4j.pb.orders.VarOrderHeapObjective;
import org.sat4j.pb.tools.ManyCorePB;
import org.sat4j.specs.ISolver;
import org.sat4j.tools.DimacsOutputSolver;

public class SolverFactory
  extends ASolverFactory<IPBSolver>
{
  private static final long serialVersionUID = 1L;
  private static SolverFactory instance;
  
  private static synchronized void createInstance()
  {
    if (instance == null) {
      instance = new SolverFactory();
    }
  }
  
  public static SolverFactory instance()
  {
    if (instance == null) {
      createInstance();
    }
    return instance;
  }
  
  public static PBSolverResolution newPBResAllPB()
  {
    return newPBRes(new PBMaxDataStructure());
  }
  
  public static PBSolverCP newPBCPAllPB()
  {
    return newPBCP(new PBMaxDataStructure());
  }
  
  public static IPBSolver newOPBStringSolver()
  {
    return new OPBStringSolver();
  }
  
  public static PBSolverCP newPBCPMixedConstraints()
  {
    return newPBCP(new PBMaxClauseCardConstrDataStructure());
  }
  
  public static PBSolverCP newPBCPMixedConstraintsObjective()
  {
    return newPBCP(new PBMaxClauseCardConstrDataStructure(), new VarOrderHeapObjective());
  }
  
  public static PBSolverCP newCompetPBCPMixedConstraintsObjective()
  {
    return newPBCP(new PBMaxClauseCardConstrDataStructure(), new VarOrderHeapObjective());
  }
  
  public static PBSolverCP newPBCPMixedConstraintsObjectiveLearnJustClauses()
  {
    ClauseOnlyLearning localClauseOnlyLearning = new ClauseOnlyLearning();
    PBSolverCP localPBSolverCP = new PBSolverCP(localClauseOnlyLearning, new PBMaxClauseCardConstrDataStructure(), new VarOrderHeapObjective());
    localClauseOnlyLearning.setSolver(localPBSolverCP);
    return localPBSolverCP;
  }
  
  public static PBSolverCP newCompetPBCPMixedConstraintsObjectiveLearnJustClauses()
  {
    ClauseOnlyLearning localClauseOnlyLearning = new ClauseOnlyLearning();
    PBSolverCP localPBSolverCP = new PBSolverCP(localClauseOnlyLearning, new PBMaxClauseCardConstrDataStructure(), new VarOrderHeapObjective());
    localClauseOnlyLearning.setSolver(localPBSolverCP);
    return localPBSolverCP;
  }
  
  private static PBSolverCP newPBKiller(IPhaseSelectionStrategy paramIPhaseSelectionStrategy)
  {
    ClauseOnlyLearning localClauseOnlyLearning = new ClauseOnlyLearning();
    PBSolverCP localPBSolverCP = new PBSolverCP(localClauseOnlyLearning, new PBMaxClauseCardConstrDataStructure(), new VarOrderHeapObjective(paramIPhaseSelectionStrategy));
    localClauseOnlyLearning.setSolver(localPBSolverCP);
    return localPBSolverCP;
  }
  
  public static PBSolverCP newPBKillerRSAT()
  {
    return newPBKiller(new RSATPhaseSelectionStrategy());
  }
  
  public static PBSolverCP newPBKillerClassic()
  {
    return newPBKiller(new PhaseInLastLearnedClauseSelectionStrategy());
  }
  
  public static PBSolverCP newPBKillerFixed()
  {
    return newPBKiller(new UserFixedPhaseSelectionStrategy());
  }
  
  private static PBSolverCP newCompetPBKiller(IPhaseSelectionStrategy paramIPhaseSelectionStrategy)
  {
    ClauseOnlyLearning localClauseOnlyLearning = new ClauseOnlyLearning();
    PBSolverCP localPBSolverCP = new PBSolverCP(localClauseOnlyLearning, new PBMaxClauseCardConstrDataStructure(), new VarOrderHeapObjective(paramIPhaseSelectionStrategy));
    localClauseOnlyLearning.setSolver(localPBSolverCP);
    return localPBSolverCP;
  }
  
  public static PBSolverCP newCompetPBKillerRSAT()
  {
    return newCompetPBKiller(new RSATPhaseSelectionStrategy());
  }
  
  public static PBSolverCP newCompetPBKillerClassic()
  {
    return newCompetPBKiller(new PhaseInLastLearnedClauseSelectionStrategy());
  }
  
  public static PBSolverCP newCompetPBKillerFixed()
  {
    return newCompetPBKiller(new UserFixedPhaseSelectionStrategy());
  }
  
  public static PBSolverCP newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalReductionToClause()
  {
    MiniSATLearning localMiniSATLearning = new MiniSATLearning();
    PBSolverClause localPBSolverClause = new PBSolverClause(localMiniSATLearning, new PBMaxClauseCardConstrDataStructure(), new VarOrderHeapObjective());
    localMiniSATLearning.setDataStructureFactory(localPBSolverClause.getDSFactory());
    localMiniSATLearning.setVarActivityListener(localPBSolverClause);
    return localPBSolverClause;
  }
  
  public static PBSolverCP newPBCPMixedConstraintsObjectiveNoLearning()
  {
    NoLearningButHeuristics localNoLearningButHeuristics = new NoLearningButHeuristics();
    PBSolverCP localPBSolverCP = new PBSolverCP(localNoLearningButHeuristics, new PBMaxClauseCardConstrDataStructure(), new VarOrderHeapObjective());
    localNoLearningButHeuristics.setSolver(localPBSolverCP);
    localNoLearningButHeuristics.setVarActivityListener(localPBSolverCP);
    return localPBSolverCP;
  }
  
  public static PBSolverResolution newPBResMixedConstraintsObjective()
  {
    MiniSATLearning localMiniSATLearning = new MiniSATLearning();
    PBSolverResolution localPBSolverResolution = new PBSolverResolution(localMiniSATLearning, new PBMaxClauseCardConstrDataStructure(), new VarOrderHeapObjective(), new MiniSATRestarts());
    localMiniSATLearning.setDataStructureFactory(localPBSolverResolution.getDSFactory());
    localMiniSATLearning.setVarActivityListener(localPBSolverResolution);
    return localPBSolverResolution;
  }
  
  public static PBSolverResolution newCompetPBResWLMixedConstraintsObjectiveExpSimp()
  {
    return newCompetPBResMixedConstraintsObjectiveExpSimp(new CompetResolutionPBMixedWLClauseCardConstrDataStructure());
  }
  
  public static PBSolverResolution newCompetPBResHTMixedConstraintsObjectiveExpSimp()
  {
    return newCompetPBResMixedConstraintsObjectiveExpSimp(new CompetResolutionPBMixedHTClauseCardConstrDataStructure());
  }
  
  public static PBSolverResolution newCompetPBResLongHTMixedConstraintsObjectiveExpSimp()
  {
    return newCompetPBResMixedConstraintsObjectiveExpSimp(new CompetResolutionPBLongMixedHTClauseCardConstrDataStructure());
  }
  
  public static PBSolverResolution newCompetPBResLongWLMixedConstraintsObjectiveExpSimp()
  {
    return newCompetPBResMixedConstraintsObjectiveExpSimp(new CompetResolutionPBLongMixedWLClauseCardConstrDataStructure());
  }
  
  public static PBSolverResolution newCompetMinPBResLongWLMixedConstraintsObjectiveExpSimp()
  {
    return newCompetPBResMixedConstraintsObjectiveExpSimp(new CompetResolutionMinPBLongMixedWLClauseCardConstrDataStructure());
  }
  
  public static PBSolverResolution newCompetPBResMixedConstraintsObjectiveExpSimp(PBDataStructureFactory paramPBDataStructureFactory)
  {
    MiniSATLearning localMiniSATLearning = new MiniSATLearning();
    PBSolverResolution localPBSolverResolution = new PBSolverResolution(localMiniSATLearning, paramPBDataStructureFactory, new VarOrderHeapObjective(new RSATPhaseSelectionStrategy()), new ArminRestarts());
    localMiniSATLearning.setDataStructureFactory(localPBSolverResolution.getDSFactory());
    localMiniSATLearning.setVarActivityListener(localPBSolverResolution);
    localPBSolverResolution.setSimplifier(EXPENSIVE_SIMPLIFICATION);
 
1 2 3 4 5 6 7 8

Further reading...

For more information on Java 1.5 Tiger, you may find Java 1.5 Tiger, A developer's Notebook by D. Flanagan and B. McLaughlin from O'Reilly of interest.

New!JAR listings


Copyright 2006-2017. Infinite Loop Ltd