3 papers
cs.LO2026
Revisiting Incremental Linearization for Nonlinear Integer Arithmetic
Marek Dančo, Karel Chvalovský, Mikoláš Janota
Incremental Linearization has previously been proposed for solving SMT problems over quantifier-free nonlinear integer arithmetic and has proven effective despite its conceptual si…
cs.LO2025
SMT and Functional Equation Solving over the Reals: Challenges from the IMO
Chad E. Brown, Karel Chvalovský, Mikoláš Janota +2
We use SMT technology to address a class of problems involving uninterpreted functions and nonlinear real arithmetic. In particular, we focus on problems commonly found in mathemat…
cs.LO2025
Towards Learning Infinite SMT Models (Work in Progress)
Mikoláš Janota, Bartosz Piotrowski, Karel Chvalovský
This short paper proposes to learn models of satisfiability modulo theories (SMT) formulas during solving. Specifically, we focus on infinite models for problems in the logic of li…