150 citations · 275 across the 41 of their papers we have counts for
46 papers
Proving at Scale for Universal Algebra
João Araújo, Jan Hůla, Mikoláš Janota +2
We introduce SemiBase, a project that computes and formally certifies finite identity bases for small semigroups. Deciding finite basability is undecidable for finite algebras and…
Compact Partial Symmetry Breaking for Graph Search Problems
Michael Codish, Mikoláš Janota, Peter J. Stuckey
Symmetry breaking in graph search problems remains challenging: complete symmetry breaking constraints are typically exponential in size, while partial approaches trade precision f…
Vibe-Coded and Tuned: A State-of-the-Art SMT Solver for QF-LRA
Mikoláš Janota, Jan Jakubův
This paper presents the SMT solver primo, which is fully vibe-coded and then parameter-tuned, achieving state-of-the-art results on linear real arithmetic (QF-LRA). The performance…
SAT-based Encodings for Optimal Decision Trees with Explicit Paths
Mikoláš Janota, António Morgado
Decision trees play an important role both in Machine Learning and Knowledge Representation. They are attractive due to their immediate interpretability. In the spirit of Occam's r…
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…