[Feature request] Equality optimization

Is your feature request related to a problem? Please describe.

Optimize the internal representation to separate equality and inequality constraints so that the algebraic operations can be performed on the subset of inequality constraints only much faster than the current approach that has both equality and inequality constraints.

Currently, an equality constraint is internally represented as two inequality constraints, see:

https://github.com/pacti-org/pacti/blob/2fd73407e05fdbafe1129b0e01016ac6b8c6d508/src/pacti/terms/polyhedra/serializer.py#L202-L224

When constructing large systems, we may have lots of binary constraints involving two variables. For example , the space mission case study's navigation loop generates increasingly long sequences of task contracts. It is useful to look at the size distribution of the constraints in these contracts:

1: shift: 0.068 compose: 0.868 each input: 32 vars, 55 constraints; result: 62 vars, 108 constraints; density=0.03644; size distribution: [(3, 48), (2, 40), (1, 20)]
2: shift: 0.139 compose: 2.640 each input: 62 vars, 108 constraints; result: 122 vars, 212 constraints; density=0.01871; size distribution: [(3, 96), (2, 80), (1, 36)]
3: shift: 0.443 compose: 9.269 each input: 122 vars, 212 constraints; result: 242 vars, 420 constraints; density=0.009484; size distribution: [(3, 192), (2, 160), (1, 68)]
4: shift: 1.761 compose: 58.307 each input: 242 vars, 420 constraints; result: 482 vars, 836 constraints; density=0.004775; size distribution: [(3, 384), (2, 320), (1, 132)]
5: shift: 10.935 compose: 272.684 each input: 482 vars, 836 constraints; result: 962 vars, 1668 constraints; density=0.002396; size distribution: [(3, 768), (2, 640), (1, 260)]

The time required for composing these contracts grows exponentially large as the contracts roughly double in number of constraints and variables.

However, notice that the fraction of 2-variable constraints is about 38% of the total number of constraints!

In the 3rd example, out of 160 binary constraints, there are 24 equality constraints that are internally represented as 48 inequality constraints.

Describe the solution you'd like A clear and concise description of what you want to happen.

Consider this contract example:

$a1 + a2 \leq b$ $a2 = a3$ $a3 + a4 \leq c$

Internally, it is represented as 4 inequality constraints:

$a1 + a2 \leq b$ $a2 - a3 \leq 0$ $-(a2 - a3) \leq 0$ $a3 + a4 \leq c$

I propose to separate the internal representation in two sets of constraints:

1) equalities

$a2 = a3$

Each equality equation involves a primary variable, e.g., the lhs ($a2$), and a redundant variable, e.g., the rhs ($a3$).

2) inequalities

$a1 + a2 \leq b$ $a2 + a4 \leq c$

This involves substituting the redundant variables by their equivalent primary variables. In this example, the 2nd constraint was originally $a3 + a4 \leq c$ and became $a2 + a4 \leq c$ after substitution.

The key idea is to reduce the size of the inequalities over which Pacti's algebra and optimization APIs operate to yield performance improvements.

Describe alternatives you've considered A clear and concise description of any alternative solutions or features you've considered.

Additional context Add any other context or screenshots about the feature request here.

pacti-org / pacti

[Feature request] Equality optimization #344