| 2025 | AAAI | Complete Symmetry Breaking for Finite Models. | Marek Danco, Mikols Janota, Michael Codish, Joo Jorge Arajo |
| 2025 | AAAI | Breaking Symmetries in Quantified Graph Search: A Comparative Study. | Mikols Janota, Markus Kirchweger, Toms Peitl, Stefan Szeider |
| 2025 | AAAI | Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization. | Pedro Orvalho, Mikols Janota, Vasco M. Manquinho |
| 2025 | CADE | SMT and Functional Equation Solving over the Reals: Challenges from the IMO. | Chad E. Brown, Karel Chvalovsk, Mikols Janota, Mirek Olsk, Stefan Ratschan |
| 2025 | CP | Breaking Symmetries with Involutions. | Michael Codish, Mikols Janota |
| 2025 | CPAIOR | Breaking Symmetries from a Set-Covering Perspective. | Michael Codish, Mikols Janota |
| 2024 | AAAI | SAT-Based Techniques for Lexicographically Smallest Finite Models. | Mikols Janota, Choiwah Chow, Joo Arajo, Michael Codish, Petr Vojtechovsk |
| 2024 | CIKM | Understanding GNNs for Boolean Satisfiability through Approximation Algorithms. | Jan Hula, David Mojzsek, Mikols Janota |
| 2024 | ECAI | Cube-Based Isomorph-Free Finite Model Finding. | Choiwah Chow, Mikols Janota, Joo Arajo |
| 2024 | ECAI | Machine Learning for Quantifier Selection in cvc5. | Jan Jakubuv, Mikols Janota, Jelle Piepenbrock, Josef Urban |
| 2024 | FM | cfaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases. | Pedro Orvalho, Mikols Janota, Vasco M. Manquinho |
| 2024 | SIGCSE | GitSEED: A Git-backed Automated Assessment Tool for Software Engineering and Programming Education. | Pedro Orvalho, Mikols Janota, Vasco Manquinho |
| 2023 | CP | Symmetries for Cube-And-Conquer in Finite Model Finding. | Joo Arajo, Choiwah Chow, Mikols Janota |
| 2023 | ECAI | Graph Neural Networks for Mapping Variables Between Programs. | Pedro Orvalho, Jelle Piepenbrock, Mikols Janota, Vasco Manquinho |
| 2023 | EPIA | Data-driven Single Machine Scheduling Minimizing Weighted Number of Tardy Jobs. | Nikolai Antonov, Premysl Sucha, Mikols Janota |
| 2023 | ICAART | Fast Heuristic for Ricochet Robots. | Jan Hula, David Adamczyk, Mikols Janota |
| 2023 | IJCCI | Molecule Builder: Environment for Testing Reinforcement Learning Agents. | Petr Hyner, Jan Hula, Mikols Janota |
| 2023 | SYNASC | Towards Learning Infinite SMT Models (Work in Progress). | Mikols Janota, Bartosz Piotrowski, Karel Chvalovsk |
| 2022 | CADE | Guiding an Automated Theorem Prover with Neural Rewriting. | Jelle Piepenbrock, Tom Heskes, Mikols Janota, Josef Urban |
| 2022 | RV | TestSelector: Automatic Test Suite Selection for Student Projects. | Filipe Marques, Antnio Morgado, Jos Fragoso Santos, Mikols Janota |
| 2022 | SAT | SAT-Based Leximax Optimisation Algorithms. | Miguel Cabral, Mikols Janota, Vasco Manquinho |
| 2022 | SAT | Towards Learning Quantifier Instantiation in SMT. | Mikols Janota, Jelle Piepenbrock, Bartosz Piotrowski |
| 2021 | CP | Filtering Isomorphic Models by Invariants (Short Paper). | Joo Arajo, Choiwah Chow, Mikols Janota |
| 2021 | CP | The Seesaw Algorithm: Function Optimization Using Implicit Hitting Sets. | Mikols Janota, Antnio Morgado, Jos Fragoso Santos, Vasco Manquinho |
| 2021 | FMCAD | Fair and Adventurous Enumeration of Quantifier Instantiations. | Mikols Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds |
| 2021 | ICTAI | Graph Neural Networks for Scheduling of SMT Solvers. | Jan Hula, David Mojzsek, Mikols Janota |
| 2020 | SAT | SAT-Based Encodings for Optimal Decision Trees with Explicit Paths. | Mikols Janota, Antnio Morgado |
| 2019 | EPIA | On Unordered BDDs and Quantified Boolean Formulas. | Mikols Janota |
| 2019 | FM | PrideMM: Second Order Model Checking for Memory Consistency Models. | Simon Cooksey, Sarah Harris, Mark Batty, Radu Grigore, Mikols Janota |
| 2018 | AAAI | Towards Generalization in QBF Solving via Machine Learning. | Mikols Janota |
| 2018 | SAT | Circuit-Based Search Space Pruning in QBF. | Mikols Janota |
| 2017 | EPIA | An Achilles' Heel of Term-Resolution. | Mikols Janota, Joo Marques-Silva |
| 2016 | CADE | On Intervals and Bounds in Bit-vector Arithmetic. | Mikols Janota, Christoph M. Wintersteiger |
| 2016 | CP | On Incremental Core-Guided MaxSAT Solving. | Xujie Si, Xin Zhang, Vasco Manquinho, Mikols Janota, Alexey Ignatiev, Mayur Naik |
| 2016 | SAT | On Q-Resolution and CDCL QBF Solving. | Mikols Janota |
| 2015 | IJCAI | Solving QBF by Clause Selection. | Mikols Janota, Joo Marques-Silva |
| 2015 | IJCAI | Efficient Model Based Diagnosis with Maximum Satisfiability. | Joo Marques-Silva, Mikols Janota, Alexey Ignatiev, Antnio Morgado |
| 2015 | LPAR | Playing with Quantified Satisfaction. | Nikolaj S. Bjrner, Mikols Janota |
| 2015 | LPAR | On Conflicts and Strategies in QBF. | Nikolaj S. Bjrner, Mikols Janota, William Klieber |
| 2015 | STACS | Proof Complexity of Resolution-based QBF Calculi. | Olaf Beyersdorff, Leroy Chew, Mikols Janota |
| 2015 | SAT | Exploiting Resolution-Based Representations for MaxSAT Solving. | Miguel Neves, Ruben Martins, Mikols Janota, Ins Lynce, Vasco Manquinho |
| 2014 | ICSE | Towards efficient optimization in package management systems. | Alexey Ignatiev, Mikols Janota, Joo Marques-Silva |
| 2013 | CAV | Minimal Sets over Monotone Predicates in Boolean Formulae. | Joo Marques-Silva, Mikols Janota, Anton Belov |
| 2013 | CP | Solving QBF with Free Variables. | William Klieber, Mikols Janota, Joo Marques-Silva, Edmund M. Clarke |
| 2013 | IJCAI | On Computing Minimal Correction Subsets. | Joo Marques-Silva, Federico Heras, Mikols Janota, Alessandro Previti, Anton Belov |
| 2013 | LPAR | On QBF Proofs and Preprocessing. | Mikols Janota, Radu Grigore, Joo Marques-Silva |
| 2013 | SAT | Quantified Maximum Satisfiability: - A Core-Guided Approach. | Alexey Ignatiev, Mikols Janota, Joo Marques-Silva |
| 2013 | SAT | On Propositional QBF Expansions and Q-Resolution. | Mikols Janota, Joo Marques-Silva |
| 2012 | CP | On Computing Minimal Equivalent Subformulas. | Anton Belov, Mikols Janota, Ins Lynce, Joo Marques-Silva |
| 2012 | DATE | QBf-based boolean function bi-decomposition. | Huan Chen, Mikols Janota, Joo Marques-Silva |
| 2012 | KR | On Unit-Refutation Complete Formulae with Existentially Quantified Variables. | Lucas Bordeaux, Mikols Janota, Joo Marques-Silva, Pierre Marquis |
| 2012 | SAT | Solving QBF with Counterexample Guided Refinement. | Mikols Janota, William Klieber, Joo Marques-Silva, Edmund M. Clarke |
| 2011 | CP | On Deciding MUS Membership with QBF. | Mikols Janota, Joo Marques-Silva |
| 2011 | LPNMR | cmMUS: A Tool for Circumscription-Based MUS Membership Testing. | Mikols Janota, Joo Marques-Silva |
| 2011 | SAT | Abstraction-Based Algorithm for 2QBF. | Mikols Janota, Joo Marques-Silva |
| 2010 | ECAI | On Computing Backbones of Propositional Theories. | Joo Marques-Silva, Mikols Janota, Ins Lynce |
| 2010 | JELIA | Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription. | Mikols Janota, Radu Grigore, Joo Marques-Silva |
| 2010 | SOFSEM | How to Complete an Interactive Configuration Process? | Mikols Janota, Goetz Botterweck, Radu Grigore, Joo Marques-Silva |
| 2008 | FASE | Formal Approach to Integrating Feature and Architecture Models. | Mikols Janota, Goetz Botterweck |
| 2008 | MODELS | Model Construction with External Constraints: An Interactive Journey from Semantics to Syntax. | Mikols Janota, Victoria Kuzina, Andrzej Wasowski |
| 2008 | SPLC | Do SAT Solvers Make Good Configurators? | Mikols Janota |
| 2007 | SPLC | Reasoning about Feature Models in Higher-Order Logic. | Mikols Janota, Joseph Kiniry |