Skip to content

Commit

Permalink
some refactoring
Browse files Browse the repository at this point in the history
  • Loading branch information
@SHildebrandt
SHildebrandt committed Apr 5, 2024
1 parent 944e268 commit e7bd4e8
Show file tree
Hide file tree
Showing 12 changed files with 105 additions and 176 deletions.
19 changes: 4 additions & 15 deletions src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfCoreSolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@
import com.booleworks.logicng.formulas.FormulaFactory;
import com.booleworks.logicng.formulas.Literal;
import com.booleworks.logicng.solvers.datastructures.LNGClause;
import com.booleworks.logicng.solvers.datastructures.LNGVariable;
import com.booleworks.logicng.solvers.sat.LNGCoreSolver;
import com.booleworks.logicng.solvers.sat.SATSolverConfig;

Expand Down Expand Up @@ -143,19 +142,16 @@ public boolean assertCdLiteral() {
uncheckedEnqueue(lastLearnt.get(0), null);
unitClauses.push(lastLearnt.get(0));
} else {
final LNGClause cr = new LNGClause(lastLearnt, stateId);
final LNGClause cr = new LNGClause(lastLearnt, nextStateId);
cr.setLBD(analyzeLBD);
cr.setOneWatched(false);
learnts.push(cr);
attachClause(cr);
claBumpActivity(cr);
uncheckedEnqueue(lastLearnt.get(0), cr);
}
varDecayActivity();
claDecayActivity();
if (--learntsizeAdjustCnt == 0) {
learntsizeAdjustConfl *= learntsizeAdjustInc;
learntsizeAdjustCnt = (int) learntsizeAdjustConfl;
maxLearnts *= llConfig.learntsizeInc;
}
return propagateAfterDecide();
}

Expand Down Expand Up @@ -203,15 +199,8 @@ protected void cancelUntil(final int level) {
final int l = trail.get(c);
assignment[l] = Tristate.UNDEF;
assignment[l ^ 1] = Tristate.UNDEF;
final int x = var(l);
final LNGVariable v = vars.get(x);
v.assign(Tristate.UNDEF);
v.setPolarity(sign(trail.get(c)));
insertVarOrder(x);
}
qhead = trailLim.get(level);
trail.removeElements(trail.size() - trailLim.get(level));
trailLim.removeElements(trailLim.size() - level);
super.cancelUntil(level);
}
}

Expand Down
42 changes: 5 additions & 37 deletions src/main/java/com/booleworks/logicng/solvers/datastructures/LNGBoundedLongQueue.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,11 @@ public LNGBoundedLongQueue() {
* @param size the size
*/
public void initSize(final int size) {
growTo(size);
elems.growTo(size, 0);
first = 0;
maxSize = size;
queueSize = 0;
last = 0;
}

/**
Expand Down Expand Up @@ -135,18 +139,6 @@ public boolean valid() {
return queueSize == maxSize;
}

/**
* Grows this queue to a given size.
* @param size the size
*/
private void growTo(final int size) {
elems.growTo(size, 0);
first = 0;
maxSize = size;
queueSize = 0;
last = 0;
}

/**
* Performs a fast clear of this queue (the elements are left untouched).
*/
Expand All @@ -157,30 +149,6 @@ public void fastClear() {
sumOfQueue = 0;
}

LNGLongVector getElems() {
return elems;
}

int getFirst() {
return first;
}

int getLast() {
return last;
}

long getSumOfQueue() {
return sumOfQueue;
}

int getMaxSize() {
return maxSize;
}

int getQueueSize() {
return queueSize;
}

@Override
public String toString() {
return String.format("LNGBoundedLongQueue{first=%d, last=%d, sumOfQueue=%d, maxSize=%d, queueSize=%d, elems=%s}",
Expand Down
16 changes: 8 additions & 8 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 @@ -323,16 +323,16 @@ protected MaxSATResult weightSearch() {
return MaxSATResult.UNDEF;
} else if (res == FALSE) {
nbCores++;
assert solver.conflict().size() > 0;
final int coreCost = computeCostCore(solver.conflict());
assert solver.assumptionsConflict().size() > 0;
final int coreCost = computeCostCore(solver.assumptionsConflict());
lbCost += coreCost;
if (verbosity != MaxSATConfig.Verbosity.NONE) {
output.printf("c LB : %d CS : %d W : %d%n", lbCost, solver.conflict().size(), coreCost);
output.printf("c LB : %d CS : %d W : %d%n", lbCost, solver.assumptionsConflict().size(), coreCost);
}
if (!foundLowerBound(lbCost, null)) {
return MaxSATResult.UNDEF;
}
relaxCore(solver.conflict(), coreCost);
relaxCore(solver.assumptionsConflict(), coreCost);
incrementalBuildWeightSolver(weightStrategy);
} else {
nbSatisfiable++;
Expand Down Expand Up @@ -421,11 +421,11 @@ protected MaxSATResult normalSearch() {
return MaxSATResult.UNDEF;
} else if (res == FALSE) {
nbCores++;
assert solver.conflict().size() > 0;
final int coreCost = computeCostCore(solver.conflict());
assert solver.assumptionsConflict().size() > 0;
final int coreCost = computeCostCore(solver.assumptionsConflict());
lbCost += coreCost;
if (verbosity != MaxSATConfig.Verbosity.NONE) {
output.printf("c LB : %d CS : %d W : %d%n", lbCost, solver.conflict().size(), coreCost);
output.printf("c LB : %d CS : %d W : %d%n", lbCost, solver.assumptionsConflict().size(), coreCost);
}
if (lbCost == ubCost) {
if (verbosity != MaxSATConfig.Verbosity.NONE) {
Expand All @@ -436,7 +436,7 @@ protected MaxSATResult normalSearch() {
if (!foundLowerBound(lbCost, null)) {
return MaxSATResult.UNDEF;
}
relaxCore(solver.conflict(), coreCost);
relaxCore(solver.assumptionsConflict(), coreCost);
} else {
nbSatisfiable++;
ubCost = incComputeCostModel(solver.model());
Expand Down
22 changes: 11 additions & 11 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 @@ -152,10 +152,10 @@ protected MaxSATResult none() {
} else if (!foundLowerBound(lbCost, null)) {
return MaxSATResult.UNDEF;
}
sumSizeCores += solver.conflict().size();
for (int i = 0; i < solver.conflict().size(); i++) {
assert !activeSoft.get(coreMapping.get(solver.conflict().get(i)));
activeSoft.set(coreMapping.get(solver.conflict().get(i)), true);
sumSizeCores += solver.assumptionsConflict().size();
for (int i = 0; i < solver.assumptionsConflict().size(); i++) {
assert !activeSoft.get(coreMapping.get(solver.assumptionsConflict().get(i)));
activeSoft.set(coreMapping.get(solver.assumptionsConflict().get(i)), true);
}
currentObjFunction.clear();
assumptions.clear();
Expand Down Expand Up @@ -232,19 +232,19 @@ protected MaxSATResult iterative() {
}
return MaxSATResult.OPTIMUM;
}
sumSizeCores += solver.conflict().size();
if (solver.conflict().size() == 0) {
sumSizeCores += solver.assumptionsConflict().size();
if (solver.assumptionsConflict().size() == 0) {
return MaxSATResult.UNSATISFIABLE;
}
if (!foundLowerBound(lbCost, null)) {
return MaxSATResult.UNDEF;
}
joinObjFunction.clear();
for (int i = 0; i < solver.conflict().size(); i++) {
if (coreMapping.containsKey(solver.conflict().get(i))) {
assert !activeSoft.get(coreMapping.get(solver.conflict().get(i)));
activeSoft.set(coreMapping.get(solver.conflict().get(i)), true);
joinObjFunction.push(softClauses.get(coreMapping.get(solver.conflict().get(i))).relaxationVars().get(0));
for (int i = 0; i < solver.assumptionsConflict().size(); i++) {
if (coreMapping.containsKey(solver.assumptionsConflict().get(i))) {
assert !activeSoft.get(coreMapping.get(solver.assumptionsConflict().get(i)));
activeSoft.set(coreMapping.get(solver.assumptionsConflict().get(i)), true);
joinObjFunction.push(softClauses.get(coreMapping.get(solver.assumptionsConflict().get(i))).relaxationVars().get(0));
}
}
currentObjFunction.clear();
Expand Down
32 changes: 16 additions & 16 deletions src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/OLL.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -146,16 +146,16 @@ private MaxSATResult unweighted() {
assert nbSatisfiable > 0;
return MaxSATResult.OPTIMUM;
}
sumSizeCores += solver.conflict().size();
sumSizeCores += solver.assumptionsConflict().size();
final LNGIntVector softRelax = new LNGIntVector();
final LNGIntVector cardinalityRelax = new LNGIntVector();

for (int i = 0; i < solver.conflict().size(); i++) {
final int p = solver.conflict().get(i);
for (int i = 0; i < solver.assumptionsConflict().size(); i++) {
final int p = solver.assumptionsConflict().get(i);
if (coreMapping.containsKey(p)) {
assert !activeSoft.get(coreMapping.get(p));
activeSoft.set(coreMapping.get(solver.conflict().get(i)), true);
assert p == softClauses.get(coreMapping.get(solver.conflict().get(i))).relaxationVars().get(0);
activeSoft.set(coreMapping.get(solver.assumptionsConflict().get(i)), true);
assert p == softClauses.get(coreMapping.get(solver.assumptionsConflict().get(i))).relaxationVars().get(0);
softRelax.push(p);
}

Expand All @@ -165,7 +165,7 @@ private MaxSATResult unweighted() {
cardinalityRelax.push(p);

// this is a soft cardinality -- bound must be increased
final IntTriple softId = boundMapping.get(solver.conflict().get(i));
final IntTriple softId = boundMapping.get(solver.assumptionsConflict().get(i));
// // increase the bound
assert softId.id < softCardinality.size();
assert softCardinality.get(softId.id).hasCardEncoding();
Expand Down Expand Up @@ -298,16 +298,16 @@ private MaxSATResult weighted() {
} else if (res == Tristate.FALSE) {
// reduce the weighted to the unweighted case
int minCore = Integer.MAX_VALUE;
for (int i = 0; i < solver.conflict().size(); i++) {
final int p = solver.conflict().get(i);
for (int i = 0; i < solver.assumptionsConflict().size(); i++) {
final int p = solver.assumptionsConflict().get(i);
if (coreMapping.containsKey(p)) {
assert !activeSoft.get(coreMapping.get(p));
if (softClauses.get(coreMapping.get(solver.conflict().get(i))).weight() < minCore) {
minCore = softClauses.get(coreMapping.get(solver.conflict().get(i))).weight();
if (softClauses.get(coreMapping.get(solver.assumptionsConflict().get(i))).weight() < minCore) {
minCore = softClauses.get(coreMapping.get(solver.assumptionsConflict().get(i))).weight();
}
}
if (boundMapping.containsKey(p)) {
final IntTriple softId = boundMapping.get(solver.conflict().get(i));
final IntTriple softId = boundMapping.get(solver.assumptionsConflict().get(i));
if (softId.weight < minCore) {
minCore = softId.weight;
}
Expand All @@ -322,12 +322,12 @@ private MaxSATResult weighted() {
assert nbSatisfiable > 0;
return MaxSATResult.OPTIMUM;
}
sumSizeCores += solver.conflict().size();
sumSizeCores += solver.assumptionsConflict().size();
final LNGIntVector softRelax = new LNGIntVector();
final LNGIntVector cardinalityRelax = new LNGIntVector();

for (int i = 0; i < solver.conflict().size(); i++) {
final int p = solver.conflict().get(i);
for (int i = 0; i < solver.assumptionsConflict().size(); i++) {
final int p = solver.assumptionsConflict().get(i);
if (coreMapping.containsKey(p)) {
if (softClauses.get(coreMapping.get(p)).weight() > minCore) {
assert !activeSoft.get(coreMapping.get(p));
Expand Down Expand Up @@ -366,7 +366,7 @@ private MaxSATResult weighted() {
assert softClauses.get(coreMapping.get(l)).weight() == minCore;
assert activeSoft.size() == nSoft();
} else {
assert softClauses.get(coreMapping.get(solver.conflict().get(i))).weight() == minCore;
assert softClauses.get(coreMapping.get(solver.assumptionsConflict().get(i))).weight() == minCore;
softRelax.push(p);
assert !activeSoft.get(coreMapping.get(p));
activeSoft.set(coreMapping.get(p), true);
Expand All @@ -375,7 +375,7 @@ private MaxSATResult weighted() {
if (boundMapping.containsKey(p)) {
assert cardinalityAssumptions.contains(p);
// this is a soft cardinality -- bound must be increased
final IntTriple softId = boundMapping.get(solver.conflict().get(i));
final IntTriple softId = boundMapping.get(solver.assumptionsConflict().get(i));

// increase the bound
assert softId.id < softCardinality.size();
Expand Down
16 changes: 8 additions & 8 deletions src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/WBO.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -460,16 +460,16 @@ protected MaxSATResult weightSearch() {
return MaxSATResult.UNDEF;
} else if (res == FALSE) {
nbCores++;
assert solver.conflict().size() > 0;
final int coreCost = computeCostCore(solver.conflict());
assert solver.assumptionsConflict().size() > 0;
final int coreCost = computeCostCore(solver.assumptionsConflict());
lbCost += coreCost;
if (verbosity != Verbosity.NONE) {
output.printf("c LB : %d CS : %d W : %d%n", lbCost, solver.conflict().size(), coreCost);
output.printf("c LB : %d CS : %d W : %d%n", lbCost, solver.assumptionsConflict().size(), coreCost);
}
if (!foundLowerBound(lbCost, null)) {
return MaxSATResult.UNDEF;
}
relaxCore(solver.conflict(), coreCost, assumptions);
relaxCore(solver.assumptionsConflict(), coreCost, assumptions);
solver = rebuildWeightSolver(weightStrategy);
} else {
nbSatisfiable++;
Expand Down Expand Up @@ -526,11 +526,11 @@ protected MaxSATResult normalSearch() {
return MaxSATResult.UNDEF;
} else if (res == FALSE) {
nbCores++;
assert solver.conflict().size() > 0;
final int coreCost = computeCostCore(solver.conflict());
assert solver.assumptionsConflict().size() > 0;
final int coreCost = computeCostCore(solver.assumptionsConflict());
lbCost += coreCost;
if (verbosity != Verbosity.NONE) {
output.printf("c LB : %d CS : %d W : %d%n", lbCost, solver.conflict().size(), coreCost);
output.printf("c LB : %d CS : %d W : %d%n", lbCost, solver.assumptionsConflict().size(), coreCost);
}
if (lbCost == ubCost) {
if (verbosity != Verbosity.NONE) {
Expand All @@ -540,7 +540,7 @@ protected MaxSATResult normalSearch() {
} else if (!foundLowerBound(lbCost, null)) {
return MaxSATResult.UNDEF;
}
relaxCore(solver.conflict(), coreCost, assumptions);
relaxCore(solver.assumptionsConflict(), coreCost, assumptions);
solver = rebuildSolver();
} else {
nbSatisfiable++;
Expand Down
Loading

0 comments on commit e7bd4e8

Please sign in to comment.