Commit 3341f79c authored by Daniel Le Berre's avatar Daniel Le Berre

Initial code for mavenized 2.0.0 release of SAT4J pseudo.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@11 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent a870d87e
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
<classpathentry kind="src" path="src/main/java"/>
<classpathentry excluding="org/sat4j/reader/GoodOPBReaderTest.java" kind="src" path="src/test/java"/>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="con" path="org.eclipse.jdt.junit.JUNIT_CONTAINER/3"/>
<classpathentry kind="output" path="bin"/>
</classpath>
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>org.sat4j.pb</name>
<comment></comment>
<projects>
<project>sat4j</project>
</projects>
<buildSpec>
<buildCommand>
<name>org.eclipse.jdt.core.javabuilder</name>
<arguments>
</arguments>
</buildCommand>
<buildCommand>
<name>org.eclipse.pde.ManifestBuilder</name>
<arguments>
</arguments>
</buildCommand>
<buildCommand>
<name>org.eclipse.pde.SchemaBuilder</name>
<arguments>
</arguments>
</buildCommand>
</buildSpec>
<natures>
<nature>org.eclipse.jdt.core.javanature</nature>
<nature>org.eclipse.pde.PluginNature</nature>
</natures>
</projectDescription>
Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: %bundleName
Bundle-SymbolicName: org.sat4j.pb
Bundle-Version: 9.9.9.token
Export-Package: org.sat4j.pb,
org.sat4j.pb.constraints,
org.sat4j.pb.constraints.pb,
org.sat4j.pb.core,
org.sat4j.pb.orders,
org.sat4j.pb.reader
Bundle-Vendor: %providerName
Bundle-Localization: plugin
Require-Bundle: org.sat4j.core
Built-By: Daniel Le Berre
Main-Class: org.sat4j.pb.LanceurPseudo2007
Specification-Title: SAT4J
Specification-Version: NA
Specification-Vendor: Daniel Le Berre
Implementation-Title: SAT4J
Implementation-Version: 2.0
Implementation-Vendor: CRIL CNRS UMR 8188 - Universite d'Artois
Class-Path: org.sat4j.core.jar
Bundle-RequiredExecutionEnvironment: J2SE-1.4
bin.includes = META-INF/,\
plugin.properties,\
.,\
src/main/resources/about.html
jars.compile.order = .
source.. = src/
output.. = bin/
###############################################################################
# SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
#
# All rights reserved. This program and the accompanying materials
# are made available under the terms of the Eclipse Public License v1.0
# which accompanies this distribution, and is available at
# http://www.eclipse.org/legal/epl-v10.html
#
# Alternatively, the contents of this file may be used under the terms of
# either the GNU Lesser General Public License Version 2.1 or later (the
# "LGPL"), in which case the provisions of the LGPL are applicable instead
# of those above. If you wish to allow use of your version of this file only
# under the terms of the LGPL, and not to allow others to use your version of
# this file under the terms of the EPL, indicate your decision by deleting
# the provisions above and replace them with the notice and other provisions
# required by the LGPL. If you do not delete the provisions above, a recipient
# may use your version of this file under the terms of the EPL or the LGPL.
#
# Based on the original MiniSat specification from:
#
# An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
# Sixth International Conference on Theory and Applications of Satisfiability
# Testing, LNCS 2919, pp 502-518, 2003.
#
# See www.minisat.se for the original solver in C++.
#
###############################################################################
bundleName = SAT4J Pseudo
providerName = CRIL CNRS UMR 8188 - Universite d'Artois
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*
* Based on the pseudo boolean algorithms described in:
* A fast pseudo-Boolean constraint solver Chai, D.; Kuehlmann, A.
* Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
* Volume 24, Issue 3, March 2005 Page(s): 305 - 317
*
* and
* Heidi E. Dixon, 2004. Automating Pseudo-Boolean Inference within a DPLL
* Framework. Ph.D. Dissertation, University of Oregon.
*******************************************************************************/
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;
/**
* A solver able to deal with pseudo boolean constraints.
*
* @author daniel
*
*/
public interface IPBSolver extends ISolver {
/**
* Create a Pseudo-Boolean constraint of the type "at least n of those
* literals must be satisfied"
*
* @param lits
* a set of literals. The vector can be reused since the solver
* is not supposed to keep a reference to that vector.
* @param coeffs
* the coefficients of the literals. The vector can be reused
* since the solver is not supposed to keep a reference to that
* vector.
* @param moreThan
* true if it is a constraint >= degree
* @param d
* the degree of the cardinality constraint
* @return a reference to the constraint added in the solver, to use in
* removeConstr().
* @throws ContradictionException
* iff the vector of literals is empty or if the constraint is
* falsified after unit propagation
* @see #removeConstr(IConstr)
*/
IConstr addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs,
boolean moreThan, BigInteger d) throws ContradictionException;
public void setListOfVariablesForExplanation(IVecInt listOfVariables);
public String getExplanation();
public void setObjectiveFunction(ObjectiveFunction obj);
}
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*
* Based on the pseudo boolean algorithms described in:
* A fast pseudo-Boolean constraint solver Chai, D.; Kuehlmann, A.
* Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
* Volume 24, Issue 3, March 2005 Page(s): 305 - 317
*
* and
* Heidi E. Dixon, 2004. Automating Pseudo-Boolean Inference within a DPLL
* Framework. Ph.D. Dissertation, University of Oregon.
*******************************************************************************/
package org.sat4j.pb;
import static java.lang.System.out;
import org.sat4j.AbstractLauncher;
import org.sat4j.AbstractOptimizationLauncher;
import org.sat4j.pb.reader.OPBReader2006;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ISolver;
/**
* Launcher especially dedicated to the pseudo boolean 05 evaluation (@link
* http://www.cril.univ-artois.fr/PB05/).
*
* @author mederic
*/
public class LanceurPseudo2005 extends AbstractOptimizationLauncher {
/**
*
*/
private static final long serialVersionUID = 1L;
/**
* Lance le prouveur sur un fichier Dimacs
*
* @param args
* doit contenir le nom d'un fichier Dimacs, eventuellement
* compress?.
*/
public static void main(final String[] args) {
final AbstractLauncher lanceur = new LanceurPseudo2005();
lanceur.run(args);
System.exit(lanceur.getExitCode().value());
}
protected ObjectiveFunction obfct;
/*
* (non-Javadoc)
*
* @see org.sat4j.Lanceur#createReader(org.sat4j.specs.ISolver)
*/
@Override
protected Reader createReader(ISolver solver, String problemname) {
return new OPBReader2006((IPBSolver)solver);
}
/*
* (non-Javadoc)
*
* @see org.sat4j.Lanceur#configureSolver(java.lang.String[])
*/
@Override
protected ISolver configureSolver(String[] args) {
IPBSolver solver;
if (args.length > 1) {
solver = SolverFactory.instance().createSolverByName(args[0]);
} else {
solver = SolverFactory.newDefault();
}
solver = new PseudoOptDecorator(solver);
// solver.setTimeout(Integer.MAX_VALUE);
out.println(solver.toString(COMMENT_PREFIX)); //$NON-NLS-1$
return solver;
}
@Override
public void usage() {
out.println("java -jar sat4j-pb.jar [solvername] instancename.opb"); //$NON-NLS-1$
showAvailableSolvers(SolverFactory.instance());
}
@Override
protected String getInstanceName(String[] args) {
assert args.length == 1 || args.length == 2;
return args[args.length - 1];
}
}
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*
* Based on the pseudo boolean algorithms described in:
* A fast pseudo-Boolean constraint solver Chai, D.; Kuehlmann, A.
* Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
* Volume 24, Issue 3, March 2005 Page(s): 305 - 317
*
* and
* Heidi E. Dixon, 2004. Automating Pseudo-Boolean Inference within a DPLL
* Framework. Ph.D. Dissertation, University of Oregon.
*******************************************************************************/
package org.sat4j.pb;
import org.sat4j.AbstractLauncher;
import org.sat4j.pb.reader.OPBReader2007;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ISolver;
/**
* Launcher for the Pseudo Boolean 2007 competition.
*
* @author daniel
*
*/
public class LanceurPseudo2007 extends LanceurPseudo2005 {
/**
*
*/
private static final long serialVersionUID = 1L;
@Override
protected Reader createReader(ISolver solver, String problemname) {
return new OPBReader2007((IPBSolver)solver);
}
/**
* Lance le prouveur sur un fichier Dimacs
*
* @param args
* doit contenir le nom d'un fichier Dimacs, eventuellement
* compress?.
*/
public static void main(final String[] args) {
final AbstractLauncher lanceur = new LanceurPseudo2007();
if (args.length==0||args.length>2) {
lanceur.usage();
return;
}
lanceur.run(args);
System.exit(lanceur.getExitCode().value());
}
}
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*
* Based on the pseudo boolean algorithms described in:
* A fast pseudo-Boolean constraint solver Chai, D.; Kuehlmann, A.
* Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
* Volume 24, Issue 3, March 2005 Page(s): 305 - 317
*
* and
* Heidi E. Dixon, 2004. Automating Pseudo-Boolean Inference within a DPLL
* Framework. Ph.D. Dissertation, University of Oregon.
*******************************************************************************/
package org.sat4j.pb;
import org.sat4j.AbstractLauncher;
import org.sat4j.ExitCode;
import org.sat4j.pb.reader.OPBEclipseReader2007;
import org.sat4j.reader.Reader;
import org.sat4j.specs.IProblem;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.TimeoutException;
public class LanceurPseudo2007Eclipse extends LanceurPseudo2007 {
/**
*
*/
private static final long serialVersionUID = 1L;
public LanceurPseudo2007Eclipse() {
// TODO Auto-generated constructor stub
}
@Override
protected void solve(IProblem problem) throws TimeoutException {
IVecInt list = ((OPBEclipseReader2007) getReader())
.getListOfVariables();
if (list != null && !list.isEmpty()){
((PseudoOptDecorator) problem).setListOfVariablesForExplanation(list);
}
super.solve(problem);
}
@Override
protected Reader createReader(ISolver solver, String problemname) {
return new OPBEclipseReader2007((IPBSolver)solver);
}
/**
* Lance le prouveur sur un fichier Dimacs
*
* @param args
* doit contenir le nom d'un fichier Dimacs, eventuellement
* compress?.
*/
public static void main(final String[] args) {
final AbstractLauncher lanceur = new LanceurPseudo2007Eclipse();
if (args.length==0||args.length>2) {
lanceur.usage();
return;
}
lanceur.run(args);
System.exit(lanceur.getExitCode().value());
}
@Override
protected void displayAnswer(){
super.displayAnswer();
ExitCode exitCode = getExitCode();
if (exitCode == ExitCode.UNSATISFIABLE)
getLogWriter().println(((IPBSolver)solver).getExplanation());
}
}
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*
* Based on the original MiniSat specification from:
*
* An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
* Sixth International Conference on Theory and Applications of Satisfiability
* Testing, LNCS 2919, pp 502-518, 2003.
*
* See www.minisat.se for the original solver in C++.
*
*******************************************************************************/
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.tools.DimacsStringSolver;
/**
* Solver used to display in a string the pb-instance in OPB format.
*
* That solver is useful to produce OPB files to be used by third party solvers.
*
* @author parrain
*
*/
public class OPBStringSolver extends DimacsStringSolver implements IPBSolver {
/**
*
*/
private static final long serialVersionUID = 1L;
private int indxConstrObj;
private int nbOfConstraints;
/**
*
*/
public OPBStringSolver() {
// TODO Auto-generated constructor stub
}
/**
* @param initSize
*/
public OPBStringSolver(int initSize) {
super(initSize);
// TODO Auto-generated constructor stub
}
public IConstr addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs,
boolean moreThan, BigInteger d) throws ContradictionException {
StringBuffer out = getOut();
assert lits.size() == coeffs.size();
nbOfConstraints ++;
if (moreThan) {
for (int i = 0; i <lits.size();i++)
out.append(coeffs.get(i)+" x"+ lits.get(i) + " ");
out.append(">= "+d+" ;\n");
}
else {
for (int i = 0; i <lits.size();i++)
out.append(coeffs.get(i).negate()+" x"+ lits.get(i) + " ");
out.append(">= "+d.negate()+" ;\n");
}
return null;
}
public void setObjectiveFunction(ObjectiveFunction obj) {
StringBuffer out = getOut();
StringBuffer tmp = new StringBuffer();
tmp.append(" #constraint= "+nbOfConstraints+" \n");
tmp.append("min : ");
IVecInt lits = obj.getVars();
IVec<BigInteger> coeffs = obj.getCoeffs();
for (int i = 0; i <lits.size();i++)
tmp.append(coeffs.get(i)+" x"+ lits.get(i) + " ");
tmp.append(" ;\n");
out.insert(indxConstrObj,tmp);
}
public IConstr addAtLeast(IVecInt literals, int degree)
throws ContradictionException {
StringBuffer out = getOut();
nbOfConstraints++;
for (IteratorInt iterator = literals.iterator();iterator.hasNext();)
out.append("+1 x"+iterator.next() + " ");
out.append(">= "+degree+" ;\n");
return null;
}
public IConstr addAtMost(IVecInt literals, int degree)
throws ContradictionException {
StringBuffer out = getOut();
nbOfConstraints++;
for (IteratorInt iterator = literals.iterator();iterator.hasNext();)
out.append("-1 x"+iterator.next() + " ");
out.append(">= "+(-degree)+" ;\n");
return null;
}
public IConstr addClause(IVecInt literals) throws ContradictionException {
StringBuffer out = getOut();
nbOfConstraints++;
for (IteratorInt iterator = literals.iterator();iterator.hasNext();)
out.append("+1 x"+iterator.next() + " ");
out.append(">= 1 ;\n");
return null;
}
/* (non-Javadoc)
* @see org.sat4j.pb.IPBSolver#getExplanation()
*/
public String getExplanation() {
// TODO Auto-generated method stub
return null;
}
/* (non-Javadoc)
* @see org.sat4j.pb.IPBSolver#setListOfVariablesForExplanation(org.sat4j.specs.IVecInt)
*/
public void setListOfVariablesForExplanation(IVecInt listOfVariables) {
// TODO Auto-generated method stub
}
public String toString(){
return getOut().toString();
}
public String toString(String prefix) {
return "OPB output solver";
}
public int newVar(int howmany) {
StringBuffer out = getOut();
out.append("* #variable= " + howmany);
setNbVars(howmany);
// to add later the number of constraints
indxConstrObj = out.length();
return 0;
}
public void setExpectedNumberOfClauses(int nb) {
}
}
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*
* Based on the pseudo boolean algorithms described in:
* A fast pseudo-Boolean constraint solver Chai, D.; Kuehlmann, A.
* Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
* Volume 24, Issue 3, March 2005 Page(s): 305 - 317
*
* and
* Heidi E. Dixon, 2004. Automating Pseudo-Boolean Inference within a DPLL
* Framework. Ph.D. Dissertation, University of Oregon.
*******************************************************************************/
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;
/**
* Abstraction for an Objective Function for Pseudo Boolean Optimization.
*