Skip to content

Commit

Permalink
MaxSAT cleanup (dont store nbSoft and nbHard redundantly)
Browse files Browse the repository at this point in the history
  • Loading branch information
@SHildebrandt
SHildebrandt committed Aug 29, 2024
1 parent 757fe5f commit 6f6ce60
Show file tree
Hide file tree
Showing 9 changed files with 109 additions and 134 deletions.
28 changes: 14 additions & 14 deletions src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/IncWBO.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -118,7 +118,7 @@ protected void incrementalBuildWeightSolver(final MaxSATConfig.WeightStrategy st
for (int i = 0; i < nVars(); i++) {
newSATVariable(solver);
}
for (int i = 0; i < nHard(); i++) {
for (int i = 0; i < hardClauses.size(); i++) {
solver.addClause(hardClauses.get(i).clause(), null);
}
if (symmetryStrategy) {
Expand All @@ -128,7 +128,7 @@ protected void incrementalBuildWeightSolver(final MaxSATConfig.WeightStrategy st
}
LNGIntVector clause;
nbCurrentSoft = 0;
for (int i = 0; i < nSoft(); i++) {
for (int i = 0; i < softClauses.size(); i++) {
if (softClauses.get(i).weight() >= currentWeight && softClauses.get(i).weight() != 0) {
nbCurrentSoft++;
clause = new LNGIntVector(softClauses.get(i).clause());
Expand Down Expand Up @@ -157,8 +157,8 @@ protected void relaxCore(final LNGIntVector conflict, final int weightCore) {
addSoftClause(weightCore, clause, vars);
final int l = newLiteral(false);
newSATVariable(solver);
softClauses.get(nSoft() - 1).setAssumptionVar(l);
coreMapping.put(l, nSoft() - 1);
softClauses.get(softClauses.size() - 1).setAssumptionVar(l);
coreMapping.put(l, softClauses.size() - 1);
incSoft.set(indexSoft, true);
incSoft.push(false);
for (int j = 0; j < vars.size(); j++) {
Expand All @@ -174,7 +174,7 @@ protected void relaxCore(final LNGIntVector conflict, final int weightCore) {
softMapping.get(indexSoft).clear();
relaxationMapping.push(new LNGIntVector(relaxationMapping.get(indexSoft)));
relaxationMapping.get(indexSoft).clear();
symmetryLog(nSoft() - 1);
symmetryLog(softClauses.size() - 1);
}
} else {
assert softClauses.get(indexSoft).weight() - weightCore > 0;
Expand All @@ -191,8 +191,8 @@ protected void relaxCore(final LNGIntVector conflict, final int weightCore) {
incSoft.set(indexSoft, true);
int l = newLiteral(false);
newSATVariable(solver);
softClauses.get(nSoft() - 1).setAssumptionVar(l);
coreMapping.put(l, nSoft() - 1);
softClauses.get(softClauses.size() - 1).setAssumptionVar(l);
coreMapping.put(l, softClauses.size() - 1);
incSoft.push(false);
for (int j = 0; j < vars.size(); j++) {
clause.push(vars.get(j));
Expand All @@ -210,8 +210,8 @@ protected void relaxCore(final LNGIntVector conflict, final int weightCore) {
addSoftClause(weightCore, clause, vars);
l = newLiteral(false);
newSATVariable(solver);
softClauses.get(nSoft() - 1).setAssumptionVar(l);
coreMapping.put(l, nSoft() - 1);
softClauses.get(softClauses.size() - 1).setAssumptionVar(l);
coreMapping.put(l, softClauses.size() - 1);
incSoft.push(false);
for (int j = 0; j < vars.size(); j++) {
clause.push(vars.get(j));
Expand All @@ -224,7 +224,7 @@ protected void relaxCore(final LNGIntVector conflict, final int weightCore) {
if (symmetryStrategy) {
softMapping.push(new LNGIntVector());
relaxationMapping.push(new LNGIntVector());
symmetryLog(nSoft() - 1);
symmetryLog(softClauses.size() - 1);
}
}
}
Expand Down Expand Up @@ -319,7 +319,7 @@ protected LNGResult<InternalMaxSATResult> weightSearch(final ComputationHandler
initAssumptions();
updateCurrentWeight(weightStrategy);
incrementalBuildWeightSolver(weightStrategy);
incSoft.growTo(nSoft(), false);
incSoft.growTo(softClauses.size(), false);
while (true) {
assumptions.clear();
for (int i = 0; i < incSoft.size(); i++) {
Expand All @@ -346,7 +346,7 @@ protected LNGResult<InternalMaxSATResult> weightSearch(final ComputationHandler
incrementalBuildWeightSolver(weightStrategy);
} else {
nbSatisfiable++;
if (nbCurrentSoft == nSoft()) {
if (nbCurrentSoft == softClauses.size()) {
assert incComputeCostModel(solver.model()) == lbCost;
if (lbCost == ubCost && verbosity != MaxSATConfig.Verbosity.NONE) {
output.println("c LB = UB");
Expand Down Expand Up @@ -389,7 +389,7 @@ protected LNGResult<InternalMaxSATResult> weightSearch(final ComputationHandler
protected int incComputeCostModel(final LNGBooleanVector currentModel) {
assert currentModel.size() != 0;
int currentCost = 0;
for (int i = 0; i < nSoft(); i++) {
for (int i = 0; i < softClauses.size(); i++) {
boolean unsatisfied = true;
for (int j = 0; j < softClauses.get(i).clause().size(); j++) {
if (incSoft.get(i)) {
Expand Down Expand Up @@ -422,7 +422,7 @@ protected LNGResult<InternalMaxSATResult> normalSearch(final ComputationHandler
}
initAssumptions();
solver = rebuildSolver();
incSoft.growTo(nSoft(), false);
incSoft.growTo(softClauses.size(), false);
while (true) {
assumptions.clear();
for (int i = 0; i < incSoft.size(); i++) {
Expand Down
6 changes: 3 additions & 3 deletions src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/LinearSU.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -250,10 +250,10 @@ protected LNGCoreSolver rebuildSolver(final int minWeight) {
for (int i = 0; i < nVars(); i++) {
newSATVariable(s);
}
for (int i = 0; i < nHard(); i++) {
for (int i = 0; i < hardClauses.size(); i++) {
s.addClause(hardClauses.get(i).clause(), null);
}
for (int i = 0; i < nSoft(); i++) {
for (int i = 0; i < softClauses.size(); i++) {
if (softClauses.get(i).weight() < minWeight) {
continue;
}
Expand All @@ -279,7 +279,7 @@ protected LNGCoreSolver rebuildBMO(final LNGVector<LNGIntVector> functions, fina
final LNGCoreSolver s = rebuildSolver(currentWeight);
objFunction.clear();
coeffs.clear();
for (int i = 0; i < nSoft(); i++) {
for (int i = 0; i < softClauses.size(); i++) {
if (softClauses.get(i).weight() == currentWeight) {
objFunction.push(softClauses.get(i).relaxationVars().get(0));
coeffs.push(softClauses.get(i).weight());
Expand Down
6 changes: 3 additions & 3 deletions src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/LinearUS.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -212,11 +212,11 @@ protected LNGCoreSolver rebuildSolver() {
for (int i = 0; i < nVars(); i++) {
newSATVariable(s);
}
for (int i = 0; i < nHard(); i++) {
for (int i = 0; i < hardClauses.size(); i++) {
s.addClause(hardClauses.get(i).clause(), null);
}
LNGIntVector clause;
for (int i = 0; i < nSoft(); i++) {
for (int i = 0; i < softClauses.size(); i++) {
clause = new LNGIntVector(softClauses.get(i).clause());
for (int j = 0; j < softClauses.get(i).relaxationVars().size(); j++) {
clause.push(softClauses.get(i).relaxationVars().get(j));
Expand All @@ -227,7 +227,7 @@ protected LNGCoreSolver rebuildSolver() {
}

protected void initRelaxation(final LNGIntVector objFunction) {
for (int i = 0; i < nbSoft; i++) {
for (int i = 0; i < softClauses.size(); i++) {
final int l = newLiteral(false);
softClauses.get(i).relaxationVars().push(l);
softClauses.get(i).setAssumptionVar(l);
Expand Down
18 changes: 9 additions & 9 deletions src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MSU3.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,8 +101,8 @@ protected LNGResult<InternalMaxSATResult> none(final ComputationHandler handler)
final LNGIntVector assumptions = new LNGIntVector();
final LNGIntVector currentObjFunction = new LNGIntVector();
encoder.setIncremental(IncrementalStrategy.NONE);
final LNGBooleanVector activeSoft = new LNGBooleanVector(nSoft(), false);
for (int i = 0; i < nSoft(); i++) {
final LNGBooleanVector activeSoft = new LNGBooleanVector(softClauses.size(), false);
for (int i = 0; i < softClauses.size(); i++) {
coreMapping.put(softClauses.get(i).assumptionVar(), i);
}
while (true) {
Expand Down Expand Up @@ -155,7 +155,7 @@ protected LNGResult<InternalMaxSATResult> none(final ComputationHandler handler)
}
currentObjFunction.clear();
assumptions.clear();
for (int i = 0; i < nSoft(); i++) {
for (int i = 0; i < softClauses.size(); i++) {
if (activeSoft.get(i)) {
currentObjFunction.push(softClauses.get(i).relaxationVars().get(0));
} else {
Expand Down Expand Up @@ -186,8 +186,8 @@ protected LNGResult<InternalMaxSATResult> iterative(final ComputationHandler han
final LNGIntVector currentObjFunction = new LNGIntVector();
final LNGIntVector encodingAssumptions = new LNGIntVector();
encoder.setIncremental(IncrementalStrategy.ITERATIVE);
final LNGBooleanVector activeSoft = new LNGBooleanVector(nSoft(), false);
for (int i = 0; i < nSoft(); i++) {
final LNGBooleanVector activeSoft = new LNGBooleanVector(softClauses.size(), false);
for (int i = 0; i < softClauses.size(); i++) {
coreMapping.put(softClauses.get(i).assumptionVar(), i);
}
while (true) {
Expand Down Expand Up @@ -249,7 +249,7 @@ protected LNGResult<InternalMaxSATResult> iterative(final ComputationHandler han
}
currentObjFunction.clear();
assumptions.clear();
for (int i = 0; i < nSoft(); i++) {
for (int i = 0; i < softClauses.size(); i++) {
if (activeSoft.get(i)) {
currentObjFunction.push(softClauses.get(i).relaxationVars().get(0));
} else {
Expand Down Expand Up @@ -282,11 +282,11 @@ protected LNGCoreSolver rebuildSolver() {
for (int i = 0; i < nVars(); i++) {
newSATVariable(s);
}
for (int i = 0; i < nHard(); i++) {
for (int i = 0; i < hardClauses.size(); i++) {
s.addClause(hardClauses.get(i).clause(), null);
}
LNGIntVector clause;
for (int i = 0; i < nSoft(); i++) {
for (int i = 0; i < softClauses.size(); i++) {
clause = new LNGIntVector(softClauses.get(i).clause());
for (int j = 0; j < softClauses.get(i).relaxationVars().size(); j++) {
clause.push(softClauses.get(i).relaxationVars().get(j));
Expand All @@ -297,7 +297,7 @@ protected LNGCoreSolver rebuildSolver() {
}

protected void initRelaxation(final LNGIntVector objFunction) {
for (int i = 0; i < nbSoft; i++) {
for (int i = 0; i < softClauses.size(); i++) {
final int l = newLiteral(false);
softClauses.get(i).relaxationVars().push(l);
softClauses.get(i).setAssumptionVar(l);
Expand Down
53 changes: 14 additions & 39 deletions src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MaxSAT.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,8 +78,6 @@ public enum ProblemType {
int hardWeight;
ProblemType problemType;
int nbVars;
int nbSoft;
int nbHard;
int nbInitialVariables;
int nbCores;
int nbSymmetryClauses;
Expand All @@ -105,8 +103,6 @@ protected MaxSAT(final FormulaFactory f, final MaxSATConfig config) {
hardWeight = Integer.MAX_VALUE;
problemType = ProblemType.UNWEIGHTED;
nbVars = 0;
nbSoft = 0;
nbHard = 0;
nbInitialVariables = 0;
currentWeight = 1;
model = new LNGBooleanVector();
Expand Down Expand Up @@ -171,17 +167,16 @@ public final LNGResult<InternalMaxSATResult> search(final ComputationHandler han
}

protected StateBeforeSolving saveStateBeforeSolving() {
assert nbSoft == softClauses.size();
final int[] softWeights = new int[nbSoft];
for (int i = 0; i < nbSoft; i++) {
final int[] softWeights = new int[softClauses.size()];
for (int i = 0; i < softClauses.size(); i++) {
softWeights[i] = softClauses.get(i).weight();
}
return new StateBeforeSolving(nbVars, nbSoft, nbHard, ubCost, currentWeight, softWeights);
return new StateBeforeSolving(nbVars, hardClauses.size(), softClauses.size(), ubCost, currentWeight, softWeights);
}

protected void loadStateBeforeSolving(final StateBeforeSolving stateBeforeSolving) {
softClauses.shrinkTo(stateBeforeSolving.nbSoft);
hardClauses.shrinkTo(stateBeforeSolving.nbHard);
softClauses.shrinkTo(stateBeforeSolving.nbSoft);
orderWeights.clear();
for (int i = stateBeforeSolving.nbVars; i < nbVars; i++) {
final Variable var = index2var.remove(i);
Expand All @@ -190,8 +185,6 @@ protected void loadStateBeforeSolving(final StateBeforeSolving stateBeforeSolvin
}
}
nbVars = stateBeforeSolving.nbVars;
nbSoft = stateBeforeSolving.nbSoft;
nbHard = stateBeforeSolving.nbHard;
nbCores = 0;
nbSymmetryClauses = 0;
sumSizeCores = 0;
Expand Down Expand Up @@ -223,26 +216,12 @@ public int nVars() {
}

/**
* Returns the number of soft clauses in the working MaxSAT formula.
* @return the number of soft clauses in the working MaxSAT formula
*/
public int nSoft() {
return nbSoft;
}

/**
* Returns the number of hard clauses in the working MaxSAT formula.
* @return the number of hard clauses in the working MaxSAT formula
* Returns a new variable index and increases the internal number of
* variables.
* @return a new variable index
*/
public int nHard() {
return nbHard;
}

/**
* Increases the number of variables in the working MaxSAT formula.
*/
public void newVar() {
nbVars++;
public int newVar() {
return nbVars++;
}

/**
Expand All @@ -251,7 +230,6 @@ public void newVar() {
*/
public void addHardClause(final LNGIntVector lits) {
hardClauses.push(new LNGHardClause(lits));
nbHard++;
}

/**
Expand All @@ -272,7 +250,6 @@ public void addSoftClause(final int weight, final LNGIntVector lits) {
*/
protected void addSoftClause(final int weight, final LNGIntVector lits, final LNGIntVector vars) {
softClauses.push(new LNGSoftClause(lits, weight, LIT_UNDEF, vars));
nbSoft++;
}

/**
Expand Down Expand Up @@ -328,9 +305,7 @@ public int literal(final Literal lit) {
* @return the new literal
*/
public int newLiteral(final boolean sign) {
final int p = LNGCoreSolver.mkLit(nVars(), sign);
newVar();
return p;
return LNGCoreSolver.mkLit(newVar(), sign);
}

/**
Expand Down Expand Up @@ -411,7 +386,7 @@ public void saveModel(final LNGBooleanVector currentModel) {
public int computeCostModel(final LNGBooleanVector currentModel, final int weight) {
assert currentModel.size() != 0;
int currentCost = 0;
for (int i = 0; i < nSoft(); i++) {
for (int i = 0; i < softClauses.size(); i++) {
boolean unsatisfied = true;
for (int j = 0; j < softClauses.get(i).clause().size(); j++) {
if (weight != Integer.MAX_VALUE && softClauses.get(i).weight() != weight) {
Expand Down Expand Up @@ -445,7 +420,7 @@ public boolean isBMO(final boolean cache) {
boolean bmo = true;
final SortedSet<Integer> partitionWeights = new TreeSet<>();
final SortedMap<Integer, Integer> nbPartitionWeights = new TreeMap<>();
for (int i = 0; i < nSoft(); i++) {
for (int i = 0; i < softClauses.size(); i++) {
final int weight = softClauses.get(i).weight();
partitionWeights.add(weight);
nbPartitionWeights.merge(weight, 1, Integer::sum);
Expand Down Expand Up @@ -509,13 +484,13 @@ LNGEvent foundUpperBound(final int upperBound, final ComputationHandler handler)

protected static class StateBeforeSolving {
protected final int nbVars;
protected final int nbSoft;
protected final int nbHard;
protected final int nbSoft;
protected final int ubCost;
protected final int currentWeight;
protected final int[] softWeights;

protected StateBeforeSolving(final int nbVars, final int nbSoft, final int nbHard, final int ubCost, final int currentWeight, final int[] softWeights) {
protected StateBeforeSolving(final int nbVars, final int nbHard, final int nbSoft, final int ubCost, final int currentWeight, final int[] softWeights) {
this.nbVars = nbVars;
this.nbSoft = nbSoft;
this.nbHard = nbHard;
Expand Down
Loading

0 comments on commit 6f6ce60

Please sign in to comment.