Linear integer arithmetic

This theory follows the shared assignment and explanation contract. Both standalone QF_LIA and combined QF_UFLIA use one LIA adapter implementing TheoryComponent; the integer algorithms described here run behind that boundary. The interface inventory explains the adapters and their responsibilities.

An arithmetic assignment can satisfy every linear inequality and still fail to be an integer model. For example, 2*x - 2*y = 1 has the real solution x = 1/2, y = 0, but no integer solution: its left side is even. Primo first solves the real relaxation, then tries to repair the assignment or prove that the current Boolean choice has no integer completion.

This chapter describes the integer stages shared by QF_LIA and QF_UFLIA. Configured resource limits can stop the search with unknown. Removing those limits alone does not guarantee a terminating decision procedure for all quantifier-free linear integer inputs: with unbounded variables, the current branch-and-bound search can follow an infinite path. The budgets and incomplete cases section distinguishes this algorithmic limitation from resource exhaustion and gives a concrete example.

Representation and ownership

The integer procedures reuse LraTableau. A row has the form

\[x_b=\sum_j a_jx_j,\]

where \(x_b\) is basic, the \(x_j\) are nonbasic, and the coefficients are exact rationals. “Basic” means that the row determines the variable’s value from the nonbasic values; pivoting changes which variable occupies that role. Bounds and assignments use DeltaRational: a pair \(q+d\delta\), with \(\delta\) a positive infinitesimal used to represent strict inequalities.

State	Owner and meaning
Prepared atoms and term-to-variable map	PreparedLraTheory connects arithmetic terms and SAT atoms to tableau variables and bounds.
integer_vars	The caller owns a vector of LraVarIds whose values must become integers. In the pure route it is collected from the Int terms in variables_by_term; the combined route also registers shared Int terms. It is not the set of all tableau variables.
Working tableau	SMT integration owns a copy of a rationally feasible tableau and lends it by mutable reference to complete_integer_assignment. Patching changes assignments; cuts allocate variables and rows; branching adds temporary bounds. These changes stay within this copy.
LiaExplanation	This explanation object stores the blocking literals contributed by GCD checks, cuts and branching in a sorted, duplicate-free vector. The stages share one object so a later conflict retains the reasons for earlier cuts.
Branch frames	branch_and_bound owns an explicit DFS stack. Each frame stores a variable ID, a split threshold, a tableau checkpoint and which side has been tried.

LraVarId is an index within a tableau and its matching copies, not a core TermId or a SAT variable. Appending a cut gives it a new ID without changing existing IDs. Neither the temporary cut variable nor a branch bound creates a core term or a new SAT atom. The working copy is discarded when its Boolean candidate is rejected; a winning copy supplies the integer model.

An auxiliary variable for a normalized polynomial need not be integer-valued. For example, dividing 2*x + y by its leading coefficient produces \(s=x+y/2\). Even with integer \(x,y\), \(s\) may be a half-integer. Conversely, normalizing 3*x <= 5 gives the direct bound \(x\le5/3\): no auxiliary row is needed. The variable is integer, but its current bound is fractional. These are different cases of the normalization described in LRA.

The integer set records semantic obligations, independently of the current basis. A pivot can move a noninteger auxiliary variable into another row as an ordinary term. No integer rule may assume that nonbasic variables are integers just because the original input used Int.

When integer reasoning runs

The standalone solve_qf_lia_impl recipe selects one LiaTheoryComponent and calls solve_component_recipe. Online rational propagation stays enabled independently of EUF settings. Model-guided combination is disabled: with only one component, there are no shared scopes, interface arrangements, equality bridges, or combination fallback. QF_UFLIA selects the same LIA component alongside EUF.

The driver observes otherwise unowned Boolean constants through SAT’s assignment interface, in the original atom registry order. Their assignments remain propositional: the dispatcher does not route them into the LIA component. Observing them preserves the standalone route’s SAT elimination policy while making their values available in the shared assignment view and final model.

At the full-model check boundary, the LIA adapter copies the rationally feasible online tableau once, or moves a newly rebuilt rational tableau, into integer completion. It passes LiaCompletionLimits (patch moves, Gomory rounds, and branch nodes). Both routes run this pipeline:

Order	Operation	Result used by the caller
1	Patch fractional integer values	A feasible assignment with fewer fractional integer variables, or no progress.
2	Check row divisibility using GCDs	A conflict, or no contradiction found.
3	Add a bounded sequence of Gomory cuts and recheck	A conflict, or a feasible tableau strengthened by the cuts.
4	Branch on fractional integer variables	An integer model, exhaustion of all branches, or a node-limit result.

GCD checks and cuts run before branching, not at each branch node. A zero cut or patch budget skips that stage. Even if patching makes every required variable integral, the final success decision comes through branch-and-bound’s integrality check, which then needs no branch nodes.

A refuted candidate produces a clause over the original arithmetic atoms. The shared driver adds it to the SAT backend and searches for another Boolean candidate. It reports unsat for the whole query when that search is exhausted; integer infeasibility of one candidate does not by itself refute a formula with other Boolean choices.

The standalone recipe sets CombinationRecipe::forgettable_clauses to false: its online external theory clauses remain permanent in the SAT backend, preserving the standalone route’s retention policy. ComponentDispatcher stores this policy for its lifetime and applies it to external clauses, including after the driver rebuilds the dispatcher for new atoms. Combined recipes retain the default true policy, which permits SAT clause deletion. This affects search and memory use, not the validity of the theory clauses.

QF_UFLIA calls the same complete_integer_assignment operation through complete_lia_integer_model. Its LIA component adapter keeps the winning tableau, exports shared integer values, or returns a learned clause/resource-limit result to the general combination driver. Rational online propagation and final integer completion have separate responsibilities. LiaTheoryComponent owns this adapter and the optional online rational execution state. ComponentAdapterSupport owns the assignment view, registered atoms, interface terms, and model-token revision. Atom growth destroys the online execution state before changing the preparation it borrows; assignment and backtracking invalidate the exported model token.

The recipe passes model-projection policy and LiaComponentTiming explicitly. The adapter does not read QF_UFLIA combination options to select its behavior. The combined recipe retains its check, rational, and integer timer keys; empty keys disable timer sampling. Both rebuilt rational checks and completion of an online tableau use LiaComponentAdapter::translate to replace the retained model and return a consistent, learned-clause, or resource-limit result. If requested projection omits a shared Int term, translation returns Unknown with that diagnostic. Shared model projection is produced only when the recipe requests it. The shared-sort contract is Int-only.

The combination chapter explains the remaining equality arrangements and model-agreement checks.

LiaCompletionResult returns a typed Sat, Unsat, or ResourceLimit, one accumulated LiaExplanation, the number of patched variables, and LiaPatchingStats. The completion operation does not copy or prepare the tableau and preserves the supplied integer-variable ordering. On success the caller reads the winning assignment directly; after a failed or limited branch search, cuts remain but speculative branch bounds are removed. It does not restore the entry basis or assignment. The caller discards unsuccessful working copies. A zero branch budget permits an already integral assignment but no branch node.

Both routes use SMT integration’s integer_conflict_clause to collect blocking literals from the asserted arithmetic atoms. It handles an empty coarse clause explicitly; otherwise the existing optional generalization checks the accumulated explanation against that clause. Individual failed integer branches do not increment the aggregate conflict budget; the SMT caller counts the reported theory conflict. The patcher’s fully_integral statistic uses its maintained remaining-variable count, avoiding another scan. Both routes publish it when patching is enabled.

The completion boundary preserves stage order, variable order, limits, the winning assignment, and antecedents from cuts used by later branching. It adds no tableau copies, preparation, or full scans. The stage-specific sources and limitations below apply to both callers.

This design keeps integer branch choices inside the theory procedure. SAT learns the resulting conflict clause, but does not see individual integer splits as CDCL decisions. That simplifies the boundary and the lifetime of temporary rows; it also means that internal branch choices and cuts are not reused across successive Boolean candidates.

Input lowering and integer bounds

Preprocessing profiles explains the automatic and explicit integer pass schedules. The transformations below run even when the optional repeated round is disabled.

Here, lowering means translating an input construct into simpler terms and constraints supported by the solving stages. Each translation below specifies the replacement and any fresh variables it introduces.

The frontend admits linear Int expressions and comparisons under QF_LIA; uninterpreted functions require QF_UFLIA. The integer logics reject Real declarations. Products must have a constant coefficient. Primo also accepts constant-divisor div/mod and integer abs as extensions to its QF_LIA input; that is not a claim of strict QF_LIA grammar conformance.

Extended-term lowering runs even when optional preprocessing is off. For positive integer \(k\), a quotient \(q\) for div(t,k) is constrained by

\[0\le t-kq\le k-1.\]

mod(t,k) becomes the residual \(t-kq\). Equal numerator/divisor pairs share one quotient. The inequalities characterize a unique integer quotient and a remainder in \([0,k-1]\): two distinct quotients would make the remainders differ by at least \(k\), which that interval cannot contain. For instance, \(-7=3(-3)+2\), so the quotient is \(-3\) and the remainder is \(2\). Term construction normalizes a negative divisor by negating the positive-divisor quotient and preserving the remainder. Zero and nonconstant divisors are rejected.

abs(t) is lowered through ite(0 <= t, t, -t). Non-Boolean ite introduces a fresh constant with guarded equalities to its two possible values. Equality lowering, despite its lower_real_equalities name, also handles Int: \(a=b\) becomes \((a\le b)\land(b\le a)\). Negating the equality therefore lets SAT choose a false non-strict comparison. Integer strictness must account for that polarity, not just syntactic < atoms.

bound_assertion computes the bound direction and strictness from the normalized relation, orientation and truth value. When the bounded variable is known to be integer, it uses

\[x<r\iff x\le\lceil r\rceil-1, \qquad x>r\iff x\ge\lfloor r\rfloor+1.\]

Thus 3*x < 5 yields \(x\le1\), while a false 3*x <= 5 yields \(x\ge2\). Subtracting or adding one to the rational threshold \(5/3\) would be wrong. Non-strict bounds retain their rational threshold; they are not all rounded eagerly.

PreparedLraTheory::append_atom marks direct bounds on Int terms as integer. For compound polynomials its current sufficient condition is more conservative: the input is integer-sorted and the normalization scale is \(1\) or \(-1\). Other auxiliary variables use the real strict-bound encoding, even if a stronger analysis could prove some of them integer-valued.

Why the relaxation can still contain infinitesimals

The current invariant is that a completed integer assignment has no infinitesimal component. Intermediate relaxation assignments can have one, including on variables corresponding to Int terms.

For example, let \(P=2x+3y\) with integer \(x,y\). Normalizing by the leading coefficient \(2\) introduces \(s=x+\tfrac32y=P/2\). Consider \(P<0\):

1. The current fallback represents it as \(s\le-\delta\). The initial assignment \(x=y=s=0\) violates this bound.

2. If simplex pivots on \(x\), the row becomes \(x=s-\tfrac32y\). Moving \(s\) to \(-\delta\) gives \(x=-\delta\), \(y=0\). Every real constraint holds, but \(x\) is not integer-valued.

3. Patching can move \(s\) to \(-1\), giving \(x=-1\), \(y=0\). This satisfies the bound and makes both integer variables exact integers.

4. If patching does not resolve the assignment, branch-and-bound uses \(\lfloor-\delta\rfloor=-1\) and splits on \(x\le-1\) or \(x\ge0\). The first branch admits that same integer solution.

This is a possible tableau trace, not a promised preprocessing or pivot order.

The integer-value helpers require both an integral rational part and a zero infinitesimal part. In particular, \(\lfloor n-\delta\rfloor=n-1\) and \(\lceil n+\delta\rceil=n+1\) for integer \(n\). Treating \(n-\delta\) as having floor \(n\) would make branching repeatedly choose an already-satisfied bound. Dutertre–de Moura’s technical report §4.1, pp. 20–21, gives this delta-aware floor for branch-and-bound [20]. Patching targets exact integers; branch bounds have zero infinitesimal components. The cut generator skips a basic value with a nonzero infinitesimal, since its rational fractional-part formula does not cover that case. The regression map links the existing branching, patching and cut guards.

There is room to avoid introducing these infinitesimals. Since \(P\) is integer-valued, \(P<0\) is equivalent to \(P\le-1\), giving \(s\le-1/2\) without a delta. This must use the spacing of \(P/2\): rounding \(s\) as if it were an integer would incorrectly require \(s\le-1\) and exclude \(x=1,y=-1\), where \(s=-1/2\). The strengthened relaxation can still have fractional assignments; integer completion remains necessary. King’s thesis §4.3 describes the underlying integer tightening, including strict bounds obtained from negated SAT atoms [30]. Preserving this spacing during bound preparation is an open lead. Simply discarding a nonzero delta would change a strict inequality and is not a valid replacement.

Patching a feasible assignment

patch_integer_variables tries to find an integer model by moving nonbasic values without violating any bounds. It derives from Bjørner and Nachmanson §4.1, with a bounded candidate search and a global improvement criterion specific to Primo.

For a nonbasic variable \(y\), its freedom interval is the intersection of its own bounds with the intervals induced by every basic row containing \(y\). If \(x_b\) has coefficient \(a\ne0\) for \(y\), moving \(y\) by \(\Delta\) changes \(x_b\) by \(a\Delta\). To set \(x_b\) to an integer \(n\), the candidate move is

\[\Delta=\frac{n-\beta(x_b)}{a},\]

where \(\beta\) denotes the current assignment. A candidate is admissible only if the proposed value of \(y\) lies in its freedom interval. This preserves both row equations and feasibility; patching does not call simplex to repair an inadmissible move. A fixed variable has a singleton freedom interval and cannot move away from its fixed value.

Primo also considers directly moving a fractional nonbasic integer variable. Unlike the simplifying assumption in the paper, nonbasic variables here may sit inside their bounds, and even an integer variable’s bound may be fractional. For each fractional target, the search considers eight integers around its delta-aware floor \(m\): \(m,m+1,m-1,m+2,\ldots,m-3,m+4\), ordered by distance from the rational part. This is a heuristic window, not an exhaustive search of its feasible values.

The width is currently the hard-coded kTargetWindow = 4; the existing --lia-patch-limit controls accepted moves, not this width. A separate open lead proposes a window parameter and compares more selective candidates with MIP rounding and repair heuristics.

Every candidate is scored by the total number of required integer variables that would remain nonintegral. Only a strict reduction is accepted. Among inspected candidates with the same count, a smaller rational move wins; the scan stops early on finding a move that makes the whole assignment integral. Each accepted move decreases a nonnegative integer, so the sweep terminates even apart from its configured move budget. It can make an individual previously integral variable fractional, provided the total count improves. An integral assignment is still subject to the ordinary model checks.

Why a nearest move is insufficient

Use the paper’s Example 3:

\[y=x/2,\qquad z=x/3,\]

with \(3\le x\le10\), \(-3\le y\le4\), \(-5\le z\le12\), and initial values \((x,y,z)=(3,3/2,1)\). All three variables must be integers. The freedom interval of nonbasic \(x\) is \([3,8]\): \(y\le4\) supplies the tighter upper endpoint. Moving \(x\) to \(4\) fixes \(y\) but makes \(z=4/3\) fractional; the total remains one fractional variable, so Primo rejects that move. Moving \(x\) to \(6\) gives \((6,3,2)\) and reduces the count to zero. Considering only the floor and ceiling of \(y=3/2\) would miss that target.

The scoring index stores, for each nonbasic variable, the basic integer rows that contain it. Scoring adjusts a cached global count using only the moved variable and those affected rows. No pivot occurs during the sweep, so this incidence index stays valid. The scoring cost per candidate is proportional to the affected integer column, rather than all integer variables; generating candidates and calculating freedom intervals still have their own costs.

LiaPatchingStats exposes occurrence entries, candidates scored, affected rows inspected and the equivalent full-scan work. The public counters include :lia.patch-occurrence-entries, :lia.patch-candidates-scored, :lia.patch-affected-rows-inspected and :lia.patch-full-scan-equivalent. The patching tests cover the paper example, fixed and strict bounds, and comparison of indexed scoring with an independent full-scan definition.

Detecting integer-infeasible rows with GCDs

The equation \(2x-2y=1\) has no integer solution because its left side is always divisible by \(2\). More generally, for integer coefficients \(C_i\) and integer variables \(z_i\), every value of \(\sum_i C_i z_i\) is divisible by \(g=\gcd(C_1,\ldots,C_k)\). An equation \(\sum_i C_i z_i=R\) is therefore impossible when \(g\) does not divide \(R\).

This is the classical divisibility criterion for a linear Diophantine equation, a consequence of Bézout’s identity. It predates Bjørner and Nachmanson: Pugh’s Omega test, §2.1 of the expanded 1992 paper, already uses it when normalizing equalities. Griggio’s 2009 thesis, §2.6.1, Algorithm 2.6, step 4, applies the same criterion in an SMT equation solver. Bjørner and Nachmanson §4.3 is Primo’s reference for applying the test to tableau rows after fixed variables have been substituted, not for the origin of the criterion.

The read-only procedure gcd_inconsistent_row prepares each row as follows:

1. Rewrite \(x_b=\sum_j a_jx_j\) as \(x_b-\sum_j a_jx_j=0\).

2. Substitute variables fixed by equal lower and upper bounds with zero infinitesimal part, including \(x_b\) if it is fixed. The remaining equation is \(\sum_i c_i z_i=r\), with possibly rational coefficients and residual.

3. Require every remaining variable to belong to integer_vars. Otherwise skip the row: a noninteger auxiliary variable could absorb a fractional value. Pivoting can put such a variable on either side of the row.

4. Scale the coefficients and the residual together to integers \(C_i,R\) using primitive_integer_scale, and check whether their coefficient GCD divides \(R\).

If no variables remain after substitution, the row supplies no additional integer test; rational consistency has already been checked. Otherwise, failure of divisibility proves a conflict. Passing the test establishes only that the isolated equation has an integer solution when the remaining bounds are ignored. It does not establish consistency of the whole tableau.

For \(2x-2y=1\), normalization can represent \(s=x-y\) fixed to \(1/2\). Substitution leaves \(x-y=1/2\). Scaling the coefficients and residual by \(2\) gives \(2x-2y=1\); the coefficient GCD is \(2\), which does not divide \(1\). Scaling only the coefficients would destroy this argument.

The conflict depends on the bounds used to fix variables. Both bound reasons are collected for each fixed variable; row equations and the declared integer sorts are unconditional invariants of the prepared problem. The scan builds a membership bitmap and visits basic rows with exact rational/GCD operations; numeric cost depends on coefficient size, not just row length.

The bounded-variable GCD extension is an open lead carried forward from the original register. It can reject an interval containing no admissible residue even when no variable is fixed. Primo does not implement that extension or a general Diophantine equation solver. The GCD regressions cover fractional normalization, bounded-but-unfixed rows, and noninteger auxiliary variables in both basic and nonbasic positions.

Excluding a fractional point with a Gomory cut

apply_gomory_cuts uses King’s thesis §4.4.3, Lemma 4.1, equation (4.9). This mixed cut requires the basic variable to be integer in every solution. It treats nonbasic variables as continuous, so their bounds may be fractional and they need not belong to integer_vars.

The helper find_eligible_row chooses the row from which to derive a cut. It takes the first eligible variable in the caller’s integer list: it must be basic, its current value must be fractional with zero infinitesimal part, and every nonbasic variable in its row must sit exactly at a lower or upper bound. A variable merely having a bound is insufficient. An ineligible row is skipped in its entirety. For a variable at both bounds, the lower bound is chosen.

Write the row as \(x_b=\sum_j a_jx_j\), let \(v=\beta(x_b)\), and define \(f=v-\lfloor v\rfloor\), so \(0<f<1\). Let \(b_j\) be the rational part of the bound occupied by \(x_j\). Subtracting the bound-site assignment gives

\[x_b-\lfloor v\rfloor=f+\sum_j a_j(x_j-b_j).\]

The left side must be an integer. Group the nonnegative contributions in the sum into \(P\), and write its nonpositive contributions as \(-N\), with \(P,N\ge0\). If \(P-N>0\), integrality forces \(P-N\ge1-f\), hence \(P\ge1-f\). Otherwise it forces \(P-N\le-f\), hence \(N\ge f\). In either case,

\[\frac{P}{1-f}+\frac{N}{f}\ge1.\]

This is the cut. In terms of the stored row coefficients, it is \(\sum_j C_j(x_j-b_j)\ge1\), with:

Occupied bound	Sign of \(a_j\)	\(C_j\)
Lower	Positive	\(a_j/(1-f)\)
Lower	Negative	\(-a_j/f\)
Upper	Positive	\(-a_j/f\)
Upper	Negative	\(a_j/(1-f)\)

The rational-bound reasoning also applies when a selected bound is strict: forgetting its infinitesimal gives a weaker bound. The row-selection requirement that the basic value has zero infinitesimal ensures that its \(v\) is the rational bound-site sum used above. It skips a basic value such as \(3-\delta\) entirely; computing a fractional part from its rational part would give zero and make the divisions invalid.

Turning the inequality into a row

Expanding the constants yields

\[\sum_j C_jx_j\ge1+\sum_j C_jb_j.\]

apply_one_cut adds a new basic variable \(c=\sum_j C_jx_j\) and asserts the right side as its lower bound, using the synthetic reason kDerivedBoundReason. Then it checks rational feasibility again. A conflict ends the cut phase; otherwise it searches for another eligible row until the cut budget is exhausted or no row qualifies. A false return means “no conflict found”, not “no changes made”.

Take \(x_b=2u+3w\), with \(u\) at lower bound \(0\) and \(w\) at lower bound \(1/2\). Only \(x_b\) is required to be integer. Its value is \(3/2\), so \(f=1/2\) and

\[4u+6(w-1/2)\ge1 \quad\Longleftrightarrow\quad4u+6w\ge4.\]

The current point \((u,w)=(0,1/2)\) gives \(3<4\) and is excluded. The feasible integer-\(x_b\) point \((0,2/3)\) gives equality and \(x_b=2\). For an upper-bound example, \(x_b=2u-3w\) with \(u=1/3\) at its lower bound and \(w=-1\) at its upper bound gives \(f=2/3\) and \(6u-9w\ge12\). It excludes the current value \(11\) and keeps \((u,w)=(1/3,-10/9)\), where \(x_b=4\) and the cut is tight.

The cut tests check both examples by rejecting the fractional point and retaining the integer point. They also cover a cut that proves infeasibility, a term inside its bounds, zero budget and a basic variable with nonzero infinitesimal. The end-to-end cut regression uses \(3x+5y=7\), \(x,y\ge0\): the real relaxation is feasible, but \(y=0\) or \(1\) requires a fractional \(x\), and \(y\ge2\) already exceeds \(7\). Cuts resolve it under a branch budget too small for branching alone.

Cuts live in the private tableau for one integer completion. They remain present while branching explores descendants, but are not retained for the next Boolean candidate. No backtrackable row-insertion mechanism is needed for this schedule. Primo does not use nonbasic integrality to strengthen King’s formula, the CAV 2024 cut-selection heuristics, or that paper’s temporary handling of large-coefficient cuts.

Branching and backtracking

branch_and_bound starts from a rationally feasible tableau. It scans integer_vars for the first nonintegral assignment \(v\) and splits on

\[x\le\lfloor v\rfloor\quad\lor\quad x\ge\lfloor v\rfloor+1.\]

Every integer satisfies one side, and the current fractional value satisfies neither. At \(v=7/3\), for example, the branches are \(x\le2\) and \(x\ge3\). Each side is asserted as an ordinary tableau bound and checked by simplex. A feasible side is searched further; a conflict closes that side. After both sides close, the search backtracks to the previous frame. It tries the lower side first and uses the caller’s variable order, without a nearest-fraction or activity heuristic.

The explicit stack stores checkpoints rather than tableau copies per node. On Sat, the tableau stays at the winning leaf, including the successful branch bounds, so the caller can extract the model. On Unsat or LimitReached, the procedure removes its speculative bounds. With the default sparse simplex, popping restores bounds rather than the previous assignment and basis. The optional SOI path also trails assignments and pivots; see LRA backtracking. Callers should rely on the bound-restoration contract, not require identical internal tableau states.

The node counter increments when a new split is created, not for every simplex pivot or every attempted side. Integrality is checked before the limit, so an already integral assignment succeeds even with a zero node budget. The search stack grows with depth; the node cap bounds the number of splits in this call but is not a wall-clock or bit-complexity bound on the intervening exact arithmetic.

Explaining integer conflicts to SAT

The coarse conflict clause contains the blocking literal of every arithmetic atom used in the current candidate. If their conjunction is integer-infeasible, its negation is a valid clause. A smaller clause can exclude more Boolean candidates, so Primo normally attempts to use the integer derivation’s antecedents instead.

LiaExplanation stores literals already signed for the outgoing clause, following the tableau’s blocking-literal convention. It drops the synthetic literal 0 used for cuts and split bounds. Dropping it is justified by different arguments:

• A GCD conflict includes both reasons fixing each substituted variable.

• A cut includes the reasons for the occupied bounds used in its derivation. They are recorded when the cut is added, even if that cut does not immediately cause a conflict. A later cut or branch conflict may depend on it.

• A split is an integer tautology. If assumptions \(A\) refute \(x\le n\) and assumptions \(B\) refute \(x\ge n+1\), then \(A\land B\) is impossible because those cases cover all integers. After both sides close, their antecedents suffice without mentioning either temporary split bound.

For example, let \(p\) mean the normalized bound \(x\ge1/2\) and \(q\) mean \(x\le1/2\), with integer \(x\). These can arise from 2*x >= 1 and 2*x <= 1. The lower branch \(x\le0\) conflicts with \(p\); the upper branch \(x\ge1\) conflicts with \(q\). Combining the closed sides yields \(\neg p\lor\neg q\). Keeping only the first conflict and dropping its branch assumption would incorrectly yield \(\neg p\). The implementation emits the accumulated clause only after integer infeasibility, never after a model or a resource limit.

The explanation can contain reasons from cuts or closed branches unnecessary to the final proof. Such extra disjuncts weaken a valid clause; they do not invalidate it. This is conservative explanation collection, not minimal-core extraction or a replayable external proof certificate.

generalized_lia_lemma checks that the explanation is nonempty and that each literal occurs in the coarse clause. Otherwise it falls back to the coarse clause. This catches foreign or synthetic literals and ensures that the chosen clause blocks the candidate. Containment alone does not prove theory validity: an arbitrary subset of a valid clause can be invalid. Soundness still depends on the GCD, cut and exhaustive-branch arguments above. The explanation regressions exercise antecedent retention, synthetic-reason removal and collection across stages.

The counters :lia.generalized-lemmas, :lia.generalized-lemma-literals, :lia.coarse-lemma-literals and :lia.generalization-fallbacks describe the clauses emitted. A smaller clause can change the SAT search substantially; it is not by itself evidence of a performance improvement.

Budgets and incomplete cases

The integer options are shared by the pure and combined routes:

Option	Default	Meaning per integer completion
--lia-patch-limit	100	Maximum accepted patch moves; zero disables patching.
--lia-gomory-cut-limit	100	Maximum cut-and-recheck iterations; zero disables cuts. Exhaustion falls through to branching.
--lia-branch-limit	100000	Maximum new split nodes. Exhaustion before finding a model or refuting the tree returns a resource-limit result.
--no-lia-conflict-generalization	Absent	Disables the default attempt to replace coarse clauses with accumulated explanations.

These are finite operational limits, not empirically optimal settings. Both routes report typed ResourceLimit to the shared driver, producing unknown with the diagnostic integer branch-and-bound node limit. An unfinished search must not become unsat. Cancellation and the aggregate theory-conflict budget remain SMT-driver outcomes, independent of internal failed integer branches.

Consider unbounded integers \(x,y\) with \(2\le4x+4y\le3\). No multiple of four lies in that interval, yet the relaxation admits \(x+y=1/2\). The normalized auxiliary variable \(s=x+y\) is bounded, not fixed, so the current GCD check does not refute the interval. With unbounded nonbasic terms there is no eligible initial Gomory row. Patching cannot produce an integer model, and branching can keep translating the fractional assignment along the unbounded direction. The node-limit regression preserves this incomplete case. Adding GCD checks and cuts before DFS does not supply a completeness proof.

Dillig, Dillig and Aiken’s Cuts from proofs [16] provides a different branching rule based on integer-infeasible intersections. Its §3.3 termination argument uses satisfiability-preserving finite variable bounds and bounded split coefficients; it is not a guarantee for arbitrary unbounded cut generation. The paper overview derives the split for the example above and identifies the mechanisms missing from Primo.

Bromberger’s thesis, Chapter 6, addresses precisely the difference between bounded row expressions and bounded variables. Its Double-Bounded reduction and Mixed-Echelon-Hermite transformation provide a route to a finite integer search while preserving solutions through a change of coordinates. They are not implemented here. The thesis reading guide works through this example in coordinates \(u=x+y\), \(v=y\) and identifies the remaining implementation obligations.

The cube test, extended bounded-variable GCD reasoning, general Diophantine or Hermite-normal-form reasoning, cuts within branch nodes, and CDCL-visible integer splits remain outside the implementation. In particular, cube tests attempt to establish feasibility by solving a strengthened relaxation; failure of that test is not an integer-infeasibility proof. The cube-test explanation derives its strengthening, rounding guarantee and equality limitation. The earlier thesis note and integer open leads retain the separate investigations and their prerequisites.

QF_LIRA, mixing declared Int and Real variables, is not admitted. The stage APIs already take an integer subset, and fractional auxiliary variables exercise some mixed-tableau cases. That does not establish end-to-end QF_LIRA support: contextual numeral typing, coercions such as to_real, frontend admission and combined model construction still need design and validation.

Models, regression coverage and retained evidence

An integer result requires every variable in integer_vars to have a zero infinitesimal part and an integral rational part. Both routes export the winning values through LiaTheoryComponent to assemble_component_model. The shared assembler restores preprocessing conversions and completes declared Boolean constants even when rewriting removed their last occurrence. The driver supplies assignments for otherwise unowned Boolean constants that remain in the SAT abstraction. Combined models must additionally agree with EUF on evaluated function arguments and shared values; see model construction.

Obligation	Existing regression coverage
Find a model, close both sides, respect the budget, handle \(n-\delta\)	Branch-and-bound tests
Guard every free row variable before using integrality	GCD tests
Exclude fractional vertices while retaining legal integer points	Gomory tests
Preserve feasibility and score all affected integer variables	Patching tests
Keep antecedents of cuts used by later conflicts	Explanation tests
Strict polarity, normalization, extensions, model completion and stage controls	QF_LIA tests
Integer completion within equality/model combination	QF_UFLIA tests

Tests of hand-built tableaux exercise algorithm preconditions; whole-solver tests exercise admission, lowering and route integration. Fuzzing must cover both generated inputs and mutations of real formulas. Historical failures involved large coefficients and repeated proportional polynomials whose nearby thresholds shared a fractional auxiliary variable. Small-coefficient generator campaigns missed them, and merely increasing coefficient width also missed the original failure in a recorded probe. The lasting requirement is structural diversity, including pivoted auxiliary variables and original input model validation; see the correctness guide.

The section preservation map accounts for the original chapter, including repaired bugs, competing designs, experiment losses and incomplete gates. Those records remain attached to their measured revisions in the development history and run log. For example, the August patching comparison reports gains and losses, and the generalization comparison records a severe regression on one rings instance. Neither fewer fractional values nor shorter lemmas guarantees a faster subsequent search.

Historical solved counts exclude clean unknown results and timeout rows, even if an answer was printed before termination. This chapter documents the current mechanism; it does not rerun those campaigns or promote their measurements to results for the current source revision.

Sources and implementation status

The local paper-to-code checklist is the stage order, guards, derivations, state contracts and regression obligations above. The primary sections used for this chapter are identified in the bibliography; the table records the specific sections and their implementation status.

Source	Implemented subset and boundary
The Omega Test, expanded CACM 1992 version of the 1991 paper, §2.1 [35]; An Effective SMT Engine for Formal Verification, thesis, §2.6.1, Algorithm 2.6 [27]	Earlier uses of the classical GCD divisibility criterion. Added for attribution; Primo’s row-local check does not implement their equality-elimination procedures. The retained Griggio thesis note covers the broader equation handler.
Nikolaj Bjørner and Lev Nachmanson, Arithmetic Solving in Z3, CAV 2024, §§4.1, 4.3–4.4	Freedom-interval patching, basic row GCD consistency and integer splits. Primo adds a finite target window and a strictly improving global patch score, and branches inside a private theory search. The paper’s cubes, extended GCD and specialized cuts are not implemented.
Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic, thesis, §§4.3, 4.4.3, Lemma 4.1, equation (4.9) [30]	The mixed-cut derivation, represented by a fresh tableau row and bound. Nonbasic integrality is not used to strengthen the cut; no complete cutting-plane algorithm is claimed. Section 4.3 supplies integer-bound normalization for the open lead on scaled auxiliaries; Primo’s current preparation has the limitations described above.
Martin Bromberger, Decision Procedures for Linear Arithmetic, PhD thesis, Saarland, 2019, Chapters 4–6 and §§7.2.3–7.2.4	Cube tests, equality/bounded-direction analysis, bounding transformations and the separation of preparation from per-node work. These supply comparisons and concrete further work; Primo does not implement that complete combination. See the reading guide.
Bruno Dutertre and Leonardo de Moura, Integrating Simplex with DPLL(T), SRI-CSL-06-01, §§2–3 and 4.1 [20]	The rational tableau, bound assertions and consistency checks explained in LRA, plus integer splitting with delta-aware floor in §4.1. Section 3.2.4 saves a successful assignment; Primo’s sparse mode retains the current assignment and basis when popping bounds. These implemented mechanisms do not establish completeness of Primo’s integer procedure.
Original Primo design: private integer completion and accumulated explanations	The owned tableau copy, internal DFS, cut lifetime and union of antecedents connect the cited arithmetic rules to Primo’s SAT and component interfaces. Defensive clause containment is not a substitute for those rules’ soundness.

The Griggio and Bromberger tableau engineering references remain mapped in LRA’s source table; they are not additional implemented integer stages.