Skip to content

Pseudo-Boolean Constraints

A pseudo-Boolean constraint PBConstraint is a generalization of a Cardinality Constraint. In a cardinality constraint, every variable has the same weight (i.e. 1); In a pseudo-Boolean constraint, each variable can have a different weight. Further, pseudo-Boolean constraints admit negated variables (literals), whereas cardinality constraints only admit variables.

Pseudo-Boolean constraints have the form

\[ c_1 \cdot lit_1 + c_2 \cdot lit_2 + ... + c_n \cdot lit_n \quad \mathtt{?} \quad k \]

where:

  • \(lit_i\) are Boolean literals, evaluating to true and false, for \(1 \leq i \leq n\)
  • \(c_i\) are integer coefficients, the "weights" of the literals, for \(1 \leq i \leq n\)
  • \(\mathtt{?}\) is a comparison operator <=, <, >, >= or =

A solution of a PB-constraint is an assignment of variables which satisfies the constraint (c.f. the next section).

Some examples for pseudo-Boolean constraints are:

  • Clauses: A | ~B | C is equivalent to A + ~B + C >= 1,
  • Cardinality constraints: A + B + C >= 3. Cardinality constraints are a special case of PB-constraints, where every coefficient is 1.
  • General constraints: A + 2*~B - 3*C = 2

Evaluating Pseudo-Boolean Constraints

If a literal in the pseudo-Boolean constraint evaluates to true for a given assignment, it is treated as 1; if it evaluates to false, it is treated as 0. When evaluating the pseudo-Boolean constraint, the left-hand side is evaluated first with standard rules of linear arithmetic and then compared to the right-hand side.

As an example, consider the pseudo-Boolean constraint:

A + 2*~B + -3*C = 2

Consider the following assignments:

  1. {A = true, B = true, C = true}. The left-hand side evaluates to 1 + 2*0 - 3*1 = -2, thus this is not a model for the formula.
  2. {A = true, B = false, C = false}. The left-hand side evaluates to 1 + 2*1 - 3*0 = 3, thus this is not a model for the formula.
  3. {A = false, B = false, C = false}. The left-hand side evaluates to 0 + 2*1 - 3*0 = 2, thus this is a model for the formula.

Negation vs. Minus

Note that the negation of a literal is different to the minus in front of a coefficient, therefore e.g. -2 * B is not equal to 2 * ~B: For the model {B = true}, -2 * B = -2, but 2 * ~B = 0.

Encoding Pseudo-Boolean Constraints

Some applications, such as SAT solvers, cannot deal with pseudo-Boolean constraints in their "natural form" since a pseudo-Boolean constraint is not a purely Boolean construct. Thus, the constraints have to be encoded to CNF before added to the solver. An encoded pseudo-Boolean constraint does not contain any signs like <=, >=, <, > and = or any coefficients anymore but is a proper Boolean formula in CNF. There exist many algorithms for encoding pseudo-Boolean constraints, depending on their type.

LogicNG implements some of these algorithms as described below. If you want to change the encoding of a pseudo-Boolean constraint using any of these algorithms, you can do this via the pseudo-Boolean constraint configuration PBConfig, see below. If you don't specify an encoding, then the default encoder is used. The default encoder for a certain pseudo-Boolean constraint was chosen based on theoretical and practical observations.

You can find a general overview over those algorithms here.

  • PBAdderNetworks: The adder networks encoding for pseudo-Boolean constraints to CNF.
  • PBSWC: A sequential weight counter for the encoding of pseudo-Boolean constraints in CNF. You can find information about this here.
  • PBBinaryMerge: This algorithm encodes for pseudo-Boolean constraints to CNF due to Manthey, Philipp, and Steinke. There are three parameters:
  • binaryMergeUseGAC: Sets whether general arc consistency should be used in the binary merge encoding. The default value is true.
  • binaryMergeNoSupportForSingleBit: Sets the support for single bits in the binary merge encoding. The default value is false
  • binaryMergeUseWatchDog: Sets whether the watchdog encoding should be used in the binary merge encoding. The default value is true.

The default encoding is the sequential weight counter PBSWC.

Using the Encoder

There are two ways to encode a pseudo-Boolean constraint:

  1. You can encode a constraint manually using the PBEncoder and get a list of clauses of the CNF.
  2. You can call the cnf() method on a pseudo-Boolean constraint and get the resulting CNF directly.

Consider the pseudo-Boolean constraint

A + 2*~B - 3*C = 2

which can be created in the following way:

List<Literal> lits =
        Arrays.asList(f.variable("A"), f.literal("B", false), f.variable("C"));
List<Integer> coeffs = Arrays.asList(1, 2, -3);
Formula f1 = f.pbc(CType.EQ, 2, lits, coeffs);

You can configure the PBEncoder with a PBConfig object. In this case we explicitly choose the PBBinaryMerge encoding with the parameter binaryMergeUseWatchDog set to false, to generate the CNF for this pseudo-Boolean constraint. When using the PBEncoder the result is a list of formulas, each representing a single clause of the encoding's CNF.

PBConfig config = PBConfig.builder()
        .pbEncoding(PBConfig.PB_ENCODER.BINARY_MERGE)
        .binaryMergeUseGAC(false)
        .build();
List<Formula> encoding = new PBEncoder(f, config).encode((PBConstraint) f1);

The result is then the list of clauses (again with replaces auxiliary variables for readability):

[
 (x1), (~A | C | x5), (C | x4) (~A | x4), (B | C | x9), (C | x8), (B | x8),
 (~x8 | ~x5 | x11), (~x9 | ~x5 | x12), (~x5 | x10), (~x8 | x10), (~x9 | x11),
 ~x12, ~B, ~C
]

When calling the cnf() method on the constraint, the default encoding configured in the formula factory is used. So when you change this default for pseudo-Boolean constraints to PBBinaryMerge with parameter binaryMergeUseWatchDog set to false beforehand, the result of calling cnf() yield the same result:

PBConfig config = PBConfig.builder()
        .pbEncoding(PBConfig.PB_ENCODER.BINARY_MERGE)
        .binaryMergeUseGAC(false).build();
f.putConfiguration(config);
Formula encoding = f1.cnf();

The result is the CNF equivalent to the clauses list above:

(x1) & (~A | C | x5) & (C | x4) & (~A | x4) & (B | C | x9) & (C | x8) &
(B | x8) & (~x8 | ~x5 | x11) & (~x9 | ~x5 | x12) & (~x5 | x10) &
(~x8 | x10) & (~x9 | x11) & ~x12 & ~B & ~C