150 citations · 275 across the 41 of their papers we have counts for
6 papers · 1 filter
Quantifier Instantiations: To Mimic or To Revolt?
Jan Jakubův, Mikoláš Janota
Quantified formulas pose a significant challenge for Satisfiability Modulo Theories (SMT) solvers due to their inherent undecidability. Existing instantiation techniques, such as e…
Machine Learning for Quantifier Selection in cvc5
Jan Jakubův, Mikoláš Janota, Jelle Piepenbrock +1
In this work we considerably improve the state-of-the-art SMT solving on first-order quantified problems by efficient machine learning guidance of quantifier selection. Quantifiers…
Solving Hard Mizar Problems with Instantiation and Strategy Invention
Jan Jakubův, Mikoláš Janota, Josef Urban
In this work, we prove over 3000 previously ATP-unproved Mizar/MPTP problems by using several ATP and AI methods, raising the number of ATP-solved Mizar problems from 75\% to above…
Fair and Adventurous Enumeration of Quantifier Instantiations
Mikoláš Janota, Haniel Barbosa, Pascal Fontaine +1
SMT solvers generally tackle quantifiers by instantiating their variables with tuples of terms from the ground part of the formula. Recent enumerative approaches for quantifier ins…
Exploiting Resolution-based Representations for MaxSAT Solving
Miguel Neves, Ruben Martins, Mikoláš Janota +2
Most recent MaxSAT algorithms rely on a succession of calls to a SAT solver in order to find an optimal solution. In particular, several algorithms take advantage of the ability of…
Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription
Mikoláš Janota, Joao Marques-Silva, Radu Grigore
Circumscription is a representative example of a nonmonotonic reasoning inference technique. Circumscription has often been studied for first order theories, but its propositional…