default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDMikolás Janota
Mikolas Janota – Mikoláš Janota
Person information
- unicode name: Mikoláš Janota
- affiliation: Czech Technical University, Prague, Czechia
- affiliation (former): University of Lisbon, Portugal
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2025
[j16]Jelle Piepenbrock
, Josef Urban, Konstantin Korovin, Miroslav Olsák, Tom Heskes, Mikolás Janota:
Invariant neural architecture for learning term synthesis in instantiation proving. J. Symb. Comput. 128: 102375 (2025)- 2024
- [c79]Mikolás Janota, Choiwah Chow, João Araújo, Michael Codish, Petr Vojtechovský:
SAT-Based Techniques for Lexicographically Smallest Finite Models. AAAI 2024: 8048-8056 - [c78]Jan Hula, David Mojzísek, Mikolás Janota:
Understanding GNNs for Boolean Satisfiability through Approximation Algorithms. CIKM 2024: 953-961 - [c77]Choiwah Chow, Mikolás Janota, João Araújo:
Cube-Based Isomorph-Free Finite Model Finding. ECAI 2024: 4100-4107 - [c76]Jan Jakubuv, Mikolás Janota, Jelle Piepenbrock, Josef Urban:
Machine Learning for Quantifier Selection in cvc5. ECAI 2024: 4336-4343 - [c75]Pedro Orvalho, Mikolás Janota, Vasco M. Manquinho:
cfaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases. FM (1) 2024: 463-481 - [c74]Pedro Orvalho, Mikolás Janota, Vasco Manquinho:
C-Pack of IPAs: A C90 Program Benchmark of Introductory Programming Assignments. APR 2024: 14-21 - [c73]Jelle Piepenbrock, Mikolas Janota, Josef Urban, Jan Jakubuv:
First Experiments with Neural cvc5. LPAR 2024: 264-277 - [c72]Jan Jakubuv, Mikolás Janota, Josef Urban:
Solving Hard Mizar Problems with Instantiation and Strategy Invention. CICM 2024: 315-333 - [c71]Chad E. Brown, Mikolas Janota, Mirek Olsák:
Symbolic Computation for All the Fun. PAAR+SC²@IJCAR 2024: 111-121 - [c70]Pedro Orvalho, Mikolás Janota, Vasco Manquinho:
GitSEED: A Git-backed Automated Assessment Tool for Software Engineering and Programming Education. SIGCSE Virtual (1) 2024 - [i33]Chad E. Brown, Mikolás Janota, Mirek Olsák:
Symbolic Computation for All the Fun. CoRR abs/2404.12048 (2024) - [i32]Jan Jakubuv, Mikolás Janota, Josef Urban:
Solving Hard Mizar Problems with Instantiation and Strategy Invention. CoRR abs/2406.17762 (2024) - [i31]Pedro Orvalho, Mikolás Janota, Vasco Manquinho:
CFaults: Model-Based Diagnosis for Fault Localization in C Programs with Multiple Test Cases. CoRR abs/2407.09337 (2024) - [i30]Jan Jakubuv, Mikolás Janota, Jelle Piepenbrock, Josef Urban:
Machine Learning for Quantifier Selection in cvc5. CoRR abs/2408.14338 (2024) - [i29]Jan Hula, David Mojzísek, Mikolás Janota:
Understanding GNNs for Boolean Satisfiability through Approximation Algorithms. CoRR abs/2408.15418 (2024) - [i28]Pedro Orvalho, Mikolás Janota, Vasco Manquinho:
GitSEED: A Git-backed Automated Assessment Tool for Software Engineering and Programming Education. CoRR abs/2409.07362 (2024) - 2023
- [j15]Mohammad Rohaninejad, Mikolás Janota, Zdenek Hanzálek:
Integrated lot-sizing and scheduling: Mitigation of uncertainty in demand and processing time by machine learning. Eng. Appl. Artif. Intell. 118: 105676 (2023) - [j14]Mikolás Janota, António Morgado, Petr Vojtechovský:
Computing generating sets of minimal size in finite algebras. J. Symb. Comput. 119: 50-63 (2023) - [c69]João Araújo, Choiwah Chow, Mikolás Janota:
Symmetries for Cube-And-Conquer in Finite Model Finding. CP 2023: 8:1-8:19 - [c68]Pedro Orvalho, Jelle Piepenbrock, Mikolás Janota, Vasco Manquinho:
Graph Neural Networks for Mapping Variables Between Programs. ECAI 2023: 1811-1818 - [c67]Nikolai Antonov, Premysl Sucha, Mikolás Janota:
Data-driven Single Machine Scheduling Minimizing Weighted Number of Tardy Jobs. EPIA (1) 2023: 483-494 - [c66]Mikolas Janota, Nina Narodytska:
The FMCAD 2023 Student Forum. FMCAD 2023: 1-2 - [c65]Jan Hula, David Adamczyk, Mikolás Janota:
Fast Heuristic for Ricochet Robots. ICAART (1) 2023: 71-79 - [c64]Petr Hyner, Jan Hula, Mikolás Janota:
Molecule Builder: Environment for Testing Reinforcement Learning Agents. IJCCI 2023: 450-458 - [c63]Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban:
A Mathematical Benchmark for Inductive Theorem Provers. LPAR 2023: 224-237 - [c62]Julian Parsert, Chad E. Brown, Mikolas Janota, Cezary Kaliszyk:
Experiments on Infinite Model Finding in SMT Solving. LPAR 2023: 317-328 - [c61]Jan Jakubuv, Mikolás Janota, Bartosz Piotrowski, Jelle Piepenbrock, Andrew Reynolds:
Selecting Quantifiers for Instantiation in SMT. SMT 2023: 71-77 - [c60]Mikolás Janota, Bartosz Piotrowski, Karel Chvalovský:
Towards Learning Infinite SMT Models (Work in Progress). SYNASC 2023: 82-85 - [i27]Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban:
A Mathematical Benchmark for Inductive Theorem Provers. CoRR abs/2304.02986 (2023) - [i26]Pedro Orvalho, Jelle Piepenbrock, Mikolás Janota, Vasco Manquinho:
Graph Neural Networks For Mapping Variables Between Programs - Extended Version. CoRR abs/2307.13014 (2023) - 2022
- [j13]João Araújo, Choiwah Chow, Mikolás Janota:
Boosting isomorphic model filtering with invariants. Constraints An Int. J. 27(3): 360-379 (2022) - [c59]Jelle Piepenbrock, Tom Heskes, Mikolás Janota, Josef Urban:
Guiding an Automated Theorem Prover with Neural Rewriting. IJCAR 2022: 597-617 - [c58]Jan Hula, Jan Jakubuv, Mikolás Janota, Lukás Kubej:
Targeted Configuration of an SMT Solver. CICM 2022: 256-271 - [c57]Filipe Marques, António Morgado, José Fragoso Santos, Mikolás Janota:
TestSelector: Automatic Test Suite Selection for Student Projects. RV 2022: 283-292 - [c56]Mikolás Janota, Jelle Piepenbrock, Bartosz Piotrowski:
Towards Learning Quantifier Instantiation in SMT. SAT 2022: 7:1-7:18 - [c55]Miguel Cabral, Mikolás Janota, Vasco Manquinho:
SAT-Based Leximax Optimisation Algorithms. SAT 2022: 29:1-29:19 - [c54]Pedro Orvalho, Mikolás Janota, Vasco Manquinho:
MultIPAs: applying program transformations to introductory programming assignments for data augmentation. ESEC/SIGSOFT FSE 2022: 1657-1661 - [c53]Chad E. Brown, Mikolás Janota, Cezary Kaliszyk:
Abstract: Challenges and Solutions for Higher-Order SMT Proofs. SMT 2022: 128 - [i25]João Araújo, Choiwah Chow, Mikolás Janota:
Boosting Isomorphic Model Filtering with Invariants. CoRR abs/2201.10516 (2022) - [i24]Pedro Orvalho, Mikolás Janota, Vasco Manquinho:
C-Pack of IPAs: A C90 Program Benchmark of Introductory Programming Assignments. CoRR abs/2206.08768 (2022) - [i23]Pedro Orvalho, Mikolás Janota, Vasco Manquinho:
InvAASTCluster: On Applying Invariant-Based Program Clustering to Introductory Programming Assignments. CoRR abs/2206.14175 (2022) - [i22]Filipe Marques, António Morgado, José Fragoso Santos, Mikolás Janota:
TestSelector: Automatic Test Suite Selection for Student Projects - Extended Version. CoRR abs/2207.09509 (2022) - [i21]Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olsák, Tom Heskes, Mikolas Janota:
Machine Learning Meets The Herbrand Universe. CoRR abs/2210.03590 (2022) - 2021
- [c52]João Araújo, Choiwah Chow, Mikolás Janota:
Filtering Isomorphic Models by Invariants (Short Paper). CP 2021: 4:1-4:9 - [c51]Mikolás Janota, António Morgado, José Fragoso Santos, Vasco Manquinho:
The Seesaw Algorithm: Function Optimization Using Implicit Hitting Sets. CP 2021: 31:1-31:16 - [c50]Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds:
Fair and Adventurous Enumeration of Quantifier Instantiations. FMCAD 2021: 256-260 - [c49]Jan Hula, David Mojzísek, Mikolás Janota:
Graph Neural Networks for Scheduling of SMT Solvers. ICTAI 2021: 447-451 - [c48]Chad E. Brown, Mikolás Janota:
First-Order Instantiation using Discriminating Terms. SMT 2021: 17-22 - [c47]Jan Jakubuv, Mikolás Janota, Andrew Reynolds:
Characteristic Subsets of SMT-LIB Benchmarks. SMT 2021: 53-63 - [p1]Olaf Beyersdorff, Mikolás Janota, Florian Lonsing, Martina Seidl:
Quantified Boolean Formulas. Handbook of Satisfiability 2021: 1177-1221 - [i20]Jelle Piepenbrock, Tom Heskes, Mikolás Janota, Josef Urban:
Learning Equational Theorem Proving. CoRR abs/2102.05547 (2021) - [i19]Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds:
Fair and Adventurous Enumeration of Quantifier Instantiations. CoRR abs/2105.13700 (2021) - 2020
- [c46]Mikolás Janota, António Morgado:
SAT-Based Encodings for Optimal Decision Trees with Explicit Paths. SAT 2020: 501-518
2010 – 2019
- 2019
- [j12]Olaf Beyersdorff, Leroy Chew, Mikolás Janota:
New Resolution-Based QBF Calculi and Their Proof Complexity. ACM Trans. Comput. Theory 11(4): 26:1-26:42 (2019) - [c45]Mikolás Janota:
On Unordered BDDs and Quantified Boolean Formulas. EPIA (2) 2019: 501-507 - [c44]Simon Cooksey, Sarah Harris, Mark Batty, Radu Grigore, Mikolás Janota:
PrideMM: Second Order Model Checking for Memory Consistency Models. FM Workshops (2) 2019: 507-525 - [e1]Mikolás Janota, Inês Lynce:
Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings. Lecture Notes in Computer Science 11628, Springer 2019, ISBN 978-3-030-24257-2 [contents] - [i18]Simon Cooksey, Sarah Harris, Mark Batty, Radu Grigore, Mikolás Janota:
PrideMM: A Solver for Relaxed Memory Models. CoRR abs/1901.00428 (2019) - 2018
- [c43]Mikolás Janota:
Towards Generalization in QBF Solving via Machine Learning. AAAI 2018: 6607-6614 - [c42]Mikolas Janota, Martin Suda:
Towards Smarter MACE-style Model Finders. LPAR 2018: 454-470 - [c41]Mikolás Janota:
Circuit-Based Search Space Pruning in QBF. SAT 2018: 187-198 - 2017
- [j11]João Marques-Silva, Mikolás Janota, Carlos Mencía:
Minimal sets on propositional formulae. Problems and reductions. Artif. Intell. 252: 22-50 (2017) - [c40]Mikolás Janota, Radu Grigore, Vasco Manquinho:
On the Quest for an Acyclic Graph. RCRA@AI*IA 2017: 33-44 - [c39]Mikolás Janota, João Marques-Silva:
On Minimal Corrections in ASP. RCRA@AI*IA 2017: 45-54 - [c38]Mikolás Janota, João Marques-Silva:
An Achilles' Heel of Term-Resolution. EPIA 2017: 670-680 - [i17]Mikolás Janota:
An Achilles' Heel of Term-Resolution. CoRR abs/1704.01071 (2017) - [i16]Mikolas Janota, Radu Grigore, Vasco Manquinho:
On the Quest for an Acyclic Graph. CoRR abs/1708.01745 (2017) - [i15]Mikolás Janota:
QFUN: Towards Machine Learning in QBF. CoRR abs/1710.02198 (2017) - 2016
- [j10]Mikolás Janota, João Marques-Silva:
On the query complexity of selecting minimal sets for monotone predicates. Artif. Intell. 233: 73-83 (2016) - [j9]Mikolás Janota, William Klieber, João Marques-Silva, Edmund M. Clarke:
Solving QBF with counterexample guided refinement. Artif. Intell. 234: 1-25 (2016) - [j8]Alexey Ignatiev, Mikolás Janota, João Marques-Silva:
Quantified maximum satisfiability. Constraints An Int. J. 21(2): 277-302 (2016) - [j7]Mikolas Janota:
On Exponential Lower Bounds for Partially Ordered Resolution. J. Satisf. Boolean Model. Comput. 10(1): 1-9 (2016) - [c37]Olaf Beyersdorff, Leroy Chew, Mikolas Janota:
Extension Variables in QBF Resolution. AAAI Workshop: Beyond NP 2016 - [c36]Mikolás Janota, Christoph M. Wintersteiger:
On Intervals and Bounds in Bit-vector Arithmetic. SMT@IJCAR 2016: 81-84 - [c35]Xujie Si, Xin Zhang, Vasco Manquinho, Mikolás Janota, Alexey Ignatiev, Mayur Naik:
On Incremental Core-Guided MaxSAT Solving. CP 2016: 473-482 - [c34]Mikolás Janota:
On Q-Resolution and CDCL QBF Solving. SAT 2016: 402-418 - [i14]Olaf Beyersdorff, Leroy Chew, Mikolas Janota:
Extension Variables in QBF Resolution. Electron. Colloquium Comput. Complex. TR16 (2016) - [i13]Mikolas Janota:
On Q-Resolution and CDCL QBF Solving. Electron. Colloquium Comput. Complex. TR16 (2016) - 2015
- [j6]Mikolás Janota, Inês Lynce, João Marques-Silva:
Algorithms for computing backbones of propositional formulae. AI Commun. 28(2): 161-177 (2015) - [j5]Mikolás Janota, João Marques-Silva:
Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci. 577: 25-42 (2015) - [c33]Valeriy Balabanov, Jie-Hong Roland Jiang, Mikolas Janota, Magdalena Widl:
Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs. AAAI 2015: 3694-3701 - [c32]Mikolás Janota, João Marques-Silva:
Solving QBF by Clause Selection. IJCAI 2015: 325-331 - [c31]João Marques-Silva, Mikolás Janota, Alexey Ignatiev, António Morgado:
Efficient Model Based Diagnosis with Maximum Satisfiability. IJCAI 2015: 1966-1972 - [c30]Nikolaj S. Bjørner, Mikolás Janota:
Playing with Quantified Satisfaction. LPAR (short papers) 2015: 15-27 - [c29]Nikolaj S. Bjørner, Mikolás Janota, William Klieber:
On Conflicts and Strategies in QBF. LPAR (short papers) 2015: 28-41 - [c28]Miguel Neves, Ruben Martins, Mikolás Janota, Inês Lynce, Vasco Manquinho:
Exploiting Resolution-Based Representations for MaxSAT Solving. SAT 2015: 272-286 - [c27]Olaf Beyersdorff, Leroy Chew, Mikolás Janota:
Proof Complexity of Resolution-based QBF Calculi. STACS 2015: 76-89 - [i12]Miguel Neves, Ruben Martins, Mikolás Janota, Inês Lynce, Vasco Manquinho:
Exploiting Resolution-based Representations for MaxSAT Solving. CoRR abs/1505.02405 (2015) - 2014
- [j4]Anton Belov, Mikolás Janota, Inês Lynce, João Marques-Silva:
Algorithms for computing minimal equivalent subformulas. Artif. Intell. 216: 309-326 (2014) - [j3]Mikolas Janota:
MiFuMax - a Literate MaxSAT Solver. J. Satisf. Boolean Model. Comput. 9(1): 83-88 (2014) - [j2]Mikolas Janota, Charles Jordan, Will Klieber, Florian Lonsing, Martina Seidl, Allen Van Gelder:
The QBFGallery 2014: The QBF Competition at the FLoC Olympic Games. J. Satisf. Boolean Model. Comput. 9(1): 187-206 (2014) - [c26]Alexey Ignatiev, Mikolás Janota, João Marques-Silva:
Towards efficient optimization in package management systems. ICSE 2014: 745-755 - [c25]Olaf Beyersdorff, Leroy Chew, Mikolas Janota:
On Unification of QBF Resolution-Based Calculi. MFCS (2) 2014: 81-93 - [c24]Mikolás Janota, Goetz Botterweck, João Marques-Silva:
On lazy and eager interactive reconfiguration. VaMoS 2014: 8:1-8:8 - [i11]João Marques-Silva, Mikolás Janota:
Computing Minimal Sets on Propositional Formulae I: Problems & Reductions. CoRR abs/1402.3011 (2014) - [i10]Mikolás Janota, João Marques-Silva:
On Minimal Corrections in ASP. CoRR abs/1406.7838 (2014) - [i9]Olaf Beyersdorff, Leroy Chew, Mikolas Janota:
Proof Complexity of Resolution-based QBF Calculi. Electron. Colloquium Comput. Complex. TR14 (2014) - [i8]Mikolas Janota, Leroy Chew, Olaf Beyersdorff:
On Unification of QBF Resolution-Based Calculi. Electron. Colloquium Comput. Complex. TR14 (2014) - [i7]João Marques-Silva, Mikolás Janota:
On the Query Complexity of Selecting Few Minimal Sets. Electron. Colloquium Comput. Complex. TR14 (2014) - 2013
- [c23]João Marques-Silva, Mikolás Janota, Anton Belov:
Minimal Sets over Monotone Predicates in Boolean Formulae. CAV 2013: 592-607 - [c22]William Klieber, Mikolás Janota, João Marques-Silva, Edmund M. Clarke:
Solving QBF with Free Variables. CP 2013: 415-431 - [c21]João Marques-Silva, Federico Heras, Mikolás Janota, Alessandro Previti, Anton Belov:
On Computing Minimal Correction Subsets. IJCAI 2013: 615-622 - [c20]Mikolás Janota, Radu Grigore, João Marques-Silva:
On QBF Proofs and Preprocessing. LPAR 2013: 473-489 - [c19]Mikolás Janota, João Marques-Silva:
On Propositional QBF Expansions and Q-Resolution. SAT 2013: 67-82 - [c18]Alexey Ignatiev, Mikolás Janota, João Marques-Silva:
Quantified Maximum Satisfiability: - A Core-Guided Approach. SAT 2013: 250-266 - [i6]Mikolás Janota, Radu Grigore, João Marques-Silva:
On QBF Proofs and Preprocessing. CoRR abs/1310.2491 (2013) - [i5]Mikolás Janota, João Marques-Silva:
On Propositional QBF Expansions and Q-Resolution. Electron. Colloquium Comput. Complex. TR13 (2013) - 2012
- [j1]Mikolás Janota, Inês Lynce, Vasco Manquinho, João Marques-Silva:
PackUp: Tools for Package Upgradability Solving. J. Satisf. Boolean Model. Comput. 8(1/2): 89-94 (2012) - [c17]Anton Belov, Mikolás Janota, Inês Lynce, João Marques-Silva:
On Computing Minimal Equivalent Subformulas. CP 2012: 158-174 - [c16]Huan Chen, Mikolás Janota, João Marques-Silva:
QBf-based boolean function bi-decomposition. DATE 2012: 816-819 - [c15]Lucas Bordeaux, Mikolás Janota, João Marques-Silva, Pierre Marquis:
On Unit-Refutation Complete Formulae with Existentially Quantified Variables. KR 2012 - [c14]Mikolás Janota, William Klieber, João Marques-Silva, Edmund M. Clarke:
Solving QBF with Counterexample Guided Refinement. SAT 2012: 114-128 - 2011
- [c13]Mikolás Janota, João Marques-Silva:
On Deciding MUS Membership with QBF. CP 2011: 414-428 - [c12]Mikolás Janota, João Marques-Silva:
cmMUS: A Tool for Circumscription-Based MUS Membership Testing. LPNMR 2011: 266-271 - [c11]Mikolás Janota, João Marques-Silva:
Abstraction-Based Algorithm for 2QBF. SAT 2011: 230-244 - [i4]Huan Chen, Mikolás Janota, João Marques-Silva:
QBF-Based Boolean Function Bi-Decomposition. CoRR abs/1112.2313 (2011) - 2010
- [c10]João Marques-Silva, Mikolás Janota, Inês Lynce:
On Computing Backbones of Propositional Theories. ECAI 2010: 15-20 - [c9]Mikolás Janota, Radu Grigore, João Marques-Silva:
Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription. JELIA 2010: 195-207 - [c8]Mikolás Janota, Goetz Botterweck, Radu Grigore, João Marques-Silva:
How to Complete an Interactive Configuration Process? SOFSEM 2010: 528-539 - [i3]Mikolás Janota, João Marques-Silva, Radu Grigore:
Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription. CoRR abs/1006.5896 (2010)
2000 – 2009
- 2009
- [c7]Mikolás Janota, Fintan Fairmichael, Viliam Holub, Radu Grigore, Julien Charles, Dermot Cochran, Joseph R. Kiniry:
CLOPS: A DSL for Command Line Options. DSL 2009: 187-210 - [c6]