Mikolás Janota

Josef Urban

Proceedings of the Intelligent Computer Mathematics - 17th International Conference, 2024

First Experiments with Neural cvc5.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2024: Proceedings of 25th Conference on Logic for Programming, 2024

C-Pack of IPAs: A C90 Program Benchmark of Introductory Programming Assignments.

[BibT_eX]

[DOI]

Proceedings of the IEEE/ACM International Workshop on Automated Program Repair, 2024

cfaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases.

[BibT_eX]

[DOI]

Vasco M. Manquinho

Proceedings of the Formal Methods - 26th International Symposium, 2024

Machine Learning for Quantifier Selection in cvc5.

[BibT_eX]

[DOI]

Proceedings of the ECAI 2024 - 27th European Conference on Artificial Intelligence, 19-24 October 2024, Santiago de Compostela, Spain, 2024

Cube-Based Isomorph-Free Finite Model Finding.

[BibT_eX]

[DOI]

Proceedings of the ECAI 2024 - 27th European Conference on Artificial Intelligence, 19-24 October 2024, Santiago de Compostela, Spain, 2024

Understanding GNNs for Boolean Satisfiability through Approximation Algorithms.

[BibT_eX]

[DOI]

David Mojzísek

Proceedings of the 33rd ACM International Conference on Information and Knowledge Management, 2024

SAT-Based Techniques for Lexicographically Smallest Finite Models.

[BibT_eX]

[DOI]

Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence, 2024

2023

Computing generating sets of minimal size in finite algebras.

[BibT_eX]

[DOI]

António Morgado

Petr Vojtechovský

J. Symb. Comput., 2023

Integrated lot-sizing and scheduling: Mitigation of uncertainty in demand and processing time by machine learning.

[BibT_eX]

[DOI]

Mohammad Rohaninejad

Zdenek Hanzálek

Eng. Appl. Artif. Intell., 2023

Graph Neural Networks For Mapping Variables Between Programs - Extended Version.

[BibT_eX]

[DOI]

CoRR, 2023

Towards Learning Infinite SMT Models (Work in Progress).

[BibT_eX]

[DOI]

Bartosz Piotrowski

Karel Chvalovský

Proceedings of the 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2023

Selecting Quantifiers for Instantiation in SMT.

[BibT_eX]

[DOI]

Proceedings of the 21st International Workshop on Satisfiability Modulo Theories (SMT 2023) co-located with the 29th International Conference on Automated Deduction (CADE 2023), 2023

Experiments on Infinite Model Finding in SMT Solving.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

A Mathematical Benchmark for Inductive Theorem Provers.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

Molecule Builder: Environment for Testing Reinforcement Learning Agents.

[BibT_eX]

[DOI]

Petr Hyner

Proceedings of the 15th International Joint Conference on Computational Intelligence, 2023

Fast Heuristic for Ricochet Robots.

[BibT_eX]

[DOI]

David Adamczyk

Proceedings of the 15th International Conference on Agents and Artificial Intelligence, 2023

The FMCAD 2023 Student Forum.

[BibT_eX]

[DOI]

Nina Narodytska

Proceedings of the Formal Methods in Computer-Aided Design, 2023

Data-driven Single Machine Scheduling Minimizing Weighted Number of Tardy Jobs.

[BibT_eX]

[DOI]

Nikolai Antonov

Premysl Sucha

Proceedings of the Progress in Artificial Intelligence, 2023

Graph Neural Networks for Mapping Variables Between Programs.

[BibT_eX]

[DOI]

Proceedings of the ECAI 2023 - 26th European Conference on Artificial Intelligence, September 30 - October 4, 2023, Kraków, Poland, 2023

Symmetries for Cube-And-Conquer in Finite Model Finding.

[BibT_eX]

[DOI]

Proceedings of the 29th International Conference on Principles and Practice of Constraint Programming, 2023

2022

Machine Learning Meets The Herbrand Universe.

[BibT_eX]

[DOI]

CoRR, 2022

TestSelector: Automatic Test Suite Selection for Student Projects - Extended Version.

[BibT_eX]

[DOI]

CoRR, 2022

InvAASTCluster: On Applying Invariant-Based Program Clustering to Introductory Programming Assignments.

[BibT_eX]

[DOI]

CoRR, 2022

Boosting isomorphic model filtering with invariants.

[BibT_eX]

[DOI]

Constraints An Int. J., 2022

Abstract: Challenges and Solutions for Higher-Order SMT Proofs.

[BibT_eX]

[DOI]

Chad E. Brown

Cezary Kaliszyk

Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), 2022

MultIPAs: applying program transformations to introductory programming assignments for data augmentation.

[BibT_eX]

[DOI]

Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2022

Towards Learning Quantifier Instantiation in SMT.

[BibT_eX]

[DOI]

Jelle Piepenbrock

Bartosz Piotrowski

Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing, 2022

SAT-Based Leximax Optimisation Algorithms.

[BibT_eX]

[DOI]

Miguel Cabral

Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing, 2022

TestSelector: Automatic Test Suite Selection for Student Projects.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - 22nd International Conference, 2022

Targeted Configuration of an SMT Solver.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 15th International Conference, 2022

Guiding an Automated Theorem Prover with Neural Rewriting.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021

Quantified Boolean Formulas.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Satisfiability - Second Edition, 2021

Learning Equational Theorem Proving.

[BibT_eX]

[DOI]

CoRR, 2021

Characteristic Subsets of SMT-LIB Benchmarks.

[BibT_eX]

[DOI]

Jan Jakubuv

Andrew Reynolds

Proceedings of the 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification(CAV 2021), 2021

First-Order Instantiation using Discriminating Terms.

[BibT_eX]

[DOI]

Chad E. Brown

Proceedings of the 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification(CAV 2021), 2021

Graph Neural Networks for Scheduling of SMT Solvers.

[BibT_eX]

[DOI]

David Mojzísek

Proceedings of the 33rd IEEE International Conference on Tools with Artificial Intelligence, 2021

Fair and Adventurous Enumeration of Quantifier Instantiations.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer Aided Design, 2021

The Seesaw Algorithm: Function Optimization Using Implicit Hitting Sets.

[BibT_eX]

[DOI]

Proceedings of the 27th International Conference on Principles and Practice of Constraint Programming, 2021

Filtering Isomorphic Models by Invariants (Short Paper).

[BibT_eX]

[DOI]

Proceedings of the 27th International Conference on Principles and Practice of Constraint Programming, 2021

2020

SAT-Based Encodings for Optimal Decision Trees with Explicit Paths.

[BibT_eX]

[DOI]

António Morgado

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2020, 2020

2019

New Resolution-Based QBF Calculi and Their Proof Complexity.

[BibT_eX]

[DOI]

ACM Trans. Comput. Theory, 2019

PrideMM: A Solver for Relaxed Memory Models.

[BibT_eX]

[DOI]

CoRR, 2019

PrideMM: Second Order Model Checking for Memory Consistency Models.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods. FM 2019 International Workshops, 2019

On Unordered BDDs and Quantified Boolean Formulas.

[BibT_eX]

[DOI]

Proceedings of the Progress in Artificial Intelligence, 2019

2018

Circuit-Based Search Space Pruning in QBF.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2018, 2018

Towards Smarter MACE-style Model Finders.

[BibT_eX]

[DOI]

Martin Suda

Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

Towards Generalization in QBF Solving via Machine Learning.

[BibT_eX]

[DOI]

Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, 2018

2017

QFUN: Towards Machine Learning in QBF.

[BibT_eX]

[DOI]

CoRR, 2017

An Achilles' Heel of Term-Resolution.

[BibT_eX]

[DOI]

CoRR, 2017

Minimal sets on propositional formulae. Problems and reductions.

[BibT_eX]

[DOI]

Carlos Mencía

Artif. Intell., 2017

An Achilles' Heel of Term-Resolution.

[BibT_eX]

[DOI]

Proceedings of the Progress in Artificial Intelligence, 2017

On Minimal Corrections in ASP.

[BibT_eX]

[DOI]

Proceedings of the 24th RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion 2017 co-located with the 16th International Conference of the Italian Association for Artificial Intelligence (AI*IA 2017), 2017

On the Quest for an Acyclic Graph.

[BibT_eX]

[DOI]

2016

On Exponential Lower Bounds for Partially Ordered Resolution.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2016

On Q-Resolution and CDCL QBF Solving.

[BibT_eX]

[DOI]

Electron. Colloquium Comput. Complex., 2016

Extension Variables in QBF Resolution.

[BibT_eX]

[DOI]

Electron. Colloquium Comput. Complex., 2016

Quantified maximum satisfiability.

[BibT_eX]

[DOI]

Alexey Ignatiev

Constraints An Int. J., 2016

On the query complexity of selecting minimal sets for monotone predicates.

[BibT_eX]

[DOI]

Artif. Intell., 2016

Solving QBF with counterexample guided refinement.

[BibT_eX]

[DOI]

Artif. Intell., 2016

On Incremental Core-Guided MaxSAT Solving.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2016

On Intervals and Bounds in Bit-vector Arithmetic.

[BibT_eX]

[DOI]

Christoph M. Wintersteiger

Proceedings of the 14th International Workshop on Satisfiability Modulo Theories affiliated with the International Joint Conference on Automated Reasoning, 2016

2015

Expansion-based QBF solving versus Q-resolution.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2015

Algorithms for computing backbones of propositional formulae.

[BibT_eX]

[DOI]

Inês Lynce

AI Commun., 2015

Exploiting Resolution-Based Representations for MaxSAT Solving.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2015, 2015

On Conflicts and Strategies in QBF.

[BibT_eX]

[DOI]

Nikolaj S. Bjørner

William Klieber

Proceedings of the 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, 2015

Playing with Quantified Satisfaction.

[BibT_eX]

[DOI]

Nikolaj S. Bjørner

Proceedings of the 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, 2015

Efficient Model Based Diagnosis with Maximum Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015

Solving QBF by Clause Selection.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015

Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs.

[BibT_eX]

[DOI]

Valeriy Balabanov

Jie-Hong Roland Jiang

Magdalena Widl

Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, 2015

2014

The QBFGallery 2014: The QBF Competition at the FLoC Olympic Games.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2014

MiFuMax - a Literate MaxSAT Solver.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2014

On the Query Complexity of Selecting Few Minimal Sets.

[BibT_eX]

[DOI]

Electron. Colloquium Comput. Complex., 2014

On Unification of QBF Resolution-Based Calculi.

[BibT_eX]

[DOI]

Electron. Colloquium Comput. Complex., 2014

Proof Complexity of Resolution-based QBF Calculi.

[BibT_eX]

[DOI]

Electron. Colloquium Comput. Complex., 2014

Computing Minimal Sets on Propositional Formulae I: Problems & Reductions.

[BibT_eX]

[DOI]

CoRR, 2014

Algorithms for computing minimal equivalent subformulas.

[BibT_eX]

[DOI]

Artif. Intell., 2014

On lazy and eager interactive reconfiguration.

[BibT_eX]

[DOI]

Goetz Botterweck

Proceedings of the Eighth International Workshop on Variability Modelling of Software-intensive Systems, 2014

Towards efficient optimization in package management systems.

[BibT_eX]

[DOI]

Alexey Ignatiev

Proceedings of the 36th International Conference on Software Engineering, 2014

2013

On Propositional QBF Expansions and Q-Resolution.

[BibT_eX]

[DOI]

Electron. Colloquium Comput. Complex., 2013

Quantified Maximum Satisfiability: - A Core-Guided Approach.

[BibT_eX]

[DOI]

Alexey Ignatiev

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2013, 2013

On QBF Proofs and Preprocessing.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

On Computing Minimal Correction Subsets.

[BibT_eX]

[DOI]

Proceedings of the IJCAI 2013, 2013

Solving QBF with Free Variables.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2013

Minimal Sets over Monotone Predicates in Boolean Formulae.

[BibT_eX]

[DOI]

Anton Belov

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2012

PackUp: Tools for Package Upgradability Solving.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2012

On Unit-Refutation Complete Formulae with Existentially Quantified Variables.

[BibT_eX]

[DOI]

Proceedings of the Principles of Knowledge Representation and Reasoning: Proceedings of the Thirteenth International Conference, 2012

QBf-based boolean function bi-decomposition.

[BibT_eX]

[DOI]

Huan Chen

Proceedings of the 2012 Design, Automation & Test in Europe Conference & Exhibition, 2012

On Computing Minimal Equivalent Subformulas.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2012

2011

Abstraction-Based Algorithm for 2QBF.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2011, 2011

cmMUS: A Tool for Circumscription-Based MUS Membership Testing.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming and Nonmonotonic Reasoning, 2011

On Deciding MUS Membership with QBF.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming - CP 2011, 2011

2010

How to Complete an Interactive Configuration Process?

[BibT_eX]

[DOI]

Proceedings of the SOFSEM 2010: Theory and Practice of Computer Science, 2010

Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription.

[BibT_eX]

[DOI]

Proceedings of the Logics in Artificial Intelligence - 12th European Conference, 2010

On Computing Backbones of Propositional Theories.

[BibT_eX]

[DOI]

Inês Lynce

Proceedings of the ECAI 2010, 2010

2009

Algorithms for finding dispensable variables

[BibT_eX]

[DOI]

CoRR, 2009

A Design of a Configurable Feature Model Configurator.

[BibT_eX]

[DOI]

Goetz Botterweck

Denny Schneeweiss

Proceedings of the Third International Workshop on Variability Modelling of Software-Intensive Systems, 2009

CLOPS: A DSL for Command Line Options.

[BibT_eX]

[DOI]

Proceedings of the Domain-Specific Languages, IFIP TC 2 Working Conference, 2009

2008

Do SAT Solvers Make Good Configurators?

[BibT_eX]

Proceedings of the Software Product Lines, 12th International Conference, 2008

Model Construction with External Constraints: An Interactive Journey from Semantics to Syntax.

[BibT_eX]

[DOI]

Victoria Kuzina

Andrzej Wasowski

Proceedings of the Model Driven Engineering Languages and Systems, 2008

Formal Approach to Integrating Feature and Architecture Models.

[BibT_eX]

[DOI]

Goetz Botterweck

Proceedings of the Fundamental Approaches to Software Engineering, 2008

2007

Reasoning about Feature Models in Higher-Order Logic.

[BibT_eX]

[DOI]

Joseph Kiniry

Proceedings of the Software Product Lines, 11th International Conference, 2007

Reachability analysis for annotated code.

[BibT_eX]

[DOI]