Home Page of Mikoláš Janota
 |
 work: Assistant Professor, IST, University of Lisbon, SAT Group previous: Microsoft Research, Cambridge, PPT Group Publications | Projects | Software | Links |
http://people.ciirc.cvut.cz/~janotmik
| 2024 |
|
Symbolic Computation for All the Fun
[preprint]
[pdf]
in Satisfiability Checking and Symbolic Computation, SC2 2024 |
|
Understanding GNNs for Boolean Satisfiability through Approximation Algorithms
[preprint]
in CIKM 2024 |
|
Machine Learning for Quantifier Selection in cvc5
[preprint]
in ECAI 2024 |
|
Cube-based Isomorph-free Finite Model Finding
[preprint]
in ECAI 2024 |
|
Solving Hard Mizar Problems with Instantiation and Strategy Invention
[arxiv]
in CICM 2024, Best Paper Award |
|
CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases
[arxiv]
[preprint]
in Formal Methods 2024 |
|
SAT-based Techniques for Lexicographically Smallest Finite Models
[doi]
[preprint]
[tool]
[data]
[slides]
[talk]
in AAAI 2024 |
|
First Experiments with Neural cvc5
[doi]
in LPAR 2024 |
| 2023 |
|
Graph Neural Networks For Mapping Variables Between Programs
[arXiv]
in ECAI 2023 |
|
Symmetries for Cube-and-conquer in Finite Model Finding
[doi]
[preprint]
[slides]
in CP 2023 |
|
Towards Learning Infinite SMT Models
[preprint]
[slides]
in SYNASC 2023 |
|
Data-driven Single Machine Scheduling Minimizing Weighted Number of Tardy Jobs
[preprint]
in EPIA 2023 |
|
Experiments on Infinite Model Finding in SMT Solving
[prepr]
[doi]
[examples]
in LPAR 2023 |
|
A Benchmark for Infinite Models in SMT
[prepr]
[data]
[slides]
[talk]
in AITP 2023 |
|
A Mathematical Benchmark for Inductive Theorem Provers
[preprint]
[doi]
in LPAR 2023 |
|
Computing Generating Sets of Minimal Size in Finite Algebras
[preprint]
[doi]
in Journal of Symbolic Computation |
| Fast Heuristic for Ricochet Robots
[pdf]
in ICAART-23 |
| Integrated lot-sizing and scheduling: Mitigation of uncertainty in demand and processing time by machine learning
[doi]
in Engineering Applications of Artificial Intelligence 2023 |
| 2022 |
|
Towards Learning Quantifier Instantiation in SMT
[preprint]
[doi]
in SAT 2022 |
|
Boosting Isomorphic Model Filtering with Invariants
[doi]
[arXiv]
in CONSTRAINTS |
|
Guiding an Automated Theorem Prover with Neural Rewriting
[preprint]
[doi]
in IJCAR 2022 |
|
TestSelector: Automatic Test Suite Selection for Student Projects
[doi]
[arXiv]
in International Conference on Runtime Verification |
|
SAT-based Leximax Optimisation Algorithms
[slides]
[preprint]
[doi]
in SAT 2022 |
|
Targeted Configuration of an SMT Solver
[doi]
[preprint]
in CICM 2022 |
|
Challenges and Solutions for Higher-Order SMT Proofs
[preprint]
in SMT 2022 |
| 2021 |
|
Fair and Adventurous Enumeration of Quantifier Instantiations
[doi]
[preprint]
[talk]
[slides]
in FMCAD 2021 |
|
The Seesaw Algorithm: Function Optimization using Implicit Hitting Sets
[preprint]
[talk]
[doi]
in CP 2021 |
|
Filtering Isomorphic Models by Invariants
[preprint]
[doi]
in CP 2021 |
|
Graph Neural Networks for Scheduling of SMT Solvers
[preprint]
in ICTAI 2021 |
|
Characteristic Subsets of SMT-LIB Benchmarks
[preprint]
in SMT 2021 |
|
First-Order Instantiation using Discriminating Terms
[preprint]
in SMT 2021 |
|
How to Approximate Leximax-optimal Solutions
[preprint]
in POS 2021 |
| 2020 |
|
SAT-based Encodings for Optimal Decision Trees with Explicit Paths
[ee]
[talk]
[preprint]
[tool]
in SAT 2020 |
| 2019 |
|
New Resolution-Based QBF Calculi and Their Proof Complexity
[ee]
[preprint]
in ACM Transactions on Computation Theory (TOCT) |
|
PrideMM: Second Order Model Checking for Memory Consistency Models
[slides]
[preprint]
in TAPAS '19 |
|
Machine Learning of Strategies in QBF Solving
[preprint]
[slides]
in RCRA '19 |
|
On Unordered BDDs and Quantified Boolean Formulas
[preprint]
[ee]
in EPIA '19 |
| 2018 |
|
Towards Smarter MACE-style Model Finders
[preprint]
[ee]
[slides]
[bib]
and in LPAR '18 |
|
QBF Solvers Submitted to QBF Competition 2018
[slides]
in QBF '18 |
|
Circuit-based Search Space Pruning in QBF
[ee]
[slides]
[preprint]
[github]
in SAT '18 |
|
Towards Generalization in QBF Solving via Machine Learning
[tool]
[ee]
[preprint]
in AAAI '18 |
| 2017 |
|
On the Quest for an Acyclic Graph
[preprint]
[slides]
[arXiv]
in RCRA '17 |
|
On Minimal Corrections in ASP
[preprint]
[slides]
in RCRA '17 |
|
Minimal sets on propositional formulae. Problems and reductions
[ee]
in Artificial Intelligence |
|
An Achilles' Heel of Term-Resolution
[ee]
[preprint]
in EPIA 17 |
| 2016 |
|
On Incremental Core-Guided MaxSAT Solving
[pdf] in CP 16 |
|
On Q-Resolution and CDCL QBF Solving
[pdf]
[slides]
[ee]
in SAT 16 [ee] |
|
Extension Variables in QBF Resolution
[eccc]
in Beyond NP Workshop |
|
Current Trends in QBF Solving
[slides]
invited talk at the Beyond NP Workshop |
|
Solving QBF with Counterexample Guided Refinement
[ee]
[bib]
in Journal of Artificial Intelligence (AI) |
|
On Intervals and Bounds in Bit-vector Arithmetic.
[ee] in SMT@IJCAR |
|
On the Query Complexity of Selecting Minimal Sets for Monotone Predicates
[ee]
in Journal of Artificial Intelligence (AI) |
| 2015 |
|
MiFuMax-a Literate MaxSAT Solver
[ee]
[tool]
in Journal on Satisfiability, Boolean Modeling and Computation (JSAT) |
|
Playing with Quantified Satisfaction
[ee]
[preprint]
[slides]
in LPAR-20 |
|
On Conflicts and Strategies in QBF
[ee]
[preprint]
[slides]
in LPAR-20 |
|
Solving QBF by Clause Selection
[ee]
[preprint]
[tool]
[bib]
in IJCAI '15 |
|
Efficient Model Based Diagnosis with Maximum Satisfiability
[ee]
in IJCAI '15 |
|
Quantified Maximum Satisfiability
[ee]
[bib]
in Constraints, An International Journal |
|
Expansion-based QBF Solving versus Q-Resolution
[ee]
[preprint]
[bib]
in Journal of Theoretical Computer Science (TCS) |
|
Exploiting Resolution-Based Representations for MaxSAT Solving
[ee]
in SAT '15 |
|
Proof Complexity of Resolution-based QBF Calculi
[ee]
[eccc]
[bib]
in STACS '15 |
|
Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs
in AAAI '15 |
| 2014 |
|
On Unification of QBF Resolution-Based Calculi
[preprint]
[slides]
[eccc]
[ee]
in Mathematical Foundations of Computer Science (MFCS '14). |
|
On Instantiation-Based Calculi for QBF
[slides]
in Invited talk at the QBF Workshop 2014. |
|
Towards efficient optimization in package management systems
[ee]
in International Conference on Software Engineering (ICSE '14) |
|
On lazy and eager interactive reconfiguration
[slides]
[ee]
in International Workshop on Variability Modelling of Software-Intensive Systems (VaMoS '14) |
|
Algorithms for Computing Backbones of Propositional Formulae
[preprint]
[ee] in Journal of AI Communications (AI-Com) |
|
Algorithms for computing minimal equivalent subformulas
[ee]
in Journal of Artificial Intelligence (AI) |
| 2013 |
|
On QBF Proofs and Preprocessing
[preprint]
[slides]
[arXiv]
[ee]
[blogpost]
[tools] Logic for Programming Artificial Intelligence and Reasoning (LPAR-19) |
|
Solving QBF with Free Variables
[preprint] 19th International Conference on Principles and Practice of Constraint Programming (CP'13) |
|
On Propositional QBF Expansions and Q-Resolution
[ee]
[preprint]
[slides]
[scripts]
16th International Conference on Theory and Applications of Satisfiability Testing (SAT '13) |
|
Quantified Maximum Satisfiability: A Core-Guided Approach
[preprint] 16th International Conference on Theory and Applications of Satisfiability Testing (SAT '13) |
|
On Computing Minimal Correction Subsets
[ee] IJCAI 2013 |
|
Minimal Sets over Monotone Predicates in Boolean Formulae
[preprint]
[ee]
International Conference on Computer Aided Verification (CAV '13) |
| 2012 |
|
On Computing Minimal Equivalent Subformulas
[ee]
[preprint]
18th International Conference on Principles and Practice of Constraint Programming (CP'12) |
|
Solving QBF with Counterexample Guided Refinement
[ee]
[preprint]
[slides]
[tool]
[bib]
The 15th International Conference on Theory and Applications of Satisfiability Testing (SAT '12) |
|
On Unit-Refutation Complete Formulae with Existentially Quantified Variables
[ee]
[preprint]
[slides]
International Conference on Principles of Knowledge Representation and Reasoning (KR), 2012 |
|
Experimental Analysis of Backbone Computation Algorithms
[pdf]
[ee]
[slides]
International Workshop on "Experimental Evaluation of Algorithms for solving problems with combinatorial explosion", RCRA |
|
On Checking of Skolem-based Models of QBF
[ee]
[slides]
International Workshop on "Experimental Evaluation of Algorithms for solving problems with combinatorial explosion", RCRA |
|
QBF-Based Boolean Function Bi-decomposition
[arXiv]
[ee]
Design, Automation & Test in Europe Conference & Exhibition (DATE), 2012 |
|
PackUp: Tools for Package Upgradability Solving
[ee]
[tool]
Journal on Satisfiability, Boolean Modeling and Computation, Volume 8, 2012 |
| 2011 |
|
On Deciding MUS Membership with QBF
[bib]
[slides]
[pdf]
[ee]
17th International Conference on Principles and Practice of Constraint Programming (CP'11) |
|
Abstraction-Based Algorithm for 2QBF
[ee]
[slides]
[pdf]
14th International Conference on Theory and Applications of Satisfiability Testing (SAT '11) |
|
cmMUS: A Tool for Circumscription-Based MUS Membership Testing
[ee]
[pdf]
[tool]
The 11th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR '11) |
| 2010 |
|
Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription
[slides]
[bib]
[ee]
[pdf]
The 12th European Conference on Logics in Artificial Intelligence (JELIA '10) |
|
On Computing Backbones of Propositional Theories
[slides]
[bib]
[pdf]
The 19th European Conference on Artificial Intelligence (ECAI '10). |
|
How to Complete an Interactive Configuration Process?
[slides]
[bib]
[pdf]
International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM '10). |
| 2009 |
|
CLOPS: A DSL for Command Line Options
[slides]
[bib]
[pdf]
[tool]
IFIP Working Conference on Domain Specific Languages (DSL WC), Oxford, 2009. |
| 2008 |
|
Model Construction with External Constraints: An Interactive Journey from Semantics to Syntax
[slides]
[pdf]
ACM/IEEE 11th Int. Conf. on Model Driven Eng. Languages and Systems Fundamental Approaches to Software Engineering (MODELS '08). |
|
Do SAT Solvers Make Good Configurators?
[slides]
[bib]
[pdf]
First Workshop on Analyses of Software Product Lines (ASPL '08). Limerick, Ireland, September 12, 2008. |
|
Formal Approach to Integrating Feature and Architecture Models
[slides]
[pdf]
Fundamental Approaches to Software Engineering (FASE '08). Budapest, Hungary. April, 2008. |
| 2007 |
|
Reachability Analysis for Annotated Code
[slides]
[pdf]
The 6th International Workshop on the Specification and Verification of Component-based Systems (SAVCBS '07). Dubrovnik, Croatia. September, 2007. |
|
Reasoning about Feature Models in Higher-Order Logic
[slides]
[pdf]
The 11th International Software Product Lines Conference (SPLC 2007). Kyoto, Japan. September, 2007. |
|
Assertion-based Loop Invariant Generation
[slides]
[pdf]
The 1st International Workshop on Invariant Generation (WING 2007). Hagenberg, Austria. June, 2007. |
INFOCOS - Intelligent Feedback for Content Students
DTFinder, finder for optimal decision trees
QFUN, QBF Solver based on RAReQS and machine learning
CQESTO, A circuit-based version of QESTO.
QESTO, QBF Solver based on clause selection
AReQS, Abstraction Refinement QBF Solver for non-CNF 2QBF
RAReQS-NN, Recursive Abstraction Refinement QBF Solver supporting Non-CNF, Non-Prenex formulas
RAReQS, Recursive Abstraction Refinement QBF Solver
MiFuMaX, unsat-based MaXSAT solver based on minisat
qcnf2z3, a set of scripts that enable invoking Z3 on QDIMACS instances.
cmMUS, MUS-membership solver based on translation to propositional circumscription
PackUP, a framework for package upgradability solving, allows for an external OPB solver
cudf2msu, a package upgradability solver based on msuncore
cudf2pbo, a package upgradability solver based on WBO
PIEnum, a simple prime implicant/model enumerator
minibones, a program to compute backbones of a formula
Theses
| SAT Solving in Interactive Configuration
[pdf]
[bib]
PhD Thesis, Department of Computer Science at University College Dublin |
| Automated Theorem Proving and Program Verification
[pdf] MSc Thesis, Department of Theoretical Computer Science and Mathematical Logic at Charles University in Prague |
Technical Reports
|
Formal Methods in Software Product Lines: Concepts, Survey, and Guidelines
[bib]
[pdf]
Lero Technical Report, Lero-TR-SPL-2008-02, University of Limerick, May 2008. |
|
|
|
Last updated: Aug 22, 2024 05:16:26 PM PM PM PM PM |