Complete implied-equality basis

Status: Open lead. Owner: unassigned.

Investigate whether computing a complete arithmetic equality basis can reduce the cost of exact shared-pair probes. Integration design, implementation, and evaluation remain open. This carries forward lead 17 in the original register.

Implemented baseline

The combination chapter describes the local tableau rules and exact fallback. The local rules can miss entailed equalities; the fallback tests unresolved model-equal pairs in both strict orientations. A complete equality basis is not currently maintained for this purpose.

Investigation and paper basis

Martin Bromberger, Decision Procedures for Linear Arithmetic, PhD thesis, 2019, Chapter 5, supplies the proposed basis. Section 5.4.1 uses the computed equality basis to normalize variables, making implied equality a comparison of normalized expressions. Section 5.4.2 derives explanations from the tight bounds used by that normalization. These are proposed extensions to Primo, not a description of its current equality producer.

The same thesis connects equality elimination to cube tests (§5.7), as explained in the arithmetic reading guide. An integer application needs a separate integrality argument: a rational substitution such as \(x=y/2\) requires even \(y\) when \(x\) is integer. A complete basis of equalities over the real relaxation does not itself enforce these divisibility conditions or find every equality implied only over integers.

Start by measuring exact-probe frequency and time across representative QF_UFLRA inputs, including the expensive tail. The retained thesis note and original lead preserve the earlier rationale and screening proposal. If probes are a material cost, write an implementation checklist covering basis construction, explanations, strict bounds, and rollback before prototyping. Establish the supported arithmetic fragment explicitly.

Any prototype must retain the current correctness boundary, pass the correctness gates, and independently validate printed SAT models. Compare total solving time and memory with the unchanged baseline; cheaper pair queries alone do not justify the cost of maintaining the basis.