8 Search Results for "Janota, Mikolás"

Document
DOI: 10.4230/LIPIcs.CP.2023.8
Symmetries for Cube-And-Conquer in Finite Model Finding

Authors: João Araújo, Choiwah Chow, and Mikoláš Janota

Published in: LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)

Abstract
The cube-and-conquer paradigm enables massive parallelization of SAT solvers, which has proven to be crucial in solving highly combinatorial problems. In this paper, we apply the paradigm in the context of finite model finding, where we show that isomorphic cubes can be discarded since they lead to isomorphic models. However, we are faced with the complication that a well-known technique, the Least Number Heuristic (LNH), already exists in finite model finders to effectively prune (some) isomorphic models from the search. Therefore, it needs to be shown that isomorphic cubes still can be discarded when the LNH is used. The presented ideas are incorporated into the finite model finder Mace4, where we demonstrate significant improvements in model enumeration.
Cite as

João Araújo, Choiwah Chow, and Mikoláš Janota. Symmetries for Cube-And-Conquer in Finite Model Finding. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{araujo_et_al:LIPIcs.CP.2023.8,
  author =	{Ara\'{u}jo, Jo\~{a}o and Chow, Choiwah and Janota, Mikol\'{a}\v{s}},
  title =	{{Symmetries for Cube-And-Conquer in Finite Model Finding}},
  booktitle =	{29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
  pages =	{8:1--8:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-300-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{280},
  editor =	{Yap, Roland H. C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.8},
  URN =		{urn:nbn:de:0030-drops-190455},
  doi =		{10.4230/LIPIcs.CP.2023.8},
  annote =	{Keywords: finite model enumeration, cube-and-conquer, symmetry-breaking, parallel algorithm, least number heuristic}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.19
MizAR 60 for Mizar 50

Authors: Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, and Josef Urban

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
As a present to Mizar on its 50th anniversary, we develop an AI/TP system that automatically proves about 60% of the Mizar theorems in the hammer setting. We also automatically prove 75% of the Mizar theorems when the automated provers are helped by using only the premises used in the human-written Mizar proofs. We describe the methods and large-scale experiments leading to these results. This includes in particular the E and Vampire provers, their ENIGMA and Deepire learning modifications, a number of learning-based premise selection methods, and the incremental loop that interleaves growing a corpus of millions of ATP proofs with training increasingly strong AI/TP systems on them. We also present a selection of Mizar problems that were proved automatically.
Cite as

Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, and Josef Urban. MizAR 60 for Mizar 50. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{jakubuv_et_al:LIPIcs.ITP.2023.19,
  author =	{Jakub\r{u}v, Jan and Chvalovsk\'{y}, Karel and Goertzel, Zarathustra and Kaliszyk, Cezary and Ol\v{s}\'{a}k, Mirek and Piotrowski, Bartosz and Schulz, Stephan and Suda, Martin and Urban, Josef},
  title =	{{MizAR 60 for Mizar 50}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{19:1--19:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.19},
  URN =		{urn:nbn:de:0030-drops-183942},
  doi =		{10.4230/LIPIcs.ITP.2023.19},
  annote =	{Keywords: Mizar, ENIGMA, Automated Reasoning, Machine Learning}
}
Document
DOI: 10.4230/LIPIcs.STACS.2023.21
Extending Merge Resolution to a Family of QBF-Proof Systems

Authors: Sravanthi Chede and Anil Shukla

Published in: LIPIcs, Volume 254, 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)

Abstract
Merge Resolution (MRes [Olaf Beyersdorff et al., 2021]) is a recently introduced proof system for false QBFs. Unlike other known QBF proof systems, it builds winning strategies for the universal player (countermodels) within the proofs as merge maps. Merge maps are deterministic branching programs in which isomorphism checking is efficient, as a result MRes is a polynomial time verifiable proof system. In this paper, we introduce a family of proof systems MRes-ℛ in which the information of countermodels are stored in any pre-fixed complete representation ℛ. Hence, corresponding to each possible complete representation ℛ, we have a sound and refutationally complete QBF-proof system in MRes-ℛ. To handle these arbitrary representations, we introduce consistency checking rules in MRes-ℛ instead of the isomorphism checking in MRes. As a result these proof systems are not polynomial time verifiable (Non-P). Consequently, the paper shows that using merge maps is too restrictive and with a slight change in rules, it can be replaced with arbitrary representations leading to several interesting proof systems. We relate these new systems with the implicit proof system from the algorithm in [Joshua Blinkhorn et al., 2021], which was designed to solve DQBFs (Dependency QBFs) using clause-strategy pairs like MRes. We use the OBDD (Ordered Binary Decision Diagrams) representation suggested in [Joshua Blinkhorn et al., 2021] and deduce that "Ordered" versions of the proof systems in MRes-ℛ are indeed polynomial time verifiable. On the lower bound side, we lift the lower bound result of regular MRes ([Olaf Beyersdorff et al., 2020]) by showing that the completion principle formulas (CR_n) from [Mikolás Janota and João Marques-Silva, 2015] which are shown to be hard for regular MRes in [Olaf Beyersdorff et al., 2020], are also hard for any regular proof system in MRes-ℛ. Thereby, the paper lifts the lower bound of regular MRes to an entire class of proof systems, which use various complete representations, including those undiscovered, instead of only merge maps. Thereby proving that the hardness of CR_n formulas is intact even after changing the weak isomorphism checking in MRes to the stronger consistency checking in MRes-ℛ.
Cite as

Sravanthi Chede and Anil Shukla. Extending Merge Resolution to a Family of QBF-Proof Systems. In 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 254, pp. 21:1-21:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{chede_et_al:LIPIcs.STACS.2023.21,
  author =	{Chede, Sravanthi and Shukla, Anil},
  title =	{{Extending Merge Resolution to a Family of QBF-Proof Systems}},
  booktitle =	{40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)},
  pages =	{21:1--21:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-266-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{254},
  editor =	{Berenbrink, Petra and Bouyer, Patricia and Dawar, Anuj and Kant\'{e}, Mamadou Moustapha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2023.21},
  URN =		{urn:nbn:de:0030-drops-176737},
  doi =		{10.4230/LIPIcs.STACS.2023.21},
  annote =	{Keywords: Proof complexity, QBFs, Merge Resolution, Simulation, Lower Bound}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.7
Towards Learning Quantifier Instantiation in SMT

Authors: Mikoláš Janota, Jelle Piepenbrock, and Bartosz Piotrowski

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract
This paper applies machine learning (ML) to solve quantified satisfiability modulo theories (SMT) problems more efficiently. The motivating idea is that the solver should learn from already solved formulas to solve new ones. This is especially relevant in classes of similar formulas. We focus on the enumerative instantiation - a well-established approach to solving quantified formulas anchored in the Herbrand’s theorem. The task is to select the right ground terms to be instantiated. In ML parlance, this means learning to rank ground terms. We devise a series of features of the considered terms and train on them using boosted decision trees. In particular, we integrate the LightGBM library into the SMT solver cvc5. The experimental results demonstrate that the ML-guided solver enables us to solve more formulas than the base solver and reduce the number of quantifier instantiations. We also do an ablation study on the features used in the machine learning component, showing the contributions of the various additions.
Cite as

Mikoláš Janota, Jelle Piepenbrock, and Bartosz Piotrowski. Towards Learning Quantifier Instantiation in SMT. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{janota_et_al:LIPIcs.SAT.2022.7,
  author =	{Janota, Mikol\'{a}\v{s} and Piepenbrock, Jelle and Piotrowski, Bartosz},
  title =	{{Towards Learning Quantifier Instantiation in SMT}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{7:1--7:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.7},
  URN =		{urn:nbn:de:0030-drops-166810},
  doi =		{10.4230/LIPIcs.SAT.2022.7},
  annote =	{Keywords: satisfiability modulo theories, quantifier instantiation, machine learning}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.29
SAT-Based Leximax Optimisation Algorithms

Authors: Miguel Cabral, Mikoláš Janota, and Vasco Manquinho

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract
In several real-world problems, it is often the case that the goal is to optimise several objective functions. However, usually there is not a single optimal objective vector. Instead, there are many optimal objective vectors known as Pareto-optima. Finding all Pareto-optima is computationally expensive and the number of Pareto-optima can be too large for a user to analyse. A compromise can be made by defining an optimisation criterion that integrates all objective functions. In this paper we propose several SAT-based algorithms to solve multi-objective optimisation problems using the leximax criterion. The leximax criterion is used to obtain a Pareto-optimal solution with a small trade-off between the objective functions, which is suitable in problems where there is an absence of priorities between the objective functions. Experimental results on the Multi-Objective Package Upgradeability Optimisation problem show that the SAT-based algorithms are able to outperform the Integer Linear Programming (ILP) approach when using non-commercial ILP solvers. Additionally, experimental results on selected instances from the MaxSAT evaluation adapted to the multi-objective domain show that our approach outperforms the ILP approach using commercial solvers.
Cite as

Miguel Cabral, Mikoláš Janota, and Vasco Manquinho. SAT-Based Leximax Optimisation Algorithms. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 29:1-29:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{cabral_et_al:LIPIcs.SAT.2022.29,
  author =	{Cabral, Miguel and Janota, Mikol\'{a}\v{s} and Manquinho, Vasco},
  title =	{{SAT-Based Leximax Optimisation Algorithms}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{29:1--29:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.29},
  URN =		{urn:nbn:de:0030-drops-167030},
  doi =		{10.4230/LIPIcs.SAT.2022.29},
  annote =	{Keywords: Multi-Objective Optimisation, Leximax, Sorting Networks}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.CP.2021.4
Filtering Isomorphic Models by Invariants (Short Paper)

Authors: João Araújo, Choiwah Chow, and Mikoláš Janota

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
The enumeration of finite models of first order logic formulas is an indispensable tool in computational algebra. The task is hindered by the existence of isomorphic models, which are of no use to mathematicians and therefore are typically filtered out a posteriori. This paper proposes a divide-and-conquer approach to speed up and parallelize this process. We design a series of invariant properties that enable us to partition existing models into mutually non-isomorphic blocks, which are then tackled separately. The presented approach is integrated into the popular tool Mace4, where it shows tremendous speed-ups for a variety of algebraic structures.
Cite as

João Araújo, Choiwah Chow, and Mikoláš Janota. Filtering Isomorphic Models by Invariants (Short Paper). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 4:1-4:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{araujo_et_al:LIPIcs.CP.2021.4,
  author =	{Ara\'{u}jo, Jo\~{a}o and Chow, Choiwah and Janota, Mikol\'{a}\v{s}},
  title =	{{Filtering Isomorphic Models by Invariants}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{4:1--4:9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.4},
  URN =		{urn:nbn:de:0030-drops-152956},
  doi =		{10.4230/LIPIcs.CP.2021.4},
  annote =	{Keywords: finite model enumeration, isomorphism, invariants, Mace4}
}
Document
DOI: 10.4230/LIPIcs.CP.2021.31
The Seesaw Algorithm: Function Optimization Using Implicit Hitting Sets

Authors: Mikoláš Janota, António Morgado, José Fragoso Santos, and Vasco Manquinho

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
The paper introduces the Seesaw algorithm, which explores the Pareto frontier of two given functions. The algorithm is complete and generalizes the well-known implicit hitting set paradigm. The first given function determines a cost of a hitting set and is optimized by an exact solver. The second, called the oracle function, is treated as a black-box. This approach is particularly useful in the optimization of functions that are impossible to encode into an exact solver. We show the effectiveness of the algorithm in the context of static solver portfolio selection. The existing implicit hitting set paradigm is applied to cost function and an oracle predicate. Hence, the Seesaw algorithm generalizes this by enabling the oracle to be a function. The paper identifies two independent preconditions that guarantee the correctness of the algorithm. This opens a number of avenues for future research into the possible instantiations of the algorithm, depending on the cost and oracle functions used.
Cite as

Mikoláš Janota, António Morgado, José Fragoso Santos, and Vasco Manquinho. The Seesaw Algorithm: Function Optimization Using Implicit Hitting Sets. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{janota_et_al:LIPIcs.CP.2021.31,
  author =	{Janota, Mikol\'{a}\v{s} and Morgado, Ant\'{o}nio and Fragoso Santos, Jos\'{e} and Manquinho, Vasco},
  title =	{{The Seesaw Algorithm: Function Optimization Using Implicit Hitting Sets}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{31:1--31:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.31},
  URN =		{urn:nbn:de:0030-drops-153220},
  doi =		{10.4230/LIPIcs.CP.2021.31},
  annote =	{Keywords: implicit hitting sets, minimal hitting set, MaxSAT, optimization}
}
Document
DOI: 10.4230/LIPIcs.STACS.2015.76
Proof Complexity of Resolution-based QBF Calculi

Authors: Olaf Beyersdorff, Leroy Chew, and Mikolás Janota

Published in: LIPIcs, Volume 30, 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)

Abstract
Proof systems for quantified Boolean formulas (QBFs) provide a theoretical underpinning for the performance of important QBF solvers. However, the proof complexity of these proof systems is currently not well understood and in particular lower bound techniques are missing. In this paper we exhibit a new and elegant proof technique for showing lower bounds in QBF proof systems based on strategy extraction. This technique provides a direct transfer of circuit lower bounds to lengths of proofs lower bounds. We use our method to show the hardness of a natural class of parity formulas for Q-resolution and universal Q-resolution. Variants of the formulas are hard for even stronger systems as long-distance Q-resolution and extensions. With a completely different lower bound argument we show the hardness of the prominent formulas of Kleine Büning et al. [34] for the strong expansion-based calculus IR-calc. Our lower bounds imply new exponential separations between two different types of resolution-based QBF calculi: proof systems for CDCL-based solvers (Q-resolution, long-distance Q-resolution) and proof systems for expansion-based solvers (forallExp+Res and its generalizations IR-calc and IRM-calc). The relations between proof systems from the two different classes were not known before.
Cite as

Olaf Beyersdorff, Leroy Chew, and Mikolás Janota. Proof Complexity of Resolution-based QBF Calculi. In 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 30, pp. 76-89, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.STACS.2015.76,
  author =	{Beyersdorff, Olaf and Chew, Leroy and Janota, Mikol\'{a}s},
  title =	{{Proof Complexity of Resolution-based QBF Calculi}},
  booktitle =	{32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)},
  pages =	{76--89},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-78-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{30},
  editor =	{Mayr, Ernst W. and Ollinger, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2015.76},
  URN =		{urn:nbn:de:0030-drops-49057},
  doi =		{10.4230/LIPIcs.STACS.2015.76},
  annote =	{Keywords: proof complexity, QBF, lower bound techniques, separations}
}
  • Refine by Author
  • 5 Janota, Mikoláš
  • 2 Araújo, João
  • 2 Chow, Choiwah
  • 2 Manquinho, Vasco
  • 2 Piotrowski, Bartosz
  • Show More...

  • Refine by Classification
  • 2 Computing methodologies
  • 2 Computing methodologies → Optimization algorithms
  • 2 Theory of computation → Automated reasoning
  • 2 Theory of computation → Constraint and logic programming
  • 1 Theory of computation → Proof complexity

  • Refine by Keyword
  • 2 finite model enumeration
  • 1 Automated Reasoning
  • 1 ENIGMA
  • 1 Leximax
  • 1 Lower Bound
  • Show More...

  • Refine by Type
  • 8 document

  • Refine by Publication Year
  • 3 2023
  • 2 2021
  • 2 2022
  • 1 2015

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact