BDDInteger#satAssignmentToLong: reduce requirement for fullSat
Callers use fullSatOne only to bias towards a lower value. Move this bias into the satAssignmentToLong
function and let callers pass in simpler BDDs.
@@ -83,13 +83,19 @@ public class BDDInteger {
if (_hasVariablesOnly) {
return Optional.of(satAssignmentToLong(bdd.minAssignmentBits()));
}
- return Optional.of(satAssignmentToLong(bdd.fullSatOne()));
+ return Optional.of(satAssignmentToLong(bdd.satOne()));
}
- /** @param satAssignment a satisfying assignment (i.e. produced by fullSat, allSat, etc) */
+ /**
+ * Returns the smallest long produced when evaluating the given assignment {@link BDD} over the
+ * representative bits in {@link #getBitvec()}.
+ *
+ * <p>When this {@link BDDInteger#hasVariablesOnly()} is {@code false}, this function will perform
+ * better if the assignment {@link BDD} is smaller, i.e., is produced by {@link BDD#satOne()}
+ * instead of {@link BDD#fullSatOne()}.
+ */
public Long satAssignmentToLong(BDD satAssignment) {
- // TODO this check could be better (should be exactly 1 path from root to the one node).
- checkArgument(!satAssignment.isZero(), "not a satisfying assignment");
+ checkArgument(satAssignment.isAssignment(), "not a satisfying assignment");
if (_hasVariablesOnly) {
// Shortcut for performance.
@@ -104,7 +110,9 @@ public class BDDInteger {
long value = 0;
for (int i = 0; i < _bitvec.length; i++) {
BDD bitBDD = _bitvec[_bitvec.length - i - 1];
- if (satAssignment.andSat(bitBDD)) {
+ // a.diff(b) is a.and(b.not()). When the input is only a partial assignment (like satOne),
+ // this biases towards lexicographically smaller solutions: set a 1 only if you can't set 0.
+ if (!satAssignment.diffSat(bitBDD)) {
value |= 1L << i;
}
}
@@ -146,12 +154,10 @@ public class BDDInteger {
int num = 0;
BDD pred = bdd;
while (num < max) {
- BDD satAssignment = pred.fullSatOne();
- if (satAssignment.isZero()) {
+ if (pred.isZero()) {
break;
}
-
- long val = satAssignmentToLong(satAssignment);
+ long val = satAssignmentToLong(pred.satOne());
values.add(val);
pred = pred.diff(value(val));
num++;
