4 papers
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…
Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols
Stefan Ratschan, Anggha Nugraha, Mikoláš Janota +1
The combination of uninterpreted function symbols and universal quantification occurs in many applications of automated reasoning, for example, due to their ability to reason about…
From MBQI to Enumerative Instantiation and Back
Marek DanÄo, Petra Hozzová, Mikoláš Janota
This work investigates the relation between model-based quantifier instantiation (MBQI) and enumerative instantiation (EI) in Satisfiability Modulo Theories (SMT). MBQI operates at…
Complete Symmetry Breaking for Finite Models
Marek DanÄo, Mikoláš Janota, Michael Codish +1
This paper introduces a SAT-based technique that calculates a compact and complete symmetry-break for finite model finding, with the focus on structures with a single binary operat…