150 citations · 210 across the 8 of their papers we have counts for
14 papers · 1 filter
Solving QBF with Counterexample Guided Refinement
Mikoláš Janota, William Klieber, Joao Marques-Silva +1
We propose two novel approaches for using Counterexample-Guided Abstraction Refinement (CEGAR) in Quantified Boolean Formula (QBF) solvers. The first approach develops a recursive…
Solving QBF by Clause Selection
Mikoláš Janota, Joao Marques-Silva
Algorithms based on the enumeration of implicit hitting sets find a growing number of applications, which include maximum satisfiability and model based diagnosis, among others. Th…
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…
LLM2SMT: Building an SMT Solver with Zero Human-Written Code
Mikoláš Janota, Mirek Olšák
Whether LLMs can reason or write software is widely debated, but whether they can write software that itself reasons is largely unexplored. We present a case study in which an LLM…
Reintroducing the Second Player in EPR
Leroy Chew, Mikoláš Janota, Miroslav Olšák +1
In this work we investigate the computational complexity of the satisfiability problem of sub-fragments of the Bernays-Schoenfinkel class of first-order logic, also known as EPR (E…
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…