Commit d2430427 authored by Daniel Le Berre's avatar Daniel Le Berre

Merge branch 'master' into JAN_FIX

parents d96ce19c a824372f
Pipeline #375 passed with stage
in 30 seconds
......@@ -60,8 +60,12 @@ public class NaturalStaticOrder implements IOrder {
@Override
public int select() {
while (!voc.isUnassigned(LiteralsUtils.posLit(index))) {
while (!voc.isUnassigned(LiteralsUtils.posLit(index))
|| !voc.belongsToPool(index)) {
index++;
if (index > voc.nVars()) {
return ILits.UNDEFINED;
}
}
return phaseSelectionStrategy.select(index);
}
......
......@@ -66,6 +66,7 @@ public class ConflictMap extends MapPb implements IConflict {
* to store the slack of the current resolvant
*/
protected BigInteger currentSlack;
protected BigInteger sumAllCoefs;
protected int currentLevel;
int backtrackLevel = NOTCOMPUTED;
......@@ -172,6 +173,7 @@ public class ConflictMap extends MapPb implements IConflict {
private void initStructures() {
this.currentSlack = BigInteger.ZERO;
this.sumAllCoefs = BigInteger.ZERO;
this.byLevel = new VecInt[levelToIndex(this.currentLevel) + 1];
int ilit, litLevel, index;
BigInteger tmp;
......@@ -180,6 +182,7 @@ public class ConflictMap extends MapPb implements IConflict {
litLevel = this.voc.getLevel(ilit);
// eventually add to slack
tmp = this.weightedLits.getCoef(i);
this.sumAllCoefs = this.sumAllCoefs.add(tmp);
if (tmp.signum() > 0 && (!this.voc.isFalsified(ilit)
|| litLevel == this.currentLevel)) {
this.currentSlack = this.currentSlack.add(tmp);
......@@ -326,7 +329,7 @@ public class ConflictMap extends MapPb implements IConflict {
System.out.println("skip");
System.out.println("coef: " + this.weightedLits.get(nLitImplied) + ", slack: " + slackConflict());
if (this.weightedLits.get(nLitImplied).negate()
.compareTo(slackConflict() /*currentSlack.subtract(degree) */) > 0) {
.compareTo(slackConflict()) > 0) {
if (this.endingSkipping)
stats.numberOfEndingSkipping++;
else
......@@ -403,6 +406,17 @@ public class ConflictMap extends MapPb implements IConflict {
// updating of the degree of the conflict
degreeCons = degreeCons.multiply(this.coefMultCons);
this.degree = this.degree.multiply(this.coefMult);
// Updating the stats about the reduction.
for (int i = 0; i < cpb.size(); i++) {
if (coefsCons[i].signum() != 0) {
if (this.voc.isUnassigned(cpb.get(i))) {
this.stats.numberOfRemainingUnassigned++;
} else {
this.stats.numberOfRemainingAssigned++;
}
}
}
}
// coefficients of the conflict must be multiplied by coefMult
......@@ -412,9 +426,7 @@ public class ConflictMap extends MapPb implements IConflict {
.multiply(this.coefMult));
}
}
}
assert slackConflict().signum() < 0;
//assert slackConflict().equals(currentSlack.subtract(degree));
......@@ -501,7 +513,7 @@ public class ConflictMap extends MapPb implements IConflict {
assert slackIndex.signum() <= 0;
// estimate of the slack after the cutting plane
slackResolve = slackThis.add(slackIndex);
} while (slackResolve.signum() >= 0);
} while ((slackResolve.signum() >= 0) || this.isUnsat());
assert this.coefMult.multiply(this.weightedLits.get(litImplied ^ 1))
.equals(this.coefMultCons.multiply(reducedCoefs[ind]));
return reducedDegree;
......@@ -575,8 +587,9 @@ public class ConflictMap extends MapPb implements IConflict {
}
/**
* tests if the conflict is assertive (allows to imply a literal) at a
* particular decision level
* change the currentLevel of the conflict to a new decision level and tests
* if the conflict is assertive (allows to imply a literal) at this new
* decision level
*
* @param dl
* the decision level
......@@ -593,6 +606,15 @@ public class ConflictMap extends MapPb implements IConflict {
return isImplyingLiteral(slack);
}
/**
* tests if the conflict is unsatisfiable
*
* @return true if the conflict is unsatisfiable
*/
public boolean isUnsat() {
return this.sumAllCoefs.subtract(this.degree).signum() < 0;
}
// given the slack already computed, tests if a literal could be implied at
// a particular level
// uses the byLevel data structure to parse each literal by decision level
......@@ -909,6 +931,7 @@ public class ConflictMap extends MapPb implements IConflict {
|| this.voc.getLevel(lit) == this.currentLevel) {
this.currentSlack = this.currentSlack.add(incCoef);
}
this.sumAllCoefs = this.sumAllCoefs.add(incCoef);
assert this.byLevel[levelToIndex(this.voc.getLevel(lit))].contains(lit);
super.increaseCoef(lit, incCoef);
}
......@@ -919,6 +942,7 @@ public class ConflictMap extends MapPb implements IConflict {
|| this.voc.getLevel(lit) == this.currentLevel) {
this.currentSlack = this.currentSlack.subtract(decCoef);
}
this.sumAllCoefs = this.sumAllCoefs.subtract(decCoef);
assert this.byLevel[levelToIndex(this.voc.getLevel(lit))].contains(lit);
super.decreaseCoef(lit, decCoef);
}
......@@ -933,6 +957,11 @@ public class ConflictMap extends MapPb implements IConflict {
}
this.currentSlack = this.currentSlack.add(newValue);
}
if (this.weightedLits.containsKey(lit)) {
this.sumAllCoefs = this.sumAllCoefs
.subtract(this.weightedLits.get(lit));
}
this.sumAllCoefs = this.sumAllCoefs.add(newValue);
int indLitLevel = levelToIndex(litLevel);
if (!this.weightedLits.containsKey(lit)) {
if (this.byLevel[indLitLevel] == null) {
......@@ -957,6 +986,12 @@ public class ConflictMap extends MapPb implements IConflict {
}
this.currentSlack = this.currentSlack.add(newValue);
}
if (this.weightedLits.containsKey(lit)) {
this.sumAllCoefs = this.sumAllCoefs
.subtract(this.weightedLits.get(lit));
}
this.sumAllCoefs = this.sumAllCoefs.add(newValue);
int indLitLevel = levelToIndex(litLevel);
assert this.weightedLits.containsKey(lit);
assert this.byLevel[indLitLevel] != null;
......@@ -971,6 +1006,8 @@ public class ConflictMap extends MapPb implements IConflict {
this.currentSlack = this.currentSlack
.subtract(this.weightedLits.get(lit));
}
this.sumAllCoefs = this.sumAllCoefs
.subtract(this.weightedLits.get(lit));
int indLitLevel = levelToIndex(litLevel);
assert indLitLevel < this.byLevel.length;
assert this.byLevel[indLitLevel] != null;
......
......@@ -35,15 +35,12 @@ import org.sat4j.pb.core.PBSolverStats;
public class ConflictMapRounding extends ConflictMap {
private final PBSolverStats stats;
/**
* @param cpb
* @param level
*/
public ConflictMapRounding(PBConstr cpb, int level, PBSolverStats stats) {
super(cpb, level);
this.stats = stats;
}
/**
......@@ -54,17 +51,37 @@ public class ConflictMapRounding extends ConflictMap {
public ConflictMapRounding(PBConstr cpb, int level, boolean noRemove,
PBSolverStats stats) {
super(cpb, level, noRemove);
this.stats = stats;
}
public static IConflict createConflict(PBConstr cpb, int level,
PBSolverStats stats) {
return new ConflictMapRounding(cpb, level, stats);
public ConflictMapRounding(PBConstr cpb, int level, boolean noRemove,
boolean skip, IPostProcess postProcessing,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) {
super(cpb, level, noRemove, skip, postProcessing, weakeningStrategy,
stats);
}
public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, PBSolverStats stats) {
return new ConflictMapRounding(cpb, level, noRemove, stats);
boolean noRemove, boolean skip, IPostProcess postProcessing,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) {
return new ConflictMapRounding(cpb, level, noRemove, skip,
postProcessing, weakeningStrategy, stats);
}
public static IConflictFactory factory() {
return new IConflictFactory() {
@Override
public IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postprocess,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) {
return ConflictMapRounding.createConflict(cpb, level, noRemove,
skip, postprocess, weakeningStrategy, stats);
}
@Override
public String toString() {
return "Always round the coefficient of the propagating literal to 1 during conflict analysis.";
}
};
}
static BigInteger ceildiv(BigInteger p, BigInteger q) {
......@@ -89,7 +106,7 @@ public class ConflictMapRounding extends ConflictMap {
boolean easyRounding = true;
for (int k = 0; k < n; k++) {
if (!sprime.equals(BigInteger.ZERO) && !voc.isFalsified(xyz.get(k))
&& xyz.get(k) != x && !abc[k].equals(BigInteger.ZERO)) {
&& !abc[k].mod(a).equals(BigInteger.ZERO)) {
// incremental computation of the slack proposed by Jakob
bigt = bigt.subtract(abc[k]);
tnewprime = ceildiv(bigt, a);
......
......@@ -54,6 +54,8 @@ public interface IConflict extends IDataStructurePB {
boolean isAssertive(int dl);
boolean isUnsat();
/**
* Reduction d'une contrainte On supprime un litteral non assigne
* prioritairement, vrai sinon. En aucun cas on ne supprime litImplied.
......
......@@ -88,7 +88,8 @@ public interface IWeakeningStrategy {
int size = wpb.size();
for (int ind = 0; ind < size && lit == -1; ind++) {
if (coefsBis[ind].signum() != 0
&& !voc.isFalsified(wpb.get(ind))) {
&& !voc.isFalsified(wpb.get(ind))
&& ind != indLitImplied) {
assert coefsBis[ind].compareTo(degreeBis) < 0;
lit = ind;
}
......
......@@ -135,7 +135,7 @@ public class PBSolverCP extends PBSolver {
int currentLevel = this.voc.getLevel(litImplied);
IConflict confl = chooseConflict((PBConstr) myconfl, currentLevel);
assert confl.slackConflict().signum() < 0;
while (!confl.isAssertive(currentLevel)) {
while (!confl.isUnsat() && !confl.isAssertive(currentLevel)) {
if (!this.undertimeout) {
throw new TimeoutException();
}
......@@ -149,7 +149,6 @@ public class PBSolverCP extends PBSolver {
break;
}
undoOne();
// assert decisionLevel() >= 0;
if (decisionLevel() == 0) {
break;
}
......@@ -166,7 +165,7 @@ public class PBSolverCP extends PBSolver {
assert litImplied > 1;
}
assert confl.isAssertive(currentLevel) || this.trail.size() == 1
|| decisionLevel() == 0;
|| decisionLevel() == 0 || confl.isUnsat();
assert currentLevel == decisionLevel();
confl.undoOne(this.trail.last());
......@@ -175,9 +174,9 @@ public class PBSolverCP extends PBSolver {
updateNumberOfReducedLearnedConstraints(confl);
// necessary informations to build a PB-constraint
// are kept from the conflict
if (confl.size() == 0
|| (decisionLevel() == 0 || this.trail.size() == 0)
&& confl.slackConflict().signum() < 0) {
if (confl.isUnsat() || confl.size() == 0 || decisionLevel() == 0
|| (this.trail.size() == 0
&& confl.slackConflict().signum() < 0)) {
results.setReason(null);
results.setBacktrackLevel(-1);
return;
......@@ -191,14 +190,9 @@ public class PBSolverCP extends PBSolver {
// the conflict give the highest decision level for the backtrack
// (which is less than current level)
// assert confl.isAssertive(currentLevel);
if (decisionLevel() == 0 || (this.trail.size() == 0
&& confl.getBacktrackLevel(currentLevel) > 0)) {
results.setBacktrackLevel(-1);
results.setReason(null);
} else {
results.setBacktrackLevel(confl.getBacktrackLevel(currentLevel));
}
int backtrackLevel = confl.getBacktrackLevel(currentLevel);
results.setBacktrackLevel(backtrackLevel);
// }
}
protected IConflict chooseConflict(PBConstr myconfl, int level) {
......@@ -212,8 +206,8 @@ public class PBSolverCP extends PBSolver {
+ this.getClass().getName() + ")\n"
+ (this.noRemove ? ""
: prefix + " - Removing satisfied literals at a higher level before CP \n")
+ (this.skipAllow ? prefix
+ " - Skipping as much as possible cutting planes during analysis conflict- Jan Elffers's algorithm \n"
+ (this.skipAllow
? prefix + " - Skipping as much as possible cutting planes during analysis conflict- Jan Elffers's algorithm \n"
: "")
+ prefix + " - " + postprocess + "\n" + prefix + " - "
+ conflictFactory + "\n" + prefix + " - " + weakeningStrategy
......
......@@ -49,7 +49,8 @@ public class PBSolverClause extends PBSolverCP {
@Override
protected IConflict chooseConflict(PBConstr myconfl, int level) {
return ConflictMapClause.createConflict(myconfl, level, isNoRemove());
return ConflictMapClause.createConflict(myconfl, level, isNoRemove(),
isSkipAllow(), stats);
}
@Override
......
......@@ -64,6 +64,10 @@ public class PBSolverStats extends SolverStats {
public long numberOfDerivationSteps;
public long numberOfRemainingUnassigned;
public long numberOfRemainingAssigned;
@Override
public void reset() {
super.reset();
......@@ -78,6 +82,8 @@ public class PBSolverStats extends SolverStats {
this.numberOfEndingSkipping = 0;
this.numberOfInternalSkipping = 0;
this.numberOfDerivationSteps = 0;
this.numberOfRemainingUnassigned = 0;
this.numberOfRemainingAssigned = 0;
}
@Override
......@@ -116,6 +122,10 @@ public class PBSolverStats extends SolverStats {
out.println(prefix + "number of skipped derivation steps \t: "
+ (this.numberOfInternalSkipping
+ this.numberOfEndingSkipping));
out.println(prefix + "number of remaining unassigned \t: "
+ this.numberOfRemainingUnassigned);
out.println(prefix + "number of remaining assigned \t: "
+ this.numberOfRemainingAssigned);
}
}
* #variable= 6 #constraint= 3
*
explain: x1 x2 x3 x4 x5 ;
* P 1.0.0 requires either PP 1.0.0
-1 x2 +1 x1 >= 0;
* 1223597333557 0.0.0.1223597333557 requires either P 1.0.0
......
......@@ -25,6 +25,7 @@ import org.sat4j.pb.constraints.pb.ConflictMapReduceByGCD;
import org.sat4j.pb.constraints.pb.ConflictMapReduceByPowersOf2;
import org.sat4j.pb.constraints.pb.ConflictMapReduceToCard;
import org.sat4j.pb.constraints.pb.ConflictMapReduceToClause;
import org.sat4j.pb.constraints.pb.ConflictMapRounding;
import org.sat4j.pb.constraints.pb.IWeakeningStrategy;
import org.sat4j.pb.constraints.pb.PostProcessToCard;
import org.sat4j.pb.constraints.pb.PostProcessToClause;
......@@ -47,6 +48,7 @@ import org.sat4j.tools.DotSearchTracing;
*/
public class KTHLauncher {
public static Options createCLIOptions() {
Options options = new Options();
options.addOption("cl", "coeflim", true,
......@@ -234,6 +236,9 @@ public class KTHLauncher {
ConflictMapReduceToCard.factory());
break;
case "divide-v1":
cpsolver.setConflictFactory(
ConflictMapRounding.factory());
break;
case "divide-unless-equal":
case "divide-unless-divisor":
case "round-to-gcd":
......@@ -305,7 +310,17 @@ public class KTHLauncher {
PBSolverHandle handle = new PBSolverHandle(
new PseudoOptDecorator(pbsolver));
OPBReader2012 reader = new OPBReader2012(handle);
OptToPBSATAdapter optimizer = new OptToPBSATAdapter(handle);
final OptToPBSATAdapter optimizer = new OptToPBSATAdapter(handle);
final Thread shutdownHook = new Thread() {
@Override
public void run() {
// stop the solver before displaying solutions
optimizer.expireTimeout();
optimizer.printStat(System.out, "c ");
}
};
Runtime.getRuntime().addShutdownHook(shutdownHook);
try {
reader.parseInstance(filename);
if (line.hasOption("dot-output")) {
......@@ -328,7 +343,6 @@ public class KTHLauncher {
} else {
System.out.println("s UNSATISFIABLE");
}
optimizer.printStat(System.out, "c ");
} catch (TimeoutException e) {
System.out.println("s UNKNOWN");
} catch (ParseFormatException e) {
......
......@@ -189,21 +189,13 @@ Sat4j is a full featured boolean reasoning library designed to bring state-of-th
</plugin>
<plugin>
<artifactId>maven-compiler-plugin</artifactId>
<version>3.6.0</version>
<version>3.6.2</version>
<configuration>
<source>${javaSource}</source>
<target>${javaTarget}</target>
<testSource>${testSource}</testSource>
<testTarget>${testTarget}</testTarget>
<compilerId>jdt</compilerId>
</configuration>
<dependencies>
<dependency>
<groupId>org.eclipse.tycho</groupId>
<artifactId>tycho-compiler-jdt</artifactId>
<version>0.23.0</version>
</dependency>
</dependencies>
</plugin>
<plugin>
<groupId>org.codehaus.mojo</groupId>
......
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