Commit 7de2fa4d authored by Romain WALLON's avatar Romain WALLON

Merge branch 'master' of https://gitlab.ow2.org/sat4j/sat4j.git

parents 1baa36f7 2e239a3b
Pipeline #2936 failed with stages
in 34 minutes and 14 seconds
......@@ -595,9 +595,8 @@ public class Solver<D extends DataStructureFactory>
int counter = 0;
int p = ILits.UNDEFINED;
// placeholder for the asserting literal
outLearnt.push(ILits.UNDEFINED);
// reserve de la place pour le litteral falsifie
int outBtlevel = 0;
IConstr prevConfl = null;
......@@ -611,9 +610,9 @@ public class Solver<D extends DataStructureFactory>
// Trace reason for p
for (int j = 0; j < preason.size(); j++) {
int q = preason.get(j);
this.order.updateVar(q);
if (!seen[q >> 1]) {
seen[q >> 1] = true;
this.order.updateVar(q);
if (this.voc.getLevel(q) == decisionLevel()) {
counter++;
this.order.updateVarAtDecisionLevel(q);
......
......@@ -39,7 +39,7 @@ import org.sat4j.specs.IProblem;
import org.sat4j.specs.ISolver;
/**
* An reader having the responsability to choose the right reader according to
* An reader having the responsibility to choose the right reader according to
* the input.
*
* @author leberre
......@@ -58,6 +58,11 @@ public class InstanceReader extends Reader {
private final ISolver solver;
public InstanceReader(ISolver solver, Reader reader) {
this.solver = solver;
this.reader = reader;
}
public InstanceReader(ISolver solver) {
// dimacs = new DimacsReader(solver);
this.solver = solver;
......@@ -94,8 +99,8 @@ public class InstanceReader extends Reader {
}
@Override
public IProblem parseInstance(String filename) throws ParseFormatException,
IOException, ContradictionException {
public IProblem parseInstance(String filename)
throws ParseFormatException, IOException, ContradictionException {
String fname;
String prefix = "";
......@@ -105,7 +110,7 @@ public class InstanceReader extends Reader {
}
if (filename.indexOf(':') != -1) {
String[] parts = filename.split(":");
String[] parts = filename.split(":", 2);
filename = parts[1];
prefix = parts[0].toUpperCase(Locale.getDefault());
......@@ -116,7 +121,9 @@ public class InstanceReader extends Reader {
} else {
fname = filename;
}
this.reader = handleFileName(fname, prefix);
if (this.reader == null) {
this.reader = handleFileName(fname, prefix);
}
return this.reader.parseInstance(filename);
}
......
package org.sat4j;
import java.io.IOException;
import org.junit.Test;
import org.mockito.Mockito;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.reader.InstanceReader;
import org.sat4j.reader.ParseFormatException;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ContradictionException;
public class BugSAT145 {
@Test
public void testWindowsPath()
throws ParseFormatException, IOException, ContradictionException {
Reader mockReader = Mockito.mock(Reader.class);
InstanceReader instanceReader = new InstanceReader(
SolverFactory.newDefault(), mockReader);
instanceReader
.parseInstance("EZCNF:C:\\projects\\bla\\testcomments.cnf");
Mockito.verify(mockReader)
.parseInstance("C:\\projects\\bla\\testcomments.cnf");
}
@Test
public void testUnixPath()
throws ParseFormatException, IOException, ContradictionException {
Reader mockReader = Mockito.mock(Reader.class);
InstanceReader instanceReader = new InstanceReader(
SolverFactory.newDefault(), mockReader);
instanceReader.parseInstance("EZCNF:/projects/bla/testcomments.cnf");
Mockito.verify(mockReader)
.parseInstance("/projects/bla/testcomments.cnf");
}
}
......@@ -383,7 +383,7 @@ public class ModelIteratorTest {
}
}
@Test(timeout = 6000)
@Test(timeout = 12000)
public void testGlobalTimeoutCounter() {
SolutionCounter counter = new SolutionCounter(
SolverFactory.newDefault());
......@@ -402,7 +402,8 @@ public class ModelIteratorTest {
}
}
@Test(timeout = 6000)
// This timed test tend to fail when the test server is loaded ...
@Test(timeout = 12000)
public void testGlobalTimeoutIterator() {
ModelIterator iterator = new ModelIterator(SolverFactory.newDefault());
IVecInt clause = new VecInt();
......
......@@ -86,7 +86,8 @@ public class GenericOptLauncher extends AbstractLauncher {
"kind of problem: minone, maxsat, etc.");
options.addOption("i", "incomplete", false,
"incomplete mode for maxsat");
options.addOption("I", "inner mode", false, "optimize using inner mode");
options.addOption("I", "inner mode", false,
"optimize using inner mode");
options.addOption("c", "clean databases", false,
"clean up the database at root level");
options.addOption("k", "keep Hot", false,
......@@ -99,8 +100,11 @@ public class GenericOptLauncher extends AbstractLauncher {
"Do not display a solution line (useful if the solution is large)");
options.addOption("l", "lower bounding", false,
"search solution by lower bounding instead of by upper bounding");
options.addOption("hs", "MaxHS Like", false,
"search solution using a MaxHS like approach");
options.addOption("m", "mystery", false, "mystery option");
options.addOption("B", "External&Internal", false, "External&Internal optimization");
options.addOption("B", "External&Internal", false,
"External&Internal optimization");
return options;
}
......@@ -127,7 +131,6 @@ public class GenericOptLauncher extends AbstractLauncher {
return reader;
}
@Override
protected String getInstanceName(String[] args) {
return args[args.length - 1];
......@@ -179,6 +182,9 @@ public class GenericOptLauncher extends AbstractLauncher {
if (cmd.hasOption("l")) {
asolver = new ConstraintRelaxingPseudoOptDecorator(
this.wmsd);
} else if (cmd.hasOption("hs")) {
asolver = org.sat4j.maxsat.SolverFactory.newMaxHSLike();
setLauncherMode(ILauncherMode.DECISION);
} else if (cmd.hasOption("I")){
this.wmsd.setSearchListener(new SearchOptimizerListener(ILauncherMode.DECISION));
setLauncherMode(ILauncherMode.DECISION);
......@@ -231,8 +237,7 @@ public class GenericOptLauncher extends AbstractLauncher {
@Override
protected IProblem readProblem(String problemname)
throws ParseFormatException, IOException,
ContradictionException {
throws ParseFormatException, IOException, ContradictionException {
super.readProblem(problemname);
return solver;
}
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004, 2012 Artois University and CNRS
*
* 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++.
*
* Contributors:
* CRIL - initial API and implementation
*******************************************************************************/
package org.sat4j.maxsat;
import java.math.BigInteger;
......@@ -19,6 +48,14 @@ import org.sat4j.specs.IteratorInt;
import org.sat4j.specs.TimeoutException;
import org.sat4j.tools.SolverDecorator;
/**
* Simple MAXHS like maxsat solver. The unsat core computation is performed by
* a SAT solver, and the minimal hitting set computation is handled by a PBO solver
* (unlike the original MAXSAT which relies on a MILP solver like CPLEX).
*
* @author leberre
* @since 2.3.6
*/
public class MaxHSLikeSolver extends SolverDecorator<ISolver>
implements WeightedPartialMaxsat {
......@@ -183,6 +220,9 @@ public class MaxHSLikeSolver extends SolverDecorator<ISolver>
public boolean isSatisfiable() throws TimeoutException {
IVecInt hs = new VecInt(hsfinder.findModel());
while (!decorated().isSatisfiable(hs)) {
if (isVerbose()) {
System.out.print(".");
}
IVecInt core = decorated().unsatExplanation();
IVecInt clause = new VecInt(core.size());
for (IteratorInt it = core.iterator(); it.hasNext();) {
......@@ -208,4 +248,14 @@ public class MaxHSLikeSolver extends SolverDecorator<ISolver>
return hsfinder.getObjectiveFunction().calculateDegree(hsfinder);
}
@Override
public String toString(String prefix) {
return prefix+"MaxHS like optimization"+System.lineSeparator()+super.toString(prefix);
}
@Override
public String toString() {
return "MaxHS like optimization "+super.toString();
}
}
......@@ -38,6 +38,7 @@ import org.sat4j.minisat.learning.MiniSATLearning;
import org.sat4j.minisat.orders.VarOrderHeap;
import org.sat4j.minisat.restarts.MiniSATRestarts;
import org.sat4j.pb.IPBSolver;
import org.sat4j.specs.ISolver;
public class SolverFactory extends ASolverFactory<IPBSolver> {
......@@ -105,4 +106,8 @@ public class SolverFactory extends ASolverFactory<IPBSolver> {
public static IPBSolver newLight() {
return org.sat4j.pb.SolverFactory.newLight();
}
public static ISolver newMaxHSLike() {
return new MaxHSLikeSolver(newDefault(), newDefault());
}
}
......@@ -289,7 +289,7 @@ Sat4j is a full featured boolean reasoning library designed to bring state-of-th
<plugin>
<groupId>org.jacoco</groupId>
<artifactId>jacoco-maven-plugin</artifactId>
<version>0.7.9</version>
<version>0.8.2</version>
<executions>
<execution>
<phase>process-test-classes</phase>
......
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