Skip to content

Tutorial: Encoding PB constraints to CNF (and back)

This guide walks you through the PbToCnfEncoder and CnfToPbDecoder plugins. You'll learn how to translate arithmetic-like Pseudo‑Boolean (PB) constraints into SAT‑friendly CNF, solve them, and then decode the result.

A PB constraint is a linear inequality over Boolean literals, e.g. \(3x + 2 \neg y - z \ge 5\). It is much more compact than pure CNF for expressing resource limits, cardinalities, or optimisation goals. While PB being a richer formalism to express constraints, SAT solvers (usually) deal with clauses only, so a common workflow is to express those higher constraints as PB and then use an encoder to transform them to clauses for the solver.

Encoding PB constraints

Loading an encoder

You have two static factory methods to instantiate your encoder: 

from paramita.encoders import PbToCnfEncoder

# Option 1: load by a registered name
encoder = PbToCnfEncoder.from_name("encoder name")

# Option 2: load by the path of the plugin
encoder = PbToCnfEncoder.dynamic_load("/path/to/my_encoder.so")

Tip

For this tutorial, you can use the paramita CLI to obtain an encoder:

paramita plugins build cmake "#pb-to-cnf-encoders/pblib"

And then in python 

encoder = PbToCnfEncoder.from_name("BestEncoder")

Note

If the encoder defines some parameters, you can pass them in the constructor or use .set(name, value).

Encoding a constraint

Call encode to translate a PB constraint into clauses. You need:

  • A PbConstraint object, defining the constraint to encode.
  • A ClauseContainer-like (e.g. a SAT solver, a CNF formula...). The generated clauses will be added to this container.

For now, we will ignore the context parameter.

Let's encode \(3x + 2 \neg y - z \ge 5\) into clauses using the best encoder from PbLib 1.

\(x\), \(y\), and \(z\) will be represented DIMACS boolean variables.

from paramita import PbConstraint
from paramita.containers import CnfFormula
from paramita.encoders import PbToCnfEncoder

x, y, z = (1, 2, 3)

pb = PbConstraint(
    lits=[x, y, z],
    weights=[3, 2, -1],
    op=PbConstraint.GTE,
    bound=5
)

f = CnfFormula()

encoder = PbToCnfEncoder.from_name("BestEncoder")
encoder.encode(pb, f)

print(f.clauses())

Tip

Encoders do not hold state. Thus, you can use them as many times as you want to encode new constraints. See the next section for the state management on incremental encoders.

Using incremental encoders

Sometimes we want to write PB constraints that only differ in the bound (the constant term in the expression). We can use an encoder multiple times to encode the PB constraints individually. But for some encoders, we can do something more efficient.

An incremental PB encoder is an encoder that holds some state about previous encodings, such that it can reuse previous encoded things to simplify new encodings.

Paramita enables the incremental capabilities of certain encoders by using a context instead of holding internal state:

  • encode has a context parameter that can be either None, or an instance of a context generated by a previous call.
  • encode returns a context after encoding some PB constraint. This is an opaque type, and it should be used exclusively by the encoder.

For example:

from paramita import PbConstraint
from paramita.containers import CnfFormula
from paramita.encoders import PbToCnfEncoder

x, y, z = (1, 2, 3)

pb = PbConstraint(
    lits=[x, y, z],
    weights=[3, 2, -1],
    op=PbConstraint.GTE,
    bound=5
)

f = CnfFormula()

encoder = PbToCnfEncoder.from_name("BestEncoder")
ctx = encoder.encode(pb, f)

print(f.clauses())

pb.bound = 6
f = CnfFormula()
encoder.encode(pb, f, ctx)

print(f.clauses())

Warning

On this example, we use a new formula to see what clauses are generated on the second call. This is usually not the desired workflow.

Tip

Note that by using a context, all encoders (incremental and non-incremental) can be used interchangeably. The only difference is that incremental encoders will use the context to be more efficient, while non-incremental encoders will have an empty context and behave as if they had never encoded anything.

Decoding constraints from CNF

Sometimes someone else performed the transformation from a higher formalism into CNF, and in the process we loose the information about those clauses representing this type of constraints. For some cases, this is not relevant, as we can deal with CNF just fine, but sometimes knowing the underlying PB constraint allows us to be more efficient in our reasoning process.

Paramita provides a mechanism to detect PB constraints from a CNF using the CnfToPbDecoder plugins.

Loading a decoder

You have two static factory methods to instantiate your decoder: 

from paramita.decoders import CnfToPbDecoder

# Option 1: load by a registered name
decoder = CnfToPbDecoder.from_name("decoder name")

# Option 2: load by the path of the plugin
decoder = CnfToPbDecoder.dynamic_load("/path/to/my_decoder.so")

Decoding PB constraints

The decoder provides a single method: decode, which receives:

  • a ClauseContainer (e.g. a SAT solver, a CNF...) with the clauses that will be analyzed to potentially find PBs
  • a target_lits sequence that receives a list of literals that can be used to restrict the PBs that are detected to a certain set of literals

The decode call returns a list of PBs that are detected in this CNF.

Warning

PB decoders are usually incomplete, meaning that there might be some PBs hidden in the CNF that can't be detected. This is implementation defined.

Next steps

Now you have seen the basics of transforming PBs to CNF and viceversa. You can move to modelling decision problems with a higher formalism or using a SAT solver.

  1. Tobias Philipp and Peter Steinke. Pblib – a library for encoding pseudo-boolean constraints into cnf. In Marijn Heule and Sean Weaver, editors, Theory and Applications of Satisfiability Testing – SAT 2015, volume 9340 of Lecture Notes in Computer Science, pages 9–16. Springer International Publishing, 2015. doi:10.1007/978-3-319-24318-4_2. ↩