3 papers
cs.LO2026
A Modern View on MCSat
Thomas Hader, Theo Jauschneg, Daniela Kaufmann +1
The Model Constructing Satisfiability (MCSat) approach has shown strong performance in solving complex SMT problems, in particular in algebraic SMT theories such as non-linear inte…
cs.LO2026
Generalizing CDCL with Graph Backtracking
Robin Coutelier, Thomas Hader, Laura Kovács
We present graph backtracking, a novel, fine-grained backtracking scheme for CDCL-based SAT solving, parametrized by a user-defined weight function. For conflict repair, we challen…
cs.LO2025
Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
Enrico Lipparini, Thomas Hader, Ahmed Irfan +1
The Model Constructing Satisfiability (MCSat) approach to the SMT problem extends the ideas of CDCL from the SAT level to the theory level. Like SAT, its search is driven by increm…