Reproduce “Revisiting Incremental Linearization for Nonlinear Integer Arithmetic” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Marek Dančo, Karel Chvalovský, Mikoláš Janota
qfn2l revisits counterexample-guided linearization for quantifier-free nonlinear integer arithmetic by replacing nonlinear monomials with fresh constants and refining a QF_LIA abstraction using sign-aware secant bounds for powers and mixed products. It solved 14,011 of 25,444 SMT-LIB instances overall, but was especially effective on a 1,100-instance number-theory family, solving 585 cases compared with 118 for Z3 and 171 for MathSAT5.
Key insights
- Secant lines over neighboring integer intervals provide tighter restrictions for powers than generic tangent or proportionality constraints, particularly for cubic and higher-degree terms.
- Treating complete monomials as single purified terms simplifies the abstraction, but it shifts congruence management from the underlying theory to explicit refinement rules.
- The approach is specialized: stronger polynomial reasoning can outperform general-purpose solvers on number-theoretic instances, while repeated model validation and many purified terms hurt performance on broad satisfiable families.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.