Commit 1edae46b authored by Daniel Le Berre's avatar Daniel Le Berre

Initial import for maxsat component in Maven structure.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@16 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent 912623e5
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
<classpathentry kind="src" path="src/main/java"/>
<classpathentry kind="src" path="src/test/java"/>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/>
<classpathentry kind="con" path="org.eclipse.jdt.junit.JUNIT_CONTAINER/4"/>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="output" path="bin"/>
</classpath>
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>org.sat4j.maxsat</name>
<comment></comment>
<projects>
</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.maxsat
Bundle-Version: 9.9.9.token
Export-Package: org.sat4j.maxsat,
org.sat4j.maxsat.reader
Bundle-Vendor: %providerName
Bundle-Localization: plugin
Require-Bundle: org.sat4j.core,
org.sat4j.pb,
org.apache.commons.cli;bundle-version="1.0.0"
Built-By: Daniel Le Berre
Main-Class: org.sat4j.maxsat.GenericOptLauncher
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.pb.jar lib/commons-cli.jar
bin.includes = META-INF/,\
lib/commons-cli.jar,\
plugin.properties
bundleName = SAT4J Pseudo
providerName = CRIL CNRS UMR 8188 - Universite d'Artois
<?xml version="1.0" encoding="UTF-8"?><project>
<modelVersion>4.0.0</modelVersion>
<parent>
<groupId>org.sat4j</groupId>
<artifactId>org.sat4j.pom</artifactId>
<version>2.0.0</version>
</parent>
<artifactId>org.sat4j.maxsat</artifactId>
<name>SAT4J maxsat</name>
<dependencies>
<dependency>
<groupId>org.sat4j</groupId>
<artifactId>org.sat4j.core</artifactId>
<version>2.0.0</version>
<scope>compile</scope>
</dependency>
<dependency>
<groupId>org.sat4j</groupId>
<artifactId>org.sat4j.pb</artifactId>
<version>2.0.0</version>
<scope>compile</scope>
</dependency>
<dependency>
<groupId>commons-cli</groupId>
<artifactId>commons-cli</artifactId>
<version>1.0</version>
<scope>compile</scope>
</dependency>
</dependencies>
</project>
/*******************************************************************************
* 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.
*******************************************************************************/
package org.sat4j.maxsat;
import static java.lang.System.out;
import org.apache.commons.cli.CommandLine;
import org.apache.commons.cli.HelpFormatter;
import org.apache.commons.cli.Options;
import org.apache.commons.cli.ParseException;
import org.apache.commons.cli.PosixParser;
import org.sat4j.AbstractLauncher;
import org.sat4j.AbstractOptimizationLauncher;
import org.sat4j.maxsat.reader.P2DimacsReader;
import org.sat4j.maxsat.reader.WDimacsReader;
import org.sat4j.opt.MaxSatDecorator;
import org.sat4j.opt.MinOneDecorator;
import org.sat4j.pb.IPBSolver;
import org.sat4j.reader.DimacsReader;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ISolver;
/**
* Generic launcher to be used for solving optimization problems.
*
* @author daniel
*
*/
public class GenericOptLauncher extends AbstractOptimizationLauncher {
/**
*
*/
private static final long serialVersionUID = 1L;
@SuppressWarnings("nls")
private Options createCLIOptions() {
Options options = new Options();
options.addOption("t", "timeout", true,
"specifies the timeout (in seconds)");
options.addOption("T", "timeoutms", true,
"specifies the timeout (in milliseconds)");
options.addOption("k", "kind", true,
"kind of problem: minone, maxsat, etc.");
return options;
}
@Override
public void displayLicense() {
super.displayLicense();
log("This software uses some libraries from the Jakarta Commons project. See jakarta.apache.org for details."); //$NON-NLS-1$
}
@Override
public void usage() {
out.println("java -jar sat4j-maxsat.jar instance-name"); //$NON-NLS-1$
}
@Override
protected Reader createReader(ISolver solver, String problemname) {
if (problemname.endsWith(".wcnf")) { //$NON-NLS-1$
return new WDimacsReader((IPBSolver) solver); //$NON-NLS-1$
} else if (problemname.endsWith("p2cnf")) {
return new P2DimacsReader((MinCostDecorator)solver);
}
return new DimacsReader(solver);
}
@Override
protected String getInstanceName(String[] args) {
return args[args.length - 1];
}
@Override
protected ISolver configureSolver(String[] args) {
ISolver asolver = null;
Options options = createCLIOptions();
if (args.length == 0) {
HelpFormatter helpf = new HelpFormatter();
helpf.printHelp("java -jar sat4j-maxsat.jar", options, true);
} else {
try {
CommandLine cmd = new PosixParser().parse(options, args);
int problemindex = args.length - 1;
String kind = cmd.getOptionValue("k"); //$NON-NLS-1$
if (kind == null) { //$NON-NLS-1$
kind = "maxsat";
}
if ("minone".equalsIgnoreCase(kind)) {
asolver = new MinOneDecorator(SolverFactory.newLight());
} else if ("mincost".equalsIgnoreCase(kind)||args[problemindex].endsWith(".p2cnf")) {
asolver = new MinCostDecorator(SolverFactory.newLight());
} else {
assert "maxsat".equalsIgnoreCase(kind);
if (args[problemindex].endsWith(".wcnf")) { //$NON-NLS-1$
asolver = new WeightedMaxSatDecorator(SolverFactory
.newLight());
} else {
asolver = new MaxSatDecorator(SolverFactory
.newMiniMaxSAT());
}
}
String timeout = cmd.getOptionValue("t");
if (timeout == null) {
timeout = cmd.getOptionValue("T");
if (timeout != null) {
asolver.setTimeoutMs(Long.parseLong(timeout));
}
} else {
asolver.setTimeout(Integer.parseInt(timeout));
}
log(asolver.toString(COMMENT_PREFIX));
} catch (ParseException e1) {
HelpFormatter helpf = new HelpFormatter();
helpf.printHelp("java -jar sat4jopt.jar", options, true);
}
}
return asolver;
}
public static void main(String[] args) {
AbstractLauncher lanceur = new GenericOptLauncher();
lanceur.run(args);
}
}
/*******************************************************************************
* 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.
*******************************************************************************/
package org.sat4j.maxsat;
import java.math.BigInteger;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.PBSolverDecorator;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IOptimizationProblem;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.TimeoutException;
/**
* A decorator that computes minimal cost models. That problem is also known as binate covering problem.
*
* Please make sure that newVar(howmany) is called first to setup the decorator.
*
* @author daniel
*
*/
public class MinCostDecorator extends PBSolverDecorator implements
IOptimizationProblem {
/**
*
*/
private static final long serialVersionUID = 1L;
private int[] costs;
private int[] prevmodel;
private final IVecInt vars = new VecInt();
private final IVec<BigInteger> coeffs = new Vec<BigInteger>();
public MinCostDecorator(IPBSolver solver) {
super(solver);
}
/*
* (non-Javadoc)
*
* @see org.sat4j.tools.SolverDecorator#newVar()
*/
@Override
public int newVar() {
throw new UnsupportedOperationException();
}
/**
* Setup the number of variables to use inside the solver.
*
* It is mandatory to call that method before setting the cost of the
* variables.
*
* @param howmany
* the maximum number of variables in the solver.
*/
@Override
public int newVar(int howmany) {
costs = new int[howmany + 1];
// Arrays.fill(costs, 1);
vars.clear();
coeffs.clear();
for (int i = 1; i <= howmany; i++) {
vars.push(i);
coeffs.push(BigInteger.ZERO);
}
// should the default cost be 1????
// here it is 0
return super.newVar(howmany);
}
/**
* to know the cost of a given var.
*
* @param var
* a variable in dimacs format
* @return the cost of that variable when assigned to true
*/
public int costOf(int var) {
return costs[var];
}
/**
* to set the cost of a given var.
*
* @param var
* a variable in dimacs format
* @param cost
* the cost of var when assigned to true
*/
public void setCost(int var, int cost) {
costs[var] = cost;
coeffs.set(var - 1, BigInteger.valueOf(cost));
}
public boolean admitABetterSolution() throws TimeoutException {
boolean result = super.isSatisfiable(true);
if (result)
prevmodel = super.model();
return result;
}
public boolean hasNoObjectiveFunction() {
return false;
}
public boolean nonOptimalMeansSatisfiable() {
return true;
}
public Number calculateObjective() {
return new Integer(calculateDegree(prevmodel));
}
private int calculateDegree(int[] prevmodel2) {
int tmpcost = 0;
for (int i = 1; i < costs.length; i++) {
if (prevmodel2[i - 1] > 0) {
tmpcost += costs[i];
}
}
return tmpcost;
}
public void discard() throws ContradictionException {
super.addPseudoBoolean(vars, coeffs, false, BigInteger
.valueOf(calculateDegree(prevmodel) - 1));
}
@Override
public int[] model() {
// DLB findbugs ok
return prevmodel;
}
}
/*******************************************************************************
* 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.
*******************************************************************************/
package org.sat4j.maxsat;
import org.sat4j.core.ASolverFactory;
import org.sat4j.minisat.constraints.MixedDataStructureDaniel;
import org.sat4j.minisat.core.DataStructureFactory;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.SearchParams;
import org.sat4j.minisat.core.Solver;
import org.sat4j.minisat.learning.MiniSATLearning;
import org.sat4j.minisat.orders.VarOrderHeap;
import org.sat4j.minisat.restarts.MiniSATRestarts;
import org.sat4j.minisat.uip.FirstUIP;
import org.sat4j.pb.IPBSolver;
public class SolverFactory extends ASolverFactory<IPBSolver> {
private static final long serialVersionUID = 1L;
/**
* Builds a SAT solver for the MAX sat evaluation. Full clause learning, no
* restarts,
*
* @return a
*/
public static Solver<ILits,DataStructureFactory<ILits>> newMiniMaxSAT() {
MiniSATLearning<ILits,DataStructureFactory<ILits>> learning = new MiniSATLearning<ILits,DataStructureFactory<ILits>>();
Solver<ILits,DataStructureFactory<ILits>> solver = new Solver<ILits,DataStructureFactory<ILits>>(new FirstUIP(), learning,
new MixedDataStructureDaniel(), new SearchParams(1.2,
100000), new VarOrderHeap<ILits>(),
new MiniSATRestarts());
learning.setDataStructureFactory(solver.getDSFactory());
learning.setVarActivityListener(solver);
return solver;
}
@Override
public IPBSolver defaultSolver() {
return newDefault();
}
@Override
public IPBSolver lightSolver() {
return newLight();
}
public static IPBSolver newDefault() {
return org.sat4j.pb.SolverFactory.newDefault();
}
public static IPBSolver newLight() {
return org.sat4j.pb.SolverFactory.newLight();
}
}
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le
*
* 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.
*******************************************************************************/
package org.sat4j.maxsat;
import java.math.BigInteger;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.core.DataStructureFactory;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.Solver;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.ObjectiveFunction;
import org.sat4j.pb.PBSolverDecorator;
import org.sat4j.pb.orders.VarOrderHeapObjective;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.IOptimizationProblem;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.TimeoutException;
/**
* A decorator for solving weighted MAX SAT problems.
*
* The first value of the list of literals in the addClause() method contains
* the weight of the clause.
*
* @author daniel
*
*/
public class WeightedMaxSatDecorator extends PBSolverDecorator implements
IOptimizationProblem {
/**
*
*/
private static final long serialVersionUID = 1L;
protected int nborigvars;
private int nbexpectedclauses;
private long falsifiedWeight;
protected int nbnewvar;
protected int[] prevfullmodel;
public WeightedMaxSatDecorator(IPBSolver solver) {
super(solver);
IOrder<?> order = ((Solver<?, ? extends DataStructureFactory<?>>) solver)
.getOrder();
if (order instanceof VarOrderHeapObjective) {
((VarOrderHeapObjective) order).setObjectiveFunction(obj);
}
}
@Override
public int newVar(int howmany) {
nborigvars = super.newVar(howmany);
return nborigvars;
}
@Override
public void setExpectedNumberOfClauses(int nb) {
nbexpectedclauses = nb;
lits.ensure(nb);
falsifiedWeight = 0;
super.setExpectedNumberOfClauses(nb);
super.newVar(nborigvars + nbexpectedclauses);
}
@Override
public int[] model() {
int[] shortmodel = new int[nborigvars];
for (int i = 0; i < nborigvars; i++) {
shortmodel[i] = prevfullmodel[i];
}
return shortmodel;
}
protected int top = -1;
public void setTopWeight(int top) {
this.top = top;
}
@Override
public IConstr addClause(IVecInt literals) throws ContradictionException {
int weight = literals.get(0);
if (weight < top) {
BigInteger bigweight = BigInteger.valueOf(weight);
if (literals.size() == 2) {
// if there is only a coefficient and a literal, no need to
// create
// a new variable
// check first if the literal is already in the list:
int lit = -literals.get(1);
int index = lits.containsAt(lit);
if (index != -1) {
coefs.set(index, coefs.get(index).add(bigweight));
} else {
// check if the opposite literal is already there
index = lits.containsAt(-lit);
if (index != -1) {
falsifiedWeight += weight;
BigInteger oldw = coefs.get(index);
BigInteger diff = oldw.subtract(bigweight);
if (diff.signum() > 0) {
coefs.set(index, diff);
} else if (diff.signum() < 0) {
lits.set(index, lit);
coefs.set(index, diff.abs());
// remove from falsifiedWeight the
// part of the weight that will remain
// in the objective function
falsifiedWeight += diff.intValue();
} else {
assert diff.signum() == 0;
lits.delete(index);
coefs.delete(index);
}
} else {
lits.push(lit);
coefs.push(bigweight);
}
}
return null;
}
coefs.push(bigweight);
int newvar = nborigvars + ++nbnewvar;
literals.set(0, newvar);
lits.push(newvar);
} else {
literals.delete(0);
}
return super.addClause(literals);
}
public boolean admitABetterSolution() throws TimeoutException {
boolean result = super.isSatisfiable(true);
if (result) {
int nbtotalvars = nborigvars + nbnewvar;
if (prevfullmodel == null)
prevfullmodel = new int[nbtotalvars];
for (int i = 1; i <= nbtotalvars; i++) {
prevfullmodel[i - 1] = super.model(i) ? i : -i;
}
}
return result;
}
@Override
public void reset() {
coefs.clear();
lits.clear();
nbnewvar = 0;
super.reset();
}
public boolean hasNoObjectiveFunction() {
return false;
}
public boolean nonOptimalMeansSatisfiable() {
return false;
}
private int counter;
public Number calculateObjective() {
counter = 0;
for (int q : prevfullmodel) {
int index = lits.containsAt(q);
if (index != -1) {
counter += coefs.get(index).intValue();
}
}
return falsifiedWeight + counter;
}
private final IVecInt lits = new VecInt();
private final IVec<BigInteger> coefs = new Vec<BigInteger>();
private final ObjectiveFunction obj = new ObjectiveFunction(lits, coefs);
public void discard() throws ContradictionException {
assert lits.size() == coefs.size();
super.addPseudoBoolean(lits, coefs, false, BigInteger
.valueOf(counter - 1));
}
}
<body>
MAXSAT and Weighted Max SAT framework.
<p>
That package contains various optimization decorators for solving optimization
problems such as MAX-SA