Search Results

Documents authored by Fichte, Johannes K.

Document
DOI: 10.4230/LIPIcs.SAT.2024.5
The Relative Strength of #SAT Proof Systems

Authors: Olaf Beyersdorff, Johannes K. Fichte, Markus Hecher, Tim Hoffmann, and Kaspar Kasche

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
The propositional model counting problem #SAT asks to compute the number of satisfying assignments for a given propositional formula. Recently, three #SAT proof systems kcps (knowledge compilation proof system), MICE (model counting induction by claim extension), and CPOG (certified partitioned-operation graphs) have been introduced with the aim to model #SAT solving and enable proof logging for solvers. Prior to this paper, the relations between these proof systems have been unclear and very few proof complexity results are known. We completely determine the simulation order of the three systems, establishing that CPOG simulates both MICE and kcps, while MICE and kcps are exponentially incomparable. This implies that CPOG is strictly stronger than the other two systems.
Cite as

Olaf Beyersdorff, Johannes K. Fichte, Markus Hecher, Tim Hoffmann, and Kaspar Kasche. The Relative Strength of #SAT Proof Systems. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.SAT.2024.5,
  author =	{Beyersdorff, Olaf and Fichte, Johannes K. and Hecher, Markus and Hoffmann, Tim and Kasche, Kaspar},
  title =	{{The Relative Strength of #SAT Proof Systems}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{5:1--5:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.5},
  URN =		{urn:nbn:de:0030-drops-205276},
  doi =		{10.4230/LIPIcs.SAT.2024.5},
  annote =	{Keywords: Model Counting, #SAT, Proof Complexity, Proof Systems, Lower Bounds, Knowledge Compilation}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.30
Proofs for Propositional Model Counting

Authors: Johannes K. Fichte, Markus Hecher, and Valentin Roland

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

Abstract
Although propositional model counting (#SAT) was long considered too hard to be practical, today’s highly efficient solvers facilitate applications in probabilistic reasoning, reliability estimation, quantitative design space exploration, and more. The current trend of solvers growing more capable every year is likely to continue as a diverse range of algorithms are explored in the field. However, to establish model counters as reliable tools like SAT-solvers, correctness is as critical as speed. As in the nature of complex systems, bugs emerge as soon as the tools are widely used. To identify and avoid bugs, explain decisions, and provide trustworthy results, we need verifiable results. We propose a novel system for certifying model counts. We show how proof traces can be generated for exact model counters based on dynamic programming, counting CDCL with component caching, and knowledge compilation to Decision-DNNF, which are the predominant techniques in today’s exact implementations. We provide proof-of-concepts for emitting proofs and a parallel trace checker. Based on this, we show the feasibility of using certified model counting in an empirical experiment.
Cite as

Johannes K. Fichte, Markus Hecher, and Valentin Roland. Proofs for Propositional Model Counting. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 30:1-30:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{fichte_et_al:LIPIcs.SAT.2022.30,
  author =	{Fichte, Johannes K. and Hecher, Markus and Roland, Valentin},
  title =	{{Proofs for Propositional Model Counting}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{30:1--30:24},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.30},
  URN =		{urn:nbn:de:0030-drops-167043},
  doi =		{10.4230/LIPIcs.SAT.2022.30},
  annote =	{Keywords: Model Counting, Verification, Certified Counting}
}
Document
DOI: 10.4230/LIPIcs.CP.2021.24
Parallel Model Counting with CUDA: Algorithm Engineering for Efficient Hardware Utilization

Authors: Johannes K. Fichte, Markus Hecher, and Valentin Roland

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

Abstract
Propositional model counting (MC) and its extensions as well as applications in the area of probabilistic reasoning have received renewed attention in recent years. As a result, also the need for quickly solving counting-based problems with automated solvers is critical for certain areas. In this paper, we present experiments evaluating various techniques in order to improve the performance of parallel model counting on general purpose graphics processing units (GPGPUs). Thereby, we mainly consider engineering efficient algorithms for model counting on GPGPUs that utilize the treewidth of a propositional formula by means of dynamic programming. The combination of our techniques results in the solver GPUSAT3, which is based on the programming framework Cuda that -compared to other frameworks- shows superior extensibility and driver support. When combining all findings of this work, we show that GPUSAT3 not only solves more instances of the recent Model Counting Competition 2020 (MCC 2020) than existing GPGPU-based systems, but also solves those significantly faster. A portfolio with one of the best solvers of MCC 2020 and GPUSAT3 solves 19% more instances than the former alone in less than half of the runtime.
Cite as

Johannes K. Fichte, Markus Hecher, and Valentin Roland. Parallel Model Counting with CUDA: Algorithm Engineering for Efficient Hardware Utilization. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 24:1-24:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{fichte_et_al:LIPIcs.CP.2021.24,
  author =	{Fichte, Johannes K. and Hecher, Markus and Roland, Valentin},
  title =	{{Parallel Model Counting with CUDA: Algorithm Engineering for Efficient Hardware Utilization}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{24:1--24:20},
  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.24},
  URN =		{urn:nbn:de:0030-drops-153150},
  doi =		{10.4230/LIPIcs.CP.2021.24},
  annote =	{Keywords: Propositional Satisfiability, GPGPU, Model Counting, Treewidth, Tree Decomposition}
}
Document
DOI: 10.4230/LIPIcs.CP.2021.25
Complications for Computational Experiments from Modern Processors

Authors: Johannes K. Fichte, Markus Hecher, Ciaran McCreesh, and Anas Shahab

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

Abstract
In this paper, we revisit the approach to empirical experiments for combinatorial solvers. We provide a brief survey on tools that can help to make empirical work easier. We illustrate origins of uncertainty in modern hardware and show how strong the influence of certain aspects of modern hardware and its experimental setup can be in an actual experimental evaluation. More specifically, there can be situations where (i) two different researchers run a reasonable-looking experiment comparing the same solvers and come to different conclusions and (ii) one researcher runs the same experiment twice on the same hardware and reaches different conclusions based upon how the hardware is configured and used. We investigate these situations from a hardware perspective. Furthermore, we provide an overview on standard measures, detailed explanations on effects, potential errors, and biased suggestions for useful tools. Alongside the tools, we discuss their feasibility as experiments often run on clusters to which the experimentalist has only limited access. Our work sheds light on a number of benchmarking-related issues which could be considered to be folklore or even myths.
Cite as

Johannes K. Fichte, Markus Hecher, Ciaran McCreesh, and Anas Shahab. Complications for Computational Experiments from Modern Processors. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 25:1-25:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{fichte_et_al:LIPIcs.CP.2021.25,
  author =	{Fichte, Johannes K. and Hecher, Markus and McCreesh, Ciaran and Shahab, Anas},
  title =	{{Complications for Computational Experiments from Modern Processors}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{25:1--25:21},
  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.25},
  URN =		{urn:nbn:de:0030-drops-153165},
  doi =		{10.4230/LIPIcs.CP.2021.25},
  annote =	{Keywords: Experimenting, Combinatorial Solving, Empirical Work}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.IPEC.2019.25
The PACE 2019 Parameterized Algorithms and Computational Experiments Challenge: The Fourth Iteration (Invited Paper)

Authors: M. Ayaz Dzulfikar, Johannes K. Fichte, and Markus Hecher

Published in: LIPIcs, Volume 148, 14th International Symposium on Parameterized and Exact Computation (IPEC 2019)

Abstract
The organizers of the 4th Parameterized Algorithms and Computational Experiments challenge (PACE 2019) report on the 4th iteration of the PACE challenge. This year, the first track featured the MinVertexCover problem, which asks given an undirected graph G=(V,E) to output a set S subseteq V of vertices such that for every edge vw in E at least one endpoint belongs to S. The exact decision version of this problem is one of the most discussed problem if not even the prototypical problem in parameterized complexity theory. Another two tracks were dedicated to computing the hypertree width of a given hypergraph, which is a certain generalization of tree decompositions to hypergraphs that has widely been applied to problems in databases, constraint programming, and artificial intelligence. On one track we asked for submissions that compute hypertree decompositions of minimum width (MinHypertreeWidth) and on the other track we asked to heuristically compute hypertree decompositions of small width quickly (HeurHypertreeWidth). We received 28 implementations from 26 teams. This year we asked participants to submit solver descriptions in order to count as a submission for the challenge. We received those from 16 teams with overall 33 participants from 10 countries. One team submitted successful solutions to all three tracks.
Cite as

M. Ayaz Dzulfikar, Johannes K. Fichte, and Markus Hecher. The PACE 2019 Parameterized Algorithms and Computational Experiments Challenge: The Fourth Iteration (Invited Paper). In 14th International Symposium on Parameterized and Exact Computation (IPEC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 148, pp. 25:1-25:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dzulfikar_et_al:LIPIcs.IPEC.2019.25,
  author =	{Dzulfikar, M. Ayaz and Fichte, Johannes K. and Hecher, Markus},
  title =	{{The PACE 2019 Parameterized Algorithms and Computational Experiments Challenge: The Fourth Iteration}},
  booktitle =	{14th International Symposium on Parameterized and Exact Computation (IPEC 2019)},
  pages =	{25:1--25:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-129-0},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{148},
  editor =	{Jansen, Bart M. P. and Telle, Jan Arne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.IPEC.2019.25},
  URN =		{urn:nbn:de:0030-drops-114861},
  doi =		{10.4230/LIPIcs.IPEC.2019.25},
  annote =	{Keywords: Parameterized Algorithms, Vertex Cover Problem, Hypertree Decompositions, Implementation Challenge, FPT}
}
Document
DOI: 10.4230/LIPIcs.ESA.2018.28
Weighted Model Counting on the GPU by Exploiting Small Treewidth

Authors: Johannes K. Fichte, Markus Hecher, Stefan Woltran, and Markus Zisser

Published in: LIPIcs, Volume 112, 26th Annual European Symposium on Algorithms (ESA 2018)

Abstract
We propose a novel solver that efficiently finds almost the exact number of solutions of a Boolean formula (#Sat) and the weighted model count of a weighted Boolean formula (WMC) if the treewidth of the given formula is sufficiently small. The basis of our approach are dynamic programming algorithms on tree decompositions, which we engineered towards efficient parallel execution on the GPU. We provide thorough experiments and compare the runtime of our system with state-of-the-art #Sat and WMC solvers. Our results are encouraging in the sense that also complex reasoning problems can be tackled by parameterized algorithms executed on the GPU if instances have treewidth at most 30, which is the case for more than half of counting and weighted counting benchmark instances.
Cite as

Johannes K. Fichte, Markus Hecher, Stefan Woltran, and Markus Zisser. Weighted Model Counting on the GPU by Exploiting Small Treewidth. In 26th Annual European Symposium on Algorithms (ESA 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 112, pp. 28:1-28:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{fichte_et_al:LIPIcs.ESA.2018.28,
  author =	{Fichte, Johannes K. and Hecher, Markus and Woltran, Stefan and Zisser, Markus},
  title =	{{Weighted Model Counting on the GPU by Exploiting Small Treewidth}},
  booktitle =	{26th Annual European Symposium on Algorithms (ESA 2018)},
  pages =	{28:1--28:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-081-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{112},
  editor =	{Azar, Yossi and Bast, Hannah and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2018.28},
  URN =		{urn:nbn:de:0030-drops-94915},
  doi =		{10.4230/LIPIcs.ESA.2018.28},
  annote =	{Keywords: Parameterized Algorithms, Weighted Model Counting, General Purpose Computing on Graphics Processing Units, Dynamic Programming, Tree Decompositions, Treewidth}
}
Document
DOI: 10.4230/LIPIcs.IPEC.2017.17
DynASP2.5: Dynamic Programming on Tree Decompositions in Action

Authors: Johannes K. Fichte, Markus Hecher, Michael Morak, and Stefan Woltran

Published in: LIPIcs, Volume 89, 12th International Symposium on Parameterized and Exact Computation (IPEC 2017)

Abstract
Efficient, exact parameterized algorithms are a vibrant theoretical research area. Recent solving competitions, such as the PACE challenge, show that there is also increasing practical interest in the parameterized algorithms community. An important research question is whether such algorithms can be built to efficiently solve specific problems in practice, that is, to be competitive with established solving systems. In this paper, we consider Answer Set Programming (ASP), a logic-based declarative modeling and problem solving framework. State-of-the-art ASP solvers generally rely on SAT-based algorithms. In addition, DynASP2, an ASP solver that is based on a classical dynamic programming on tree decompositions, has recently been introduced. DynASP2 outperforms modern ASP solvers when the goal is to count the number of solutions of programs that have small treewidth. However, for quickly finding one solutions, DynASP2 proved uncompetitive. In this paper, we present a new algorithm and implementation, called DynASP2.5, that shows competitive behavior compared to state-of-the-art ASP solvers on problems like Steiner tree for low-treewidth graphs, even when the task is to find just one solution. Our implementation is based on a novel approach that we call multi-pass dynamic programming.
Cite as

Johannes K. Fichte, Markus Hecher, Michael Morak, and Stefan Woltran. DynASP2.5: Dynamic Programming on Tree Decompositions in Action. In 12th International Symposium on Parameterized and Exact Computation (IPEC 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 89, pp. 17:1-17:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{fichte_et_al:LIPIcs.IPEC.2017.17,
  author =	{Fichte, Johannes K. and Hecher, Markus and Morak, Michael and Woltran, Stefan},
  title =	{{DynASP2.5: Dynamic Programming on Tree Decompositions in Action}},
  booktitle =	{12th International Symposium on Parameterized and Exact Computation (IPEC 2017)},
  pages =	{17:1--17:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-051-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{89},
  editor =	{Lokshtanov, Daniel and Nishimura, Naomi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.IPEC.2017.17},
  URN =		{urn:nbn:de:0030-drops-85739},
  doi =		{10.4230/LIPIcs.IPEC.2017.17},
  annote =	{Keywords: Parameterized algorithms, Fixed-parameter linear time, Tree decompositions, Multi-pass dynamic programming}
}
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