# 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

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:

Consider the following assignments:

`{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.`{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.`{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:

- You can encode a constraint manually using the PBEncoder and get a list of clauses of the CNF.
- You can call the
`cnf()`

method on a pseudo-Boolean constraint and get the resulting CNF directly.

Consider the pseudo-Boolean constraint

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: