Skip to content

Using variable pools

Most SAT solvers use the DIMACS format to represent boolean variables, where each variable has a number associated to it (e.g. \(x\) maps to 1), and the integer being positive or negative means that the variable appears as a variable or its negation.

In Paramita, when we model decision or optimization problems we use the Bool class to represent the boolean variables with a readable name.

When we translate from this high-level representation to a DIMACS-based representation (e.g. a CnfFormula), we need a way to track the integer representation of each variable. For this, Paramita offers the DimacsVariablePool class.

You typically start with an empty pool:

from paramita.modelling import DimacsVariablePool

pool = DimacsVariablePool()

The pool assigns integer identifiers to the variables automatically as you request them. The first variable gets 1, the second 2, and so on.

If you need a specific mapping, you can pre-populate it:

pool = DimacsVariablePool({"x": 1, "y": 3})
This bounds each variable to the desired integer. Note though, that the pool keeps track of the highest value, so the identifier 2 will not be used, and the next variable will have 4 assigned to it.


To obtain the DIMACS representation of a variable we can use the get_variable method:

from paramita.modelling import Bool

x = Bool("x")
y = Bool("y")

pool = DimacsVariablePool({"x": 5})

print(pool.get_variable(x.name)) # prints 5
print(pool.get_variable(y.name)) # prints 6

You can see that \(x\) was known by the pool, but \(y\) wasn't. So for the new variable, it assigned the next free identifier.


The counterpart to get_variable is decode_literal. It takes a DIMACS literal (a positive or negative integer) and returns the corresponding Paramita expression object.

pool = DimacsVariablePool({"x": 1, "y": 2})

expr1 = pool.decode_literal(1)    # returns Bool("x")
expr2 = pool.decode_literal(-1)   # returns ~Bool("x") (a Not operation)
expr3 = pool.decode_literal(2)    # returns Bool("y")
  • A positive integer returns the Bool object itself.
  • A negative integer returns the negated form (~Bool).

If the variable number has never been registered, the method returns None. This is particularly handy when you receive a model from a SAT solver (as a list of DIMACS literals) and want to translate it back into a dictionary of Bool assignments without manually tracking numbers:

model_from_solver = [1, -2, 3]   # e.g., from solver.model()
for lit in model_from_solver:
    expr = pool.decode_literal(lit)
    print(f"{lit} -> {expr}")

Auxiliary variables

Many encodings (PB‑to‑CNF, reification, Tseitin transformation) need to introduce fresh variables that do not correspond to any user‑defined ones. The pool provides a dedicated method to generate those so called auxiliary variables:

aux1 = pool.new_aux() # a new Bool
aux2 = pool.new_aux() # a new Bool

Note

Auxiliary variables are intended to be used as anonymous variables.

For the interested reader, the name assigned to the variables is f"aux_{i}", where i is the next free auxiliary identifier. So in the example, aux1 would be a Bool("aux_1") and aux2 would be Bool("aux_2").

The auxiliary variables are unique within the same pool, but are not globally unique in the application.