Commit 0332b1a8 authored by Daniel Le Berre's avatar Daniel Le Berre

Test case showing the issue reported in bug report SAT-84.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1651 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent 2856f40a
package org.sat4j.maxsat;
import static org.junit.Assert.*;
import java.math.BigInteger;
import org.junit.Test;
import org.sat4j.core.VecInt;
import org.sat4j.pb.OptToPBSATAdapter;
import org.sat4j.pb.PseudoOptDecorator;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IProblem;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.TimeoutException;
public class BugSAT84 {
@Test
public void test() throws ContradictionException, TimeoutException {
WeightedMaxSatDecorator wms = new WeightedMaxSatDecorator(SolverFactory.newDefault());
wms.newVar(401432);
wms.setExpectedNumberOfClauses(1);
wms.setTopWeight(BigInteger.valueOf(729));
IVecInt clause = new VecInt().push(-378671).push(59559);
wms.addSoftClause(BigInteger.valueOf(729),clause);
IProblem problem = new OptToPBSATAdapter(new PseudoOptDecorator(wms,false,true));
assertTrue(problem.isSatisfiable());
}
}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment