Skip to content

Commit

Permalink
support adding of incremental cardinality constraints in MiniSat
Browse files Browse the repository at this point in the history
  • Loading branch information
@czengler
czengler committed Jun 16, 2016
1 parent 7146c65 commit f25bc8b
Show file tree
Hide file tree
Showing 17 changed files with 391 additions and 122 deletions.
6 changes: 2 additions & 4 deletions src/main/java/org/logicng/cardinalityconstraints/CCALKCardinalityNetwork.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,6 @@

package org.logicng.cardinalityconstraints;

import org.logicng.formulas.FormulaFactory;
import org.logicng.formulas.Variable;

/**
Expand All @@ -43,10 +42,9 @@ final class CCALKCardinalityNetwork implements CCAtLeastK {

/**
* Constructs a new cardinality encoder.
* @param f the formula factory
*/
CCALKCardinalityNetwork(final FormulaFactory f) {
this.cardinalityNetwork = new CCCardinalityNetworks(f);
CCALKCardinalityNetwork() {
this.cardinalityNetwork = new CCCardinalityNetworks();
}

@Override
Expand Down
6 changes: 2 additions & 4 deletions src/main/java/org/logicng/cardinalityconstraints/CCALKTotalizer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,6 @@

package org.logicng.cardinalityconstraints;

import org.logicng.formulas.FormulaFactory;
import org.logicng.formulas.Variable;

/**
Expand All @@ -43,10 +42,9 @@ final class CCALKTotalizer implements CCAtLeastK {

/**
* Constructs a new totalizer.
* @param f the formula factory
*/
CCALKTotalizer(final FormulaFactory f) {
this.totalizer = new CCTotalizer(f);
CCALKTotalizer() {
this.totalizer = new CCTotalizer();
}

@Override
Expand Down
6 changes: 2 additions & 4 deletions src/main/java/org/logicng/cardinalityconstraints/CCAMKCardinalityNetwork.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,6 @@

package org.logicng.cardinalityconstraints;

import org.logicng.formulas.FormulaFactory;
import org.logicng.formulas.Variable;

/**
Expand All @@ -43,10 +42,9 @@ final class CCAMKCardinalityNetwork implements CCAtMostK {

/**
* Constructs a new cardinality encoder.
* @param f the formula factory
*/
CCAMKCardinalityNetwork(final FormulaFactory f) {
this.cardinalityNetwork = new CCCardinalityNetworks(f);
CCAMKCardinalityNetwork() {
this.cardinalityNetwork = new CCCardinalityNetworks();
}

@Override
Expand Down
6 changes: 2 additions & 4 deletions src/main/java/org/logicng/cardinalityconstraints/CCAMKTotalizer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,6 @@

package org.logicng.cardinalityconstraints;

import org.logicng.formulas.FormulaFactory;
import org.logicng.formulas.Variable;

/**
Expand All @@ -43,10 +42,9 @@ final class CCAMKTotalizer implements CCAtMostK {

/**
* Constructs a new totalizer.
* @param f the formula factory
*/
CCAMKTotalizer(final FormulaFactory f) {
this.totalizer = new CCTotalizer(f);
CCAMKTotalizer() {
this.totalizer = new CCTotalizer();
}


Expand Down
10 changes: 3 additions & 7 deletions src/main/java/org/logicng/cardinalityconstraints/CCCardinalityNetworks.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,6 @@
package org.logicng.cardinalityconstraints;

import org.logicng.collections.LNGVector;
import org.logicng.formulas.FormulaFactory;
import org.logicng.formulas.Literal;
import org.logicng.formulas.Variable;

Expand All @@ -67,16 +66,13 @@
*/
final class CCCardinalityNetworks {

private final FormulaFactory f;
private final CCSorting sorting;
private CCIncrementalData incData;

/**
* Constructs a new cardinality encoder.
* @param f the formula factory
*/
CCCardinalityNetworks(final FormulaFactory f) {
this.f = f;
CCCardinalityNetworks() {
this.sorting = new CCSorting();
}

Expand Down Expand Up @@ -108,7 +104,7 @@ void buildAMKForIncremental(final CCResult result, final Variable[] vars, int rh
this.sorting.sort(rhs + 1, input, result, output, INPUT_TO_OUTPUT);
assert (output.size() > rhs);
result.addClause(output.get(rhs).negate());
this.incData = new CCIncrementalData(this.f, CCConfig.AMK_ENCODER.CARDINALITY_NETWORK, rhs, output);
this.incData = new CCIncrementalData(result, CCConfig.AMK_ENCODER.CARDINALITY_NETWORK, rhs, output);
}

void buildALK(final CCResult result, final Variable[] vars, int rhs) {
Expand Down Expand Up @@ -141,7 +137,7 @@ void buildALKForIncremental(final CCResult result, final Variable[] vars, int rh
this.sorting.sort(newRHS + 1, input, result, output, INPUT_TO_OUTPUT);
assert (output.size() > newRHS);
result.addClause(output.get(newRHS).negate());
this.incData = new CCIncrementalData(this.f, CCConfig.ALK_ENCODER.CARDINALITY_NETWORK, rhs, vars.length, output);
this.incData = new CCIncrementalData(result, CCConfig.ALK_ENCODER.CARDINALITY_NETWORK, rhs, vars.length, output);
}

void buildEXK(final CCResult result, final Variable[] vars, int rhs) {
Expand Down
6 changes: 2 additions & 4 deletions src/main/java/org/logicng/cardinalityconstraints/CCEXKCardinalityNetwork.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,6 @@

package org.logicng.cardinalityconstraints;

import org.logicng.formulas.FormulaFactory;
import org.logicng.formulas.Variable;

/**
Expand All @@ -43,10 +42,9 @@ final class CCEXKCardinalityNetwork implements CCAtMostK {

/**
* Constructs a new cardinality encoder.
* @param f the formula factory
*/
CCEXKCardinalityNetwork(final FormulaFactory f) {
this.cardinalityNetwork = new CCCardinalityNetworks(f);
CCEXKCardinalityNetwork() {
this.cardinalityNetwork = new CCCardinalityNetworks();
}

@Override
Expand Down
6 changes: 2 additions & 4 deletions src/main/java/org/logicng/cardinalityconstraints/CCEXKTotalizer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,6 @@

package org.logicng.cardinalityconstraints;

import org.logicng.formulas.FormulaFactory;
import org.logicng.formulas.Variable;

/**
Expand All @@ -43,10 +42,9 @@ final class CCEXKTotalizer implements CCExactlyK {

/**
* Constructs a new totalizer.
* @param f the formula factory
*/
CCEXKTotalizer(final FormulaFactory f) {
this.totalizer = new CCTotalizer(f);
CCEXKTotalizer() {
this.totalizer = new CCTotalizer();
}


Expand Down
62 changes: 38 additions & 24 deletions src/main/java/org/logicng/cardinalityconstraints/CCEncoder.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -121,32 +121,46 @@ public void encode(final PBConstraint cc, final CCResult result) {
this.encodeConstraint(cc, result);
}

/**
* Encodes an incremental cardinality constraint and returns its encoding.
* @param cc the cardinality constraint
* @return the encoding of the constraint and the incremental data
*/
public Pair<ImmutableFormulaList, CCIncrementalData> encodeIncremental(final PBConstraint cc) {
final CCResult result = CCResult.resultForFormula(f);
final CCIncrementalData incData = this.encodeIncremental(cc, result);
return new Pair<>(new ImmutableFormulaList(FType.AND, result.result()), incData);
}

/**
* Encodes an incremental cardinality constraint on a given solver.
* @param cc the cardinality constraint
* @param result the result of the encoding
* @return the incremental data
*/
public CCIncrementalData encodeIncremental(final PBConstraint cc, final CCResult result) {
return this.encodeIncrementalConstraint(cc, result);
}

private CCIncrementalData encodeIncrementalConstraint(final PBConstraint cc, final CCResult result) {
if (!cc.isCC())
throw new IllegalArgumentException("Cannot encode a non-cardinality constraint with a cardinality constraint encoder.");
final Variable[] ops = litsAsVars(cc.operands());
final CCResult result = CCResult.resultForFormula(f);
switch (cc.comparator()) {
case LE:
if (cc.rhs() == 1)
throw new IllegalArgumentException("Incremental encodings are not supported for at-most-one constraints");
else {
final CCIncrementalData incData = this.amkIncremental(result, ops, cc.rhs());
return new Pair<>(new ImmutableFormulaList(FType.AND, result.result()), incData);
}
else
return this.amkIncremental(result, ops, cc.rhs());
case LT:
if (cc.rhs() == 2)
throw new IllegalArgumentException("Incremental encodings are not supported for at-most-one constraints");
else {
final CCIncrementalData incData = this.amkIncremental(result, ops, cc.rhs() - 1);
return new Pair<>(new ImmutableFormulaList(FType.AND, result.result()), incData);
}
else
return this.amkIncremental(result, ops, cc.rhs() - 1);
case GE:
CCIncrementalData incData = this.alkIncremental(result, ops, cc.rhs());
return new Pair<>(new ImmutableFormulaList(FType.AND, result.result()), incData);
return this.alkIncremental(result, ops, cc.rhs());
case GT:
incData = this.alkIncremental(result, ops, cc.rhs() + 1);
return new Pair<>(new ImmutableFormulaList(FType.AND, result.result()), incData);
return this.alkIncremental(result, ops, cc.rhs() + 1);
default:
throw new IllegalArgumentException("Incremental encodings are only supported for at-most-k and at-least k constraints.");
}
Expand Down Expand Up @@ -307,7 +321,7 @@ private void amk(final CCResult result, final Variable[] vars, int rhs) {
switch (this.config().amkEncoder) {
case TOTALIZER:
if (this.amkTotalizer == null)
this.amkTotalizer = new CCAMKTotalizer(this.f);
this.amkTotalizer = new CCAMKTotalizer();
this.amkTotalizer.build(result, vars, rhs);
break;
case MODULAR_TOTALIZER:
Expand All @@ -317,7 +331,7 @@ private void amk(final CCResult result, final Variable[] vars, int rhs) {
break;
case CARDINALITY_NETWORK:
if (this.amkCardinalityNetwork == null)
this.amkCardinalityNetwork = new CCAMKCardinalityNetwork(this.f);
this.amkCardinalityNetwork = new CCAMKCardinalityNetwork();
this.amkCardinalityNetwork.build(result, vars, rhs);
break;
case BEST:
Expand Down Expand Up @@ -348,7 +362,7 @@ private CCIncrementalData amkIncremental(final CCResult result, final Variable[]
switch (this.config().amkEncoder) {
case TOTALIZER:
if (this.amkTotalizer == null)
this.amkTotalizer = new CCAMKTotalizer(this.f);
this.amkTotalizer = new CCAMKTotalizer();
this.amkTotalizer.build(result, vars, rhs);
return this.amkTotalizer.incrementalData();
case MODULAR_TOTALIZER:
Expand All @@ -358,7 +372,7 @@ private CCIncrementalData amkIncremental(final CCResult result, final Variable[]
return this.amkModularTotalizer.incrementalData();
case CARDINALITY_NETWORK:
if (this.amkCardinalityNetwork == null)
this.amkCardinalityNetwork = new CCAMKCardinalityNetwork(this.f);
this.amkCardinalityNetwork = new CCAMKCardinalityNetwork();
this.amkCardinalityNetwork.buildForIncremental(result, vars, rhs);
return this.amkCardinalityNetwork.incrementalData();
case BEST:
Expand Down Expand Up @@ -396,7 +410,7 @@ private void alk(final CCResult result, final Variable[] vars, int rhs) {
switch (this.config().alkEncoder) {
case TOTALIZER:
if (this.alkTotalizer == null)
this.alkTotalizer = new CCALKTotalizer(this.f);
this.alkTotalizer = new CCALKTotalizer();
this.alkTotalizer.build(result, vars, rhs);
break;
case MODULAR_TOTALIZER:
Expand All @@ -406,7 +420,7 @@ private void alk(final CCResult result, final Variable[] vars, int rhs) {
break;
case CARDINALITY_NETWORK:
if (this.alkCardinalityNetwork == null)
this.alkCardinalityNetwork = new CCALKCardinalityNetwork(this.f);
this.alkCardinalityNetwork = new CCALKCardinalityNetwork();
this.alkCardinalityNetwork.build(result, vars, rhs);
break;
case BEST:
Expand Down Expand Up @@ -445,7 +459,7 @@ private CCIncrementalData alkIncremental(final CCResult result, final Variable[]
switch (this.config().alkEncoder) {
case TOTALIZER:
if (this.alkTotalizer == null)
this.alkTotalizer = new CCALKTotalizer(this.f);
this.alkTotalizer = new CCALKTotalizer();
this.alkTotalizer.build(result, vars, rhs);
return this.alkTotalizer.incrementalData();
case MODULAR_TOTALIZER:
Expand All @@ -455,7 +469,7 @@ private CCIncrementalData alkIncremental(final CCResult result, final Variable[]
return this.alkModularTotalizer.incrementalData();
case CARDINALITY_NETWORK:
if (this.alkCardinalityNetwork == null)
this.alkCardinalityNetwork = new CCALKCardinalityNetwork(this.f);
this.alkCardinalityNetwork = new CCALKCardinalityNetwork();
this.alkCardinalityNetwork.buildForIncremental(result, vars, rhs);
return this.alkCardinalityNetwork.incrementalData();
case BEST:
Expand Down Expand Up @@ -492,12 +506,12 @@ private void exk(final CCResult result, final Variable[] vars, int rhs) {
switch (this.config().exkEncoder) {
case TOTALIZER:
if (this.exkTotalizer == null)
this.exkTotalizer = new CCEXKTotalizer(this.f);
this.exkTotalizer = new CCEXKTotalizer();
this.exkTotalizer.build(result, vars, rhs);
break;
case CARDINALITY_NETWORK:
if (this.exkCardinalityNetwork == null)
this.exkCardinalityNetwork = new CCEXKCardinalityNetwork(this.f);
this.exkCardinalityNetwork = new CCEXKCardinalityNetwork();
this.exkCardinalityNetwork.build(result, vars, rhs);
break;
case BEST:
Expand Down Expand Up @@ -562,7 +576,7 @@ private CCAtLeastK bestALK(int n) {
*/
private CCExactlyK bestEXK(int n) {
if (this.exkTotalizer == null)
this.exkTotalizer = new CCEXKTotalizer(this.f);
this.exkTotalizer = new CCEXKTotalizer();
return this.exkTotalizer;
}

Expand Down
Loading

0 comments on commit f25bc8b

Please sign in to comment.