150 citations · 210 across the 3 of their papers we have counts for
18 papers
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…
Geometric Reasoning in the Embedding Space
Jan Hůla, David MojžÃÅ¡ek, JiÅà JaneÄek +2
In this contribution, we demonstrate that Graph Neural Networks and Transformers can learn to reason about geometric constraints. We train them to predict spatial position of point…
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…