Integer variables (`pysat.integer`)#

List of classes#

`Integer`	Finite-domain integer variable with a configurable CNF encoding.
`LinearExpr`	Minimal linear expression builder for `Integer` with numeric coefficients.
`IntegerEngine`	Thin wrapper around `BooleanEngine`: converts integer constraints to pseudo-Boolean linear constraints and delegates reasoning to `BooleanEngine`.

Module description#

This module provides a small set of experimental modelling and solving techniques for finite-domain integer variables and linear constraints, implemented on top of BooleanEngine. Integer variables are encoded into Boolean literals, while integer linear constraints are translated into Boolean linear (pseudo-Boolean) constraints with non-negative weights. Domain constraints are clausified into CNF clauses and can be added directly to the SAT solver; the propagator is used only for the remaining linear constraints.

The implementation is intentionally lightweight and aims to be simple and illustrative, providing working solutions that can be extended over time. It is not a full-featured CP solver and is not meant to be competitive with state-of-the-art CP or SMT tooling. It can serve educational and prototyping purposes and may evolve into a more complete front-end as (and if) additional constraints and encodings are added.

Given an integer variable \(x \in D\), the supported encodings of integer domains are:

Direct (value / one-hot) encoding [1] where a Boolean literal \(d_i \triangleq (x=i)\) is introduced for each value \(i \in D\). Exactly one value is allowed to be true.
Order (bound) encoding [2] [3] introduces Boolean literals \(o_i \triangleq (x \geq i)\) for each value \(i \in D\) representing the corresponding thresholds, with monotonicity constraints \(o_i \rightarrow o_{i-1}\).
Coupled encoding: both direct and order encodings are present with channeling clauses \(d_i \leftrightarrow (o_i \land \neg{o_{i+1}})\) linking them [4] [5], and no separate one-hot constraints are added for \(d_i\) because the order chain and channeling suffice to imply exactly one value (cf. constraints (3)–(7) in [4]).

Encodings can be mixed across variables (and even within the same linear constraint), as each variable \(x\) provides its own translation of a term \(c \cdot x\). Assuming the domain of variable \(x\) is \(D\), in the case of direct encoding, we have \(x = \sum_{i\in D}{i \cdot d_i}\) and so \(c \cdot x = \sum_{i\in D}{c \cdot i \cdot d_i}\). In the case of order encoding, it holds that \(x = \min(D) + \sum_{i=\min(D)+1}^{\max(D)}{o_i}\), so \(c \cdot x = c \cdot \min(D) + \sum_{i=\min(D)+1}^{\max(D)}{c \cdot o_i}\). Next, we apply the same rule to compute an offset value \(shift=-\min_{i\in D}{(c \cdot i)}\) such that each coefficient is incremented by \(shift\).

Translation of linear constraints over integer variables roughly follows the ideas described in [6]. Consider a linear constraint over integer variables \(x_j\) with numeric coefficients and the right-hand side: \(\sum_j c_j \cdot x_j \leq b\). The aim of the transformation is to booleanize each term \(c_j \cdot x_j\) of this expression (see the paragraph above) so the whole constraint becomes a pseudo-Boolean (PB) constraint: a sum of non-negative weights on positive Boolean literals. The flow is as follows:

Express each integer variable as a Boolean sum using variables \(d_i\) or \(o_i\), depending on the encoding of the domain of \(x_j\), i.e. either direct or order.
Multiply the resulting sum by the coefficient \(c_j\).
If any resulting weights are negative, which happens when \(c_j<0\), add a constant shift so that all weights become non-negative.
Drop all zero-weight literals (there is one per integer variable).

The final Boolean linear constraint has the form: \(\sum_k w_k \cdot l_k \leq b'\), where \(l_k\) are Boolean literals representing the integers involved, \(w_k > 0\) are weights, and \(b'\) is the shifted bound.

Consider an example constraint \(x - y \le 2\) with \(x\) and \(y\) sharing the domain \(\{1,2,3\}\) and assume direct encoding. Assume Boolean variables \(x_i\) and \(y_i\) play the role of direct encoding variables \(d_i\) from above. Observe that \(x = 1 \cdot x_1 + 2 \cdot x_2 + 3 \cdot x_3\) while \(-y = -1 \cdot y_1 - 2 \cdot y_2 - 3 \cdot y_3\). The shifts for \(x\) and \(y\) are \(-1\) and \(3\), respectively. The total shift is \(-1 + 3 = 2\), to be added to the right-hand side. The expressions for the terms are updated as follows: \(x = 0 \cdot x_1 + 1 \cdot x_2 + 2 \cdot x_3\) and \(-y = 2 \cdot y_1 + 1 \cdot y_2 + 0 \cdot y_3\). Removing zero-weight literals results in the final PB constraint: \(x_2 + 2\cdot x_3 + 2\cdot y_1 + y_2 \leq 4\).

Consider another example, this time with an order encoding: \(x + y \leq 2\) with the domain of both \(x\) and \(y\) being \([1,2]\). Assuming \(x_i\) and \(y_i\) play the role of order encoding variables \(o_i\) from above, we have: \(x=1 + x_2\) and \(y=1 + y_2\). The shift in both cases is calculated to be \(-1\) totalling to \(-2\), to be added to both sides of the inequality. Therefore, the final PB constraint is \(x_2 + y_2 \leq 0\).

The module also includes a minimal expression DSL (see LinearExpr) so that constraints can be written in a natural form (e.g. X + Y <= 4). Supported syntactic sugar includes +, -, unary negation, scalar * by numeric constants, and comparisons <=, >=, <, >, ==, !=. Notably unsupported are variable-variable multiplication, division, modulus, absolute values, and reification.

Integer variables can be declared to operate with either 'float' or 'decimal' coefficients, which is handled by the numeric parameter. Integer coefficients can be mixed with either mode. However, float and decimal coefficients must not be mixed in the same constraints, hence one cannot mix integers with float and decimal numeric modes.

Below is a compact 4x4 Sudoku example (digits 1..4). It demonstrates direct-encoded integer variables, AllDifferent constraints, and the use of the propagator. This is intentionally lightweight and meant to be illustrative.

>>> from pysat.integer import Integer, IntegerEngine
>>> from pysat.solvers import Cadical195
>>>
>>> # 4x4 Sudoku (2x2 blocks), 0 denotes empty
>>> givens = [
...     [0, 0, 2, 0],
...     [0, 0, 0, 3],
...     [0, 1, 0, 0],
...     [4, 0, 0, 0],
... ]
>>>
>>> X = [[Integer(f'x{r}{c}', 1, 4, encoding='direct')
...       for c in range(4)] for r in range(4)]
>>>
>>> eng = IntegerEngine([v for row in X for v in row], adaptive=False)
>>>
>>> # rows and columns
>>> for r in range(4):
...     eng.add_alldifferent(X[r])
>>> for c in range(4):
...     eng.add_alldifferent([X[r][c] for r in range(4)])
>>>
>>> # 2x2 blocks
>>> for br in (0, 2):
...     for bc in (0, 2):
...         block = [X[r][c] for r in range(br, br + 2)
...                           for c in range(bc, bc + 2)]
...         eng.add_alldifferent(block)
>>>
>>> # clues
>>> for r in range(4):
...     for c in range(4):
...         if givens[r][c]:
...             eng.add_linear(X[r][c] == givens[r][c])
>>>
>>> with Cadical195() as solver:
...     solver.connect_propagator(eng)
...     eng.setup_observe(solver)
...     if solver.solve():
...         model = solver.get_model()
...         values = eng.decode_model(model)
...         for r in range(4):
...             row = [values[X[r][c]] for c in range(4)]
...             print(row)
[1, 3, 2, 4]
[2, 4, 1, 3]
[3, 1, 4, 2]
[4, 2, 3, 1]

Module details#

class pysat.integer.Integer(name, lb, ub, encoding='direct', card_enc=1, vpool=None, numeric='float')#

Finite-domain integer variable with a configurable CNF encoding.

Supported encodings are:

'direct': one-hot / value encoding
'order': order / bound encoding
'coupled': both encodings with channeling clauses

Direct encoding uses Boolean literals \(d_i \triangleq (x=i)\) for each value \(i\) in the domain and a cardinality encoding to enforce that exactly one value is chosen. Order encoding introduces Boolean literals \(o_i \triangleq (x\ge i)\) and adds monotonicity implications between them. Coupled encoding mixes the two types of literals but omits explicit one-hot constraints for \(d_i\) since the order chain plus channeling already imply exactly one value.

Parameters:

name (str) – variable name
lb (int) – lower bound
ub (int) – upper bound
encoding (str) – domain encoding (‘direct’, ‘order’, or ‘coupled’)
card_enc (int) – cardinality encoding for the direct encoding (ignored for coupled encoding)
vpool (pysat.formula.IDPool or None) – external variable pool (optional)
numeric (str) – numeric mode (‘float’ or ‘decimal’)

Example:

>>> from pysat.integer import Integer
>>> X = Integer('X', 0, 3, encoding='direct')
>>> Y = Integer('Y', 0, 3, encoding='order')
>>> c1 = X + Y <= 4
>>> c2 = X - Y >= 1
>>> print(c1)
('linear', [[2, 3, 4, 5, 6, 7], 4, {2: 1, 3: 2, 4: 3, 5: 1, 6: 1, 7: 1}])
>>> print(c2)
('linear', [[1, 2, 3, 5, 6, 7], 2, {1: 3, 2: 2, 3: 1, 5: 1, 6: 1, 7: 1}])

Note

Integer coefficients attached to the variables can be mixed with either numeric mode. Mixing floats with decimals raises TypeError.

atleast(value)#: Return the literal representing \(x \geq value\). Same as ge().

atmost(value)#: Return the literal representing \(X \leq value\).

decode(model)#

Decode the integer value of the variable given a SAT model assigning the Boolean variables encoding the domain.

Parameters:: model (list(int)) – SAT model (list of literals)
Return type:: int or None

domain_clauses()#

Return CNF clauses encoding the variable’s domain.

Example:

>>> from pysat.integer import Integer
>>> X = Integer('X', 1, 3, encoding='direct')
>>> cnf = X.domain_clauses()
>>> print(cnf)
[[1, 2, 3], [-1, 4], [-4, 5], [-2, -4], [-2, 5], [-3, -5]]

Return type:: list(list(int))

encode(value)#

Encode an integer value as a list of true literals.

For direct encoding, the list contains a single Boolean literal \(d_i\) such that \(d_i \triangleq (x=i)\).

For order encoding, the list contains at most two Boolean literals \(o_i\) and \(\neg{o_{i+1}}\) such that \(o_i \triangleq (x \ge i)\) and \(o_{i+1} \triangleq (x \ge i+1)\). For the bound values, only one literal is used.

Parameters:: value (int or None) – domain value
Return type:: list(int)

equals(value)#

Return the Boolean literal corresponding to \(x = value\).

Only available with the direct (or coupled) encoding.

Parameters:: value (int) – domain value
Return type:: int

ge(value)#

Return the literal representing \(x \geq value\).

Only available with the order (or coupled) encoding.

Parameters:: value (int) – lower bound value
Return type:: int

le(value)#

Return the literal representing \(x \leq value\).

Only available with the order (or coupled) encoding.

Parameters:: value (int) – upper bound value
Return type:: int

linearize(coeff)#

Return a pair (weights, shift) encoding coeff * X using Boolean literals. The sum of weights for a satisfying assignment equals coeff * X + shift.

The shift is the negative of the minimum value of coeff * X over the variable’s domain. This normalization ensures all weights are non-negative (required by pysat.pb and BooleanEngine) while preserving equivalence by adjusting the bound by the same constant. When the minimum term is 0 (e.g., domain includes 0 with a non-negative coefficient), the shift is 0 and no adjustment occurs. For order encoding this corresponds to -coeff * lb when coeff >= 0 and -coeff * ub when coeff < 0, derived from the threshold identity for X.

For direct encoding, this is simply a per-value weight map. For example, if \(x \in \{0, 1, 2\}\) and \(2x\) is requested, then literals for values 0, 1, 2 get weights 0, 2, 4, respectively. For order encoding, we use the identity \(x = lb + \sum_{k=lb+1}^{ub} (x \geq k)\).

Parameters:: coeff (int, float, or Decimal) – coefficient
Return type:: (dict, number)

Consider an example (direct encoding, \(x \in \{0,1,2\}\)):

>>> x = Integer('X', 0, 2, encoding='direct')
>>> wmap, shift = x.linearize(-3)
>>> print(shift)
6
>>> # weights correspond to literals [x=0], [x=1], [x=2]
>>> print([wmap[x.equals(v)] for v in x.domain])
[6, 3, 0]

Here the minimum term is -3 * 2 = -6, so the shift is 6, which makes all weights in the final expression non-negative.

Consider another example, this time with a negative coefficient:

>>> y = Integer('y', 1, 3, encoding='direct')
>>> wmap, shift = y.linearize(-4)
>>> print(shift)
12
>>> # weights correspond to literals [y=1], [y=2], [y=3]
>>> print([wmap[y.equals(v)] for v in y.domain])
[8, 4, 0]

The minimum term is -4 * 3 = -12, so the shift is 12.

class pysat.integer.IntegerEngine(vars=None, constraints=None, adaptive=True, vpool=None)#

Thin wrapper around BooleanEngine: converts integer constraints to pseudo-Boolean linear constraints and delegates reasoning to BooleanEngine.

This is a somewhat experimental, simple and illustrative implementation rather than a performance-optimized CP solver.

Example:

>>> from pysat.integer import Integer, IntegerEngine
>>> from pysat.solvers import Solver
>>> X = Integer('X', 0, 3)
>>> Y = Integer('Y', 0, 3)
>>> eng = IntegerEngine([X, Y], adaptive=True)
>>> eng.add_linear(X + Y <= 4)
>>> eng.add_linear(X != Y)
>>> with Solver(name='cd195') as solver:
...     solver.connect_propagator(eng)
...     eng.setup_observe(solver)
...     while solver.solve():
...         model = solver.get_model()
...         vals = eng.decode_model(model)
...         print('model:', {var.name: value for var, value in vals.items()})
...         blits = eng.encode_model(vals)
...         solver.add_clause([-l for l in blits])
model: {'X': 1, 'Y': 0}
model: {'X': 2, 'Y': 0}
model: {'X': 0, 'Y': 1}
model: {'X': 2, 'Y': 1}
model: {'X': 1, 'Y': 2}
model: {'X': 0, 'Y': 2}

add_alldifferent(vars)#

Add an AllDifferent constraint over variables (for direct/coupled encoding only).

Parameters:: vars (list(Integer)) – variables to be all-different

add_linear(constraint)#

Add a constraint or a bundle of constraints to the engine.

Accepts a single LinearExpr-style constraint (e.g. X + Y <= 4), a list of such constraints (from ==), or a BooleanEngine’s 'linear' constraint tuple (or a list of them). The != operator is supported between Integer variables and between linear expressions (via auxiliary Boolean variables).

Note that in the case of variants of LinearExpr constraints, those are internally transformed into BooleanEngine-style PB constraint first.

Parameters:: constraint (LinearExpr | tuple | list) – constraint or list of constraints

add_not_equal(left, right)#

Add a not-equal constraint on two Integer variables: left != right (for direct/coupled encodings only).

Parameters:

left (Integer) – left variable
right (Integer) – right variable

add_var(var)#

Add a new integer variable and its domain clauses.

Parameters:: var (Integer) – integer variable

clausify(cardenc=1, pbenc=0)#

Clausify all constraints and return a CNF encoding. All linear constraints are converted using the user-specified cardinality and pseudo-Boolean encoding. The former are utilized for unweighted constraints, while the latter are utilized for weighted constraints.

Note that parameters cardenc and pbenc default to card.EncType.seqcounter and pysat.pb.EncType.best, respectively.

Parameters:

cardenc (int) – cardinality encoding for unweighted constraints
pbenc (int) – PB encoding for weighted constraints

Return type:

pysat.formula.CNF

decode_model(model, vars=None)#

Given a SAT model (list of int identifiers), return a mapping {Integer: integer_value} for the engine’s integer variables.

If vars is provided, decode only those variables.

Example:

>>> model = solver.get_model()
>>> values = eng.decode_model(model, vars=[X, Y])
>>> print(values)

Parameters:

model (list(int)) – SAT model (list of literals)
vars (list(Integer) or None) – subset of variables to decode (optional)

Return type:

dict

encode_model(model, vars=None)#

Given an integer-level model, return a list of true literals.

model can be a dict mapping Integer objects (preferred) or variable names to values, or a list/tuple of values corresponding to vars (or self.integers if vars is None).

This is the inverse of decode_model() at the integer level.

Parameters:

model (dict or list) – integer-level model
vars (list(Integer) or None) – variable order for list/tuple models (optional)

Return type:

list(int)

static pb_linear_leq(terms, bound)#: Convenience wrapper for building a PySAT 'linear' constraint (cardinality / pseudo-Boolean) from integer terms. Calls LinearExpr.pb_linear_leq().

setup_observe(solver)#

Inform the solver about observed variables and add domain clauses.

Parameters:: solver (pysat.solvers.Cadical195) – SAT solver instance

class pysat.integer.LinearExpr(terms=None, const=0, numeric='float')#

Minimal linear expression builder for Integer with numeric coefficients. Supports comparisons against numeric values.

The resulting comparisons return BooleanEngine-style constraints (tuples) that can be passed to IntegerEngine.add_linear(). Syntactic sugar supports +, -, unary negation, scalar * by numeric constants, and comparisons. Variable-variable multiplication, division, modulus, absolute values, and reification are not supported.

Example:

>>> from pysat.integer import Integer
>>> X = Integer('X', 0, 3)
>>> Y = Integer('Y', 0, 3, encoding='order')
>>> c1 = X + Y <= 4
>>> c2 = 2 * X - Y >= 1
>>> print(c1)
('linear', [[2, 3, 4, 5, 6, 7], 4, {2: 1, 3: 2, 4: 3, 5: 1, 6: 1, 7: 1}])
>>> print(c2)
('linear', [[1, 2, 3, 5, 6, 7], 5, {1: 6, 2: 4, 3: 2, 5: 1, 6: 1, 7: 1}])

Note

Integer constants (coefficients) can be mixed with either numeric mode. Mixing floats with decimals raises TypeError.

bounds()#: Compute a (min, max) pair for the expression over variable domains.

static pb_linear_leq(terms, bound)#

Build a PySAT 'linear' constraint over Boolean variables (cardinality / pseudo-Boolean) representing:

sum_i coeff_i * X_i <= bound

where the left-hand side of the constraint signifies a list of pairs (coeff_i, X_i) with coeff_i being a number and X_i being Integer and bound is a number.

Parameters:

terms (list of pairs (coeff, Integer)) – terms of the left-hand side
bound (number) – right-hand side

Example:

>>> from pysat.integer import Integer, LinearExpr
>>> X = Integer('X', 0, 2)
>>> Y = Integer('Y', 0, 2, encoding='order')
>>> c = LinearExpr.pb_linear_leq([(1, X), (2, Y)], 2)
>>> print(c)
('linear', [[2, 3, 4, 5], 2, {2: 1, 3: 2, 4: 2, 5: 2}])

Return type:: tuple

Integer variables (pysat.integer)#

List of classes#

Module description#

Module details#

Integer variables (`pysat.integer`)#