Mikolás Janota

145 papers A* 11A 29B 9C 3Misc 2Journal 66Unranked 23

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Case Study: Saturations as Explicit Models in Equational Theories. CoRR Mikolás Janota, Michael Rawson, Stephan Schulz
2026	J	`jnl`	Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols. CoRR Stefan Ratschan, Anggha Nugraha, Mikolás Janota, Marek Danco
2026	J	`jnl`	LLM2SMT: Building an SMT Solver with Zero Human-Written Code. CoRR Mikolás Janota, Mirek Olsák
2026	J	`jnl`	MENTOR: Fixing introductory programming assignments with formula-based fault localization and LLM-driven program repair. J. Syst. Softw. Pedro Orvalho, Mikolás Janota, Vasco Manquinho
2026	J	`jnl`	Machine learning for quantifier selection in cvc5. Int. J. Approx. Reason. Jan Jakubuv, Mikolás Janota, Jelle Piepenbrock, Josef Urban
2026	J	`jnl`	Minimizing the weighted number of tardy jobs: data-driven heuristic for single-machine scheduling. Comput. Oper. Res. Nikolai Antonov, Premysl Sucha, Mikolás Janota, Jan Hula
2026	J	`jnl`	Neural approaches to SAT solving: Design choices and interpretability. Int. J. Approx. Reason. David Mojzísek, Jan Hula, Ziwei Li, Ziyu Zhou, Mikolás Janota
2026	J	`jnl`	Reintroducing the Second Player in EPR. CoRR Leroy Chew, Mikolás Janota, Miroslav Olsák, Martin Suda
2025	—	`conf`	Breaking Symmetries from a Set-Covering Perspective. CPAIOR (1) Michael Codish, Mikolás Janota
2025	J	`jnl`	Breaking Symmetries from a Set-Covering Perspective. CoRR Michael Codish, Mikolás Janota
2025	A*	`conf`	Breaking Symmetries in Quantified Graph Search: A Comparative Study. AAAI Mikolás Janota, Markus Kirchweger, Tomás Peitl, Stefan Szeider
2025	J	`jnl`	Breaking Symmetries in Quantified Graph Search: A Comparative Study. CoRR Mikolás Janota, Markus Kirchweger, Tomás Peitl, Stefan Szeider
2025	A	`conf`	Breaking Symmetries with Involutions. CP Michael Codish, Mikolás Janota
2025	J	`jnl`	Breaking Symmetries with Involutions. CoRR Michael Codish, Mikolás Janota
2025	A*	`conf`	Complete Symmetry Breaking for Finite Models. AAAI Marek Danco, Mikolás Janota, Michael Codish, João Jorge Araújo
2025	J	`jnl`	Complete Symmetry Breaking for Finite Models. CoRR Marek Danco, Mikolás Janota, Michael Codish, João Araújo
2025	A*	`conf`	Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization. AAAI Pedro Orvalho, Mikolás Janota, Vasco M. Manquinho
2025	J	`jnl`	Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization. CoRR Pedro Orvalho, Mikolás Janota, Vasco Manquinho
2025	J	`jnl`	Cube-based Isomorph-free Finite Model Finding. CoRR Choiwah Chow, Mikolás Janota, João Araújo
2025	J	`jnl`	Experimental Results for Vampire on the Equational Theories Project. CoRR Mikolás Janota
2025	J	`jnl`	First Experiments with Neural cvc5. CoRR Jelle Piepenbrock, Mikolás Janota, Jan Jakubuv
2025	J	`jnl`	From MBQI to Enumerative Instantiation and Back. CoRR Marek Danco, Petra Hozzová, Mikolás Janota
2025	J	`jnl`	Geometric Reasoning in the Embedding Space. CoRR Jan Hula, David Mojzísek, Jirí Janecek, David Herel, Mikolás Janota
2025	J	`jnl`	Geometric Reasoning in the Embedding Space. Mach. Learn. Knowl. Extr. David Mojzísek, Jan Hula, Jirí Janecek, David Herel, Mikolás Janota
2025	J	`jnl`	InvAASTCluster: On Applying Invariant-Based Program Clustering to Introductory Programming Assignments. J. Syst. Softw. Pedro Orvalho, Mikolás Janota, Vasco Manquinho
2025	J	`jnl`	Invariant neural architecture for learning term synthesis in instantiation proving. J. Symb. Comput. Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olsák, Tom Heskes, Mikolás Janota
2025	J	`jnl`	Minimizing the Weighted Number of Tardy Jobs: Data-Driven Heuristic for Single-Machine Scheduling. CoRR Nikolai Antonov, Premysl Sucha, Mikolás Janota, Jan Hula
2025	J	`jnl`	Model-Based Diagnosis with Multiple Observations: A Unified Approach for C Software and Boolean Circuits. CoRR Pedro Orvalho, Marta Kwiatkowska, Mikolás Janota, Vasco Manquinho
2025	J	`jnl`	Neural Approaches to SAT Solving: Design Choices and Interpretability. CoRR David Mojzísek, Jan Hula, Ziwei Li, Ziyu Zhou, Mikolás Janota
2025	—	`ed.`	Proceedings of the 10th International Workshop on Satisfiability Checking and Symbolic Computation (SC-Square 2025) Collocated with The 30th International Conference on Automated Deduction (CADE 2025), Stuttgart, Germany, August 2, 2025. SC-Square@CADE Madalina Erascu, Mikolás Janota
2025	J	`jnl`	Quantifier Instantiations: To Mimic or To Revolt? CoRR Jan Jakubuv, Mikolás Janota
2025	J	`jnl`	SAT-Based Techniques for Lexicographically Smallest Finite Models. CoRR Mikolás Janota, Choiwah Chow, João Araújo, Michael Codish, Petr Vojtechovský
2025	A	`conf`	SMT and Functional Equation Solving over the Reals: Challenges from the IMO. CADE Chad E. Brown, Karel Chvalovský, Mikolás Janota, Mirek Olsák, Stefan Ratschan
2025	J	`jnl`	SMT and Functional Equation Solving over the Reals: Challenges from the IMO. CoRR Chad E. Brown, Karel Chvalovský, Mikolás Janota, Mirek Olsák, Stefan Ratschan
2025	J	`jnl`	Towards Learning Infinite SMT Models (Work in Progress). CoRR Mikolás Janota, Bartosz Piotrowski, Karel Chvalovský
2024	—	`conf`	C-Pack of IPAs: A C90 Program Benchmark of Introductory Programming Assignments. APR Pedro Orvalho, Mikolás Janota, Vasco Manquinho
2024	J	`jnl`	CFaults: Model-Based Diagnosis for Fault Localization in C Programs with Multiple Test Cases. CoRR Pedro Orvalho, Mikolás Janota, Vasco Manquinho
2024	A	`conf`	Cube-Based Isomorph-Free Finite Model Finding. ECAI Choiwah Chow, Mikolás Janota, João Araújo
2024	—	`conf`	GitSEED: A Git-backed Automated Assessment Tool for Software Engineering and Programming Education. SIGCSE Virtual (1) Pedro Orvalho, Mikolás Janota, Vasco Manquinho
2024	J	`jnl`	GitSEED: A Git-backed Automated Assessment Tool for Software Engineering and Programming Education. CoRR Pedro Orvalho, Mikolás Janota, Vasco Manquinho
2024	A	`conf`	Machine Learning for Quantifier Selection in cvc5. ECAI Jan Jakubuv, Mikolás Janota, Jelle Piepenbrock, Josef Urban
2024	J	`jnl`	Machine Learning for Quantifier Selection in cvc5. CoRR Jan Jakubuv, Mikolás Janota, Jelle Piepenbrock, Josef Urban
2024	A*	`conf`	SAT-Based Techniques for Lexicographically Smallest Finite Models. AAAI Mikolás Janota, Choiwah Chow, João Araújo, Michael Codish, Petr Vojtechovský
2024	C	`conf`	Solving Hard Mizar Problems with Instantiation and Strategy Invention. CICM Jan Jakubuv, Mikolás Janota, Josef Urban
2024	J	`jnl`	Solving Hard Mizar Problems with Instantiation and Strategy Invention. CoRR Jan Jakubuv, Mikolás Janota, Josef Urban
2024	J	`jnl`	Symbolic Computation for All the Fun. CoRR Chad E. Brown, Mikolás Janota, Mirek Olsák
2024	A	`conf`	Understanding GNNs for Boolean Satisfiability through Approximation Algorithms. CIKM Jan Hula, David Mojzísek, Mikolás Janota
2024	J	`jnl`	Understanding GNNs for Boolean Satisfiability through Approximation Algorithms. CoRR Jan Hula, David Mojzísek, Mikolás Janota
2024	—	`conf`	cfaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases. FM (1) Pedro Orvalho, Mikolás Janota, Vasco M. Manquinho
2023	J	`jnl`	Computing generating sets of minimal size in finite algebras. J. Symb. Comput. Mikolás Janota, António Morgado, Petr Vojtechovský
2023	—	`conf`	Data-driven Single Machine Scheduling Minimizing Weighted Number of Tardy Jobs. EPIA (1) Nikolai Antonov, Premysl Sucha, Mikolás Janota
2023	—	`conf`	Fast Heuristic for Ricochet Robots. ICAART (1) Jan Hula, David Adamczyk, Mikolás Janota
2023	J	`jnl`	Graph Neural Networks For Mapping Variables Between Programs - Extended Version. CoRR Pedro Orvalho, Jelle Piepenbrock, Mikolás Janota, Vasco Manquinho
2023	A	`conf`	Graph Neural Networks for Mapping Variables Between Programs. ECAI Pedro Orvalho, Jelle Piepenbrock, Mikolás Janota, Vasco Manquinho
2023	J	`jnl`	Integrated lot-sizing and scheduling: Mitigation of uncertainty in demand and processing time by machine learning. Eng. Appl. Artif. Intell. Mohammad Rohaninejad, Mikolás Janota, Zdenek Hanzálek
2023	C	`conf`	Molecule Builder: Environment for Testing Reinforcement Learning Agents. IJCCI Petr Hyner, Jan Hula, Mikolás Janota
2023	—	`conf`	Selecting Quantifiers for Instantiation in SMT. SMT Jan Jakubuv, Mikolás Janota, Bartosz Piotrowski, Jelle Piepenbrock, Andrew Reynolds
2023	A	`conf`	Symmetries for Cube-And-Conquer in Finite Model Finding. CP João Araújo, Choiwah Chow, Mikolás Janota
2023	Misc	`conf`	Towards Learning Infinite SMT Models (Work in Progress). SYNASC Mikolás Janota, Bartosz Piotrowski, Karel Chvalovský
2022	—	`conf`	Abstract: Challenges and Solutions for Higher-Order SMT Proofs. SMT Chad E. Brown, Mikolás Janota, Cezary Kaliszyk
2022	J	`jnl`	Boosting Isomorphic Model Filtering with Invariants. CoRR João Araújo, Choiwah Chow, Mikolás Janota
2022	J	`jnl`	Boosting isomorphic model filtering with invariants. Constraints An Int. J. João Araújo, Choiwah Chow, Mikolás Janota
2022	J	`jnl`	C-Pack of IPAs: A C90 Program Benchmark of Introductory Programming Assignments. CoRR Pedro Orvalho, Mikolás Janota, Vasco Manquinho
2022	A	`conf`	Guiding an Automated Theorem Prover with Neural Rewriting. IJCAR Jelle Piepenbrock, Tom Heskes, Mikolás Janota, Josef Urban
2022	J	`jnl`	InvAASTCluster: On Applying Invariant-Based Program Clustering to Introductory Programming Assignments. CoRR Pedro Orvalho, Mikolás Janota, Vasco Manquinho
2022	—	`conf`	MultIPAs: applying program transformations to introductory programming assignments for data augmentation. ESEC/SIGSOFT FSE Pedro Orvalho, Mikolás Janota, Vasco Manquinho
2022	A	`conf`	SAT-Based Leximax Optimisation Algorithms. SAT Miguel Cabral, Mikolás Janota, Vasco Manquinho
2022	C	`conf`	Targeted Configuration of an SMT Solver. CICM Jan Hula, Jan Jakubuv, Mikolás Janota, Lukás Kubej
2022	J	`jnl`	TestSelector: Automatic Test Suite Selection for Student Projects - Extended Version. CoRR Filipe Marques, António Morgado, José Fragoso Santos, Mikolás Janota
2022	B	`conf`	TestSelector: Automatic Test Suite Selection for Student Projects. RV Filipe Marques, António Morgado, José Fragoso Santos, Mikolás Janota
2022	A	`conf`	Towards Learning Quantifier Instantiation in SMT. SAT Mikolás Janota, Jelle Piepenbrock, Bartosz Piotrowski
2021	—	`conf`	Characteristic Subsets of SMT-LIB Benchmarks. SMT Jan Jakubuv, Mikolás Janota, Andrew Reynolds
2021	B	`conf`	Fair and Adventurous Enumeration of Quantifier Instantiations. FMCAD Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
2021	J	`jnl`	Fair and Adventurous Enumeration of Quantifier Instantiations. CoRR Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
2021	A	`conf`	Filtering Isomorphic Models by Invariants (Short Paper). CP João Araújo, Choiwah Chow, Mikolás Janota
2021	—	`conf`	First-Order Instantiation using Discriminating Terms. SMT Chad E. Brown, Mikolás Janota
2021	B	`conf`	Graph Neural Networks for Scheduling of SMT Solvers. ICTAI Jan Hula, David Mojzísek, Mikolás Janota
2021	J	`jnl`	Learning Equational Theorem Proving. CoRR Jelle Piepenbrock, Tom Heskes, Mikolás Janota, Josef Urban
2021	—	`ch.`	Quantified Boolean Formulas. Handbook of Satisfiability Olaf Beyersdorff, Mikolás Janota, Florian Lonsing, Martina Seidl
2021	A	`conf`	The Seesaw Algorithm: Function Optimization Using Implicit Hitting Sets. CP Mikolás Janota, António Morgado, José Fragoso Santos, Vasco Manquinho
2020	A	`conf`	SAT-Based Encodings for Optimal Decision Trees with Explicit Paths. SAT Mikolás Janota, António Morgado
2019	J	`jnl`	New Resolution-Based QBF Calculi and Their Proof Complexity. ACM Trans. Comput. Theory Olaf Beyersdorff, Leroy Chew, Mikolás Janota
2019	—	`conf`	On Unordered BDDs and Quantified Boolean Formulas. EPIA (2) Mikolás Janota
2019	J	`jnl`	PrideMM: A Solver for Relaxed Memory Models. CoRR Simon Cooksey, Sarah Harris, Mark Batty, Radu Grigore, Mikolás Janota
2019	—	`conf`	PrideMM: Second Order Model Checking for Memory Consistency Models. FM Workshops (2) Simon Cooksey, Sarah Harris, Mark Batty, Radu Grigore, Mikolás Janota
2019	A	`ed.`	Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings SAT Mikolás Janota, Inês Lynce
2018	A	`conf`	Circuit-Based Search Space Pruning in QBF. SAT Mikolás Janota
2018	A*	`conf`	Towards Generalization in QBF Solving via Machine Learning. AAAI Mikolás Janota
2017	Misc	`conf`	An Achilles' Heel of Term-Resolution. EPIA Mikolás Janota, João Marques-Silva
2017	J	`jnl`	An Achilles' Heel of Term-Resolution. CoRR Mikolás Janota
2017	J	`jnl`	Minimal sets on propositional formulae. Problems and reductions. Artif. Intell. João Marques-Silva, Mikolás Janota, Carlos Mencía
2017	—	`conf`	On Minimal Corrections in ASP. RCRA@AI*IA Mikolás Janota, João Marques-Silva
2017	—	`conf`	On the Quest for an Acyclic Graph. RCRA@AI*IA Mikolás Janota, Radu Grigore, Vasco Manquinho
2017	J	`jnl`	QFUN: Towards Machine Learning in QBF. CoRR Mikolás Janota
2016	A	`conf`	On Incremental Core-Guided MaxSAT Solving. CP Xujie Si, Xin Zhang, Vasco Manquinho, Mikolás Janota, Alexey Ignatiev, Mayur Naik
2016	—	`conf`	On Intervals and Bounds in Bit-vector Arithmetic. SMT@IJCAR Mikolás Janota, Christoph M. Wintersteiger
2016	A	`conf`	On Q-Resolution and CDCL QBF Solving. SAT Mikolás Janota
2016	J	`jnl`	On the query complexity of selecting minimal sets for monotone predicates. Artif. Intell. Mikolás Janota, João Marques-Silva
2016	J	`jnl`	Quantified maximum satisfiability. Constraints An Int. J. Alexey Ignatiev, Mikolás Janota, João Marques-Silva
2016	J	`jnl`	Solving QBF with counterexample guided refinement. Artif. Intell. Mikolás Janota, William Klieber, João Marques-Silva, Edmund M. Clarke
2015	J	`jnl`	Algorithms for computing backbones of propositional formulae. AI Commun. Mikolás Janota, Inês Lynce, João Marques-Silva
2015	A*	`conf`	Efficient Model Based Diagnosis with Maximum Satisfiability. IJCAI João Marques-Silva, Mikolás Janota, Alexey Ignatiev, António Morgado
2015	J	`jnl`	Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci. Mikolás Janota, João Marques-Silva
2015	A	`conf`	Exploiting Resolution-Based Representations for MaxSAT Solving. SAT Miguel Neves, Ruben Martins, Mikolás Janota, Inês Lynce, Vasco Manquinho
2015	J	`jnl`	Exploiting Resolution-based Representations for MaxSAT Solving. CoRR Miguel Neves, Ruben Martins, Mikolás Janota, Inês Lynce, Vasco Manquinho
2015	—	`conf`	On Conflicts and Strategies in QBF. LPAR (short papers) Nikolaj S. Bjørner, Mikolás Janota, William Klieber
2015	—	`conf`	Playing with Quantified Satisfaction. LPAR (short papers) Nikolaj S. Bjørner, Mikolás Janota
2015	A	`conf`	Proof Complexity of Resolution-based QBF Calculi. STACS Olaf Beyersdorff, Leroy Chew, Mikolás Janota
2015	A*	`conf`	Solving QBF by Clause Selection. IJCAI Mikolás Janota, João Marques-Silva
2014	J	`jnl`	Algorithms for computing minimal equivalent subformulas. Artif. Intell. Anton Belov, Mikolás Janota, Inês Lynce, João Marques-Silva
2014	J	`jnl`	Computing Minimal Sets on Propositional Formulae I: Problems & Reductions. CoRR João Marques-Silva, Mikolás Janota
2014	J	`jnl`	On Minimal Corrections in ASP. CoRR Mikolás Janota, João Marques-Silva
2014	—	`conf`	On lazy and eager interactive reconfiguration. VaMoS Mikolás Janota, Goetz Botterweck, João Marques-Silva
2014	J	`jnl`	On the Query Complexity of Selecting Few Minimal Sets. Electron. Colloquium Comput. Complex. João Marques-Silva, Mikolás Janota
2014	A*	`conf`	Towards efficient optimization in package management systems. ICSE Alexey Ignatiev, Mikolás Janota, João Marques-Silva
2013	A*	`conf`	Minimal Sets over Monotone Predicates in Boolean Formulae. CAV João Marques-Silva, Mikolás Janota, Anton Belov
2013	A*	`conf`	On Computing Minimal Correction Subsets. IJCAI João Marques-Silva, Federico Heras, Mikolás Janota, Alessandro Previti, Anton Belov
2013	A	`conf`	On Propositional QBF Expansions and Q-Resolution. SAT Mikolás Janota, João Marques-Silva
2013	J	`jnl`	On Propositional QBF Expansions and Q-Resolution. Electron. Colloquium Comput. Complex. Mikolás Janota, João Marques-Silva
2013	B	`conf`	On QBF Proofs and Preprocessing. LPAR Mikolás Janota, Radu Grigore, João Marques-Silva
2013	J	`jnl`	On QBF Proofs and Preprocessing. CoRR Mikolás Janota, Radu Grigore, João Marques-Silva
2013	A	`conf`	Quantified Maximum Satisfiability: - A Core-Guided Approach. SAT Alexey Ignatiev, Mikolás Janota, João Marques-Silva
2013	A	`conf`	Solving QBF with Free Variables. CP William Klieber, Mikolás Janota, João Marques-Silva, Edmund M. Clarke
2012	A	`conf`	On Computing Minimal Equivalent Subformulas. CP Anton Belov, Mikolás Janota, Inês Lynce, João Marques-Silva
2012	A*	`conf`	On Unit-Refutation Complete Formulae with Existentially Quantified Variables. KR Lucas Bordeaux, Mikolás Janota, João Marques-Silva, Pierre Marquis
2012	J	`jnl`	PackUp: Tools for Package Upgradability Solving. J. Satisf. Boolean Model. Comput. Mikolás Janota, Inês Lynce, Vasco Manquinho, João Marques-Silva
2012	A	`conf`	QBf-based boolean function bi-decomposition. DATE Huan Chen, Mikolás Janota, João Marques-Silva
2012	A	`conf`	Solving QBF with Counterexample Guided Refinement. SAT Mikolás Janota, William Klieber, João Marques-Silva, Edmund M. Clarke
2011	A	`conf`	Abstraction-Based Algorithm for 2QBF. SAT Mikolás Janota, João Marques-Silva
2011	A	`conf`	On Deciding MUS Membership with QBF. CP Mikolás Janota, João Marques-Silva
2011	J	`jnl`	QBF-Based Boolean Function Bi-Decomposition CoRR Huan Chen, Mikolás Janota, João Marques-Silva
2011	B	`conf`	cmMUS: A Tool for Circumscription-Based MUS Membership Testing. LPNMR Mikolás Janota, João Marques-Silva
2010	J	`jnl`	Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription CoRR Mikolás Janota, João Marques-Silva, Radu Grigore
2010	B	`conf`	Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription. JELIA Mikolás Janota, Radu Grigore, João Marques-Silva
2010	B	`conf`	How to Complete an Interactive Configuration Process? SOFSEM Mikolás Janota, Goetz Botterweck, Radu Grigore, João Marques-Silva
2010	A	`conf`	On Computing Backbones of Propositional Theories. ECAI João Marques-Silva, Mikolás Janota, Inês Lynce
2009	—	`conf`	A Design of a Configurable Feature Model Configurator. VaMoS Goetz Botterweck, Mikolás Janota, Denny Schneeweiss
2009	J	`jnl`	Algorithms for finding dispensable variables CoRR Mikolás Janota, João Marques-Silva, Radu Grigore
2009	—	`conf`	CLOPS: A DSL for Command Line Options. DSL Mikolás Janota, Fintan Fairmichael, Viliam Holub, Radu Grigore, Julien Charles, Dermot Cochran, Joseph R. Kiniry
2009	J	`jnl`	How to Complete an Interactive Configuration Process? CoRR Mikolás Janota, Goetz Botterweck, Radu Grigore, João Marques-Silva
2008	—	`conf`	Do SAT Solvers Make Good Configurators? SPLC (2) Mikolás Janota
2008	B	`conf`	Formal Approach to Integrating Feature and Architecture Models. FASE Mikolás Janota, Goetz Botterweck
2008	A	`conf`	Model Construction with External Constraints: An Interactive Journey from Semantics to Syntax. MoDELS Mikolás Janota, Victoria Kuzina, Andrzej Wasowski
2007	—	`conf`	Reachability analysis for annotated code. SAVCBS Mikolás Janota, Radu Grigore, Michal Moskal
2007	B	`conf`	Reasoning about Feature Models in Higher-Order Logic. SPLC Mikolás Janota, Joseph Kiniry