6 Search Results for "Heisinger, Maximilian"

Document
DOI: 10.4230/LIPIcs.CP.2025.34
DynamicSAT: Dynamic Configuration Tuning for SAT Solving

Authors: Zhengyuan Shi, Wentao Jiang, Xindi Zhang, Jin Luo, Yun Liang, Zhufei Chu, and Qiang Xu

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
Boolean Satisfiability (SAT) problem serves as a foundation for solving numerous real-world challenges. As problem complexity increases, so does the demand for sophisticated SAT solvers, which incorporate a variety of heuristics tailored to optimize performance for specific problem instances. However, a major limitation persists: a configuration that performs well on one instance may lead to inefficiencies on others. While previous approaches to automatic algorithm configuration set parameters prior to runtime, they fail to adapt to the dynamic evolution of problem characteristics during the solving process. We introduce DynamicSAT, a novel SAT solver framework that dynamically tunes configuration parameters during solving process. By adjusting parameters on-the-fly, DynamicSAT adapts to changes arising from clause learning, elimination, and other transformations, thus improving efficiency and robustness across diverse SAT instances. We demonstrate that DynamicSAT achieves significant performance gains over the state-of-the-art solver on 2024 SAT Competition Benchmark.
Cite as

Zhengyuan Shi, Wentao Jiang, Xindi Zhang, Jin Luo, Yun Liang, Zhufei Chu, and Qiang Xu. DynamicSAT: Dynamic Configuration Tuning for SAT Solving. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 34:1-34:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{shi_et_al:LIPIcs.CP.2025.34,
  author =	{Shi, Zhengyuan and Jiang, Wentao and Zhang, Xindi and Luo, Jin and Liang, Yun and Chu, Zhufei and Xu, Qiang},
  title =	{{DynamicSAT: Dynamic Configuration Tuning for SAT Solving}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{34:1--34:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.34},
  URN =		{urn:nbn:de:0030-drops-238952},
  doi =		{10.4230/LIPIcs.CP.2025.34},
  annote =	{Keywords: Boolean satisfiability problem, configuration tuning, multi-armed bandit}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.27
Streamlining Distributed SAT Solver Design

Authors: Dominik Schreiber, Niccolò Rigi-Luperti, and Armin Biere

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
Distributed clause-sharing SAT solvers have recently been established as powerful automated reasoning tools that can conquer previously infeasible instances. A common design of distributed SAT solvers is to run many off-the-shelf sequential solvers in parallel, employ some diversification (e.g., restart intervals or decision orders), and share conflict clauses among the solver threads. This approach, naïvely, adopts all best practices of sequential solver design for distributed solving, where these practices may be less useful or even actively detrimental. In this work we diagnose such shortcomings in the state-of-the-art system MallobSat and propose first effective mitigations. In particular, we replace the redundant pre- and inprocessing at all threads with single-core preprocessing that runs next to the parallel search, remove LBD values from the clause-sharing operation, and slim down solver diversification to very few lightweight and uniform methods. Experimental evaluations on up to 3072 cores (64 nodes) confirm that our measures improve performance while also drastically simplifying the SAT solving program that is run in parallel.
Cite as

Dominik Schreiber, Niccolò Rigi-Luperti, and Armin Biere. Streamlining Distributed SAT Solver Design. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 27:1-27:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{schreiber_et_al:LIPIcs.SAT.2025.27,
  author =	{Schreiber, Dominik and Rigi-Luperti, Niccol\`{o} and Biere, Armin},
  title =	{{Streamlining Distributed SAT Solver Design}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{27:1--27:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.27},
  URN =		{urn:nbn:de:0030-drops-237615},
  doi =		{10.4230/LIPIcs.SAT.2025.27},
  annote =	{Keywords: Satisfiability, parallel SAT solving, distributed computing, preprocessing}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.28
CNOT-Optimal Clifford Synthesis as SAT

Authors: Irfansha Shaik and Jaco van de Pol

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
Clifford circuit optimization is an important step in the quantum compilation pipeline. Major compilers employ heuristic approaches. While they are fast, their results are often suboptimal. Minimization of noisy gates, like 2-qubit CNOT gates, is crucial for practical computing. Exact approaches have been proposed to fill the gap left by heuristic approaches. Among these are SAT based approaches that optimize gate count or depth, but they suffer from scalability issues. Further, they do not guarantee optimality on more important metrics like CNOT count or CNOT depth. A recent work proposed an exhaustive search only on Clifford circuits in a certain normal form to guarantee CNOT count optimality. But an exhaustive approach cannot scale beyond 6 qubits. In this paper, we incorporate search restricted to Clifford normal forms in a SAT encoding to guarantee CNOT count optimality. By allowing parallel plans, we propose a second SAT encoding that optimizes CNOT depth. By taking advantage of flexibility in SAT based approaches, we also handle connectivity restrictions in hardware platforms, and allow for qubit relabeling. We have implemented the above encodings and variations in our open source tool Q-Synth. In experiments, our encodings significantly outperform existing SAT approaches on random Clifford circuits. We consider practical VQE and Feynman benchmarks to compare with TKET and Qiskit compilers. In all-to-all connectivity, we observe reductions up to 32.1% in CNOT count and 48.1% in CNOT depth. Overall, we observe better results than TKET in the CNOT count and depth. We also experiment with connectivity restrictions of major quantum platforms. Compared to Qiskit, we observe up to 30.3% CNOT count and 35.9% CNOT depth further reduction.
Cite as

Irfansha Shaik and Jaco van de Pol. CNOT-Optimal Clifford Synthesis as SAT. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 28:1-28:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{shaik_et_al:LIPIcs.SAT.2025.28,
  author =	{Shaik, Irfansha and van de Pol, Jaco},
  title =	{{CNOT-Optimal Clifford Synthesis as SAT}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{28:1--28:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.28},
  URN =		{urn:nbn:de:0030-drops-237621},
  doi =		{10.4230/LIPIcs.SAT.2025.28},
  annote =	{Keywords: Circuit Synthesis, Circuit Optimization, Quantum Circuits, Propositional Satisfiability, Parallel Plans, Clifford Circuits, Encodings}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.25
QRP+Gen: A Framework for Checking Q-Resolution Proofs with Generalized Axioms

Authors: Mark Peyrer and Martina Seidl

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
Q-resolution is a proof system for quantified Boolean formulas (QBFs) that forms the foundation for search-based QBF solvers with clause and cube learning. To derive stronger clauses and cubes, Q-resolution was extended with so-called generalized axioms. The derivation of such generalized axioms relies on solving oracles that could be, for example, SAT solvers or even QBF solvers. While the correctness of results obtained with classical QCDCL-based solving can be efficiently certified by an independent checker, until now, proof generation had to be turned off to benefit from generalized axioms. Consequently, the results obtained with reasoning under generalized axioms could not be certified independently. To overcome this restriction, we present QRP+Gen, a novel framework to automatically generate and check Q-resolution proofs that contain generalized axioms. To this end, we extended the Q-resolution format QRP such that all necessary information is included to verify the correctness of generalized axioms. Our extension allows to integrate certificates produced by any oracle which can produce automatically checkable proofs. Furthermore, we developed a proof checker that orchestrates the proof checking of the core Q-resolution proof and the proofs produced by the oracles. As a case study, we equipped the search-based QBF solver DepQBF with proof-producing oracles for the SAT-based techniques trivial truth and trivial falsity.
Cite as

Mark Peyrer and Martina Seidl. QRP+Gen: A Framework for Checking Q-Resolution Proofs with Generalized Axioms. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 25:1-25:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{peyrer_et_al:LIPIcs.SAT.2025.25,
  author =	{Peyrer, Mark and Seidl, Martina},
  title =	{{QRP+Gen: A Framework for Checking Q-Resolution Proofs with Generalized Axioms}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{25:1--25:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.25},
  URN =		{urn:nbn:de:0030-drops-237592},
  doi =		{10.4230/LIPIcs.SAT.2025.25},
  annote =	{Keywords: Automated Reasoning, Quantified Resolution Proof, Generalized Axioms}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.16
Depth-Optimal Quantum Layout Synthesis as SAT

Authors: Anna B. Jakobsen, Anders B. Clausen, Jaco van de Pol, and Irfansha Shaik

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
Quantum circuits consist of gates applied to qubits. Current quantum hardware platforms impose connectivity restrictions on binary CX gates. Hence, Layout Synthesis is an important step to transpile quantum circuits before they can be executed. Since CX gates are noisy, it is important to reduce the CX count or CX depth of the mapped circuits. We provide a new and efficient encoding of Quantum-circuit Layout Synthesis in SAT. Previous SAT encodings focused on gate count and CX-gate count. Our encoding instead guarantees that we find mapped circuits with minimal circuit depth or minimal CX-gate depth. We use incremental SAT solving and parallel plans for an efficient encoding. This results in speedups of more than 10-100x compared to OLSQ2, which guarantees depth-optimality. But minimizing depth still takes more time than minimizing gate count with Q-Synth. We correlate the noise reduction achieved by simulating circuits after (CX)-count and (CX)-depth reduction. We find that minimizing for CX-count correlates better with reducing noise than minimizing for CX-depth. However, taking into account both CX-count and CX-depth provides the best noise reduction.
Cite as

Anna B. Jakobsen, Anders B. Clausen, Jaco van de Pol, and Irfansha Shaik. Depth-Optimal Quantum Layout Synthesis as SAT. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{jakobsen_et_al:LIPIcs.SAT.2025.16,
  author =	{Jakobsen, Anna B. and Clausen, Anders B. and van de Pol, Jaco and Shaik, Irfansha},
  title =	{{Depth-Optimal Quantum Layout Synthesis as SAT}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{16:1--16:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.16},
  URN =		{urn:nbn:de:0030-drops-237501},
  doi =		{10.4230/LIPIcs.SAT.2025.16},
  annote =	{Keywords: Quantum Layout Synthesis, Transpiling, Circuit Mapping, Incremental SAT, Parallel Plans}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.24
Validation of QBF Encodings with Winning Strategies

Authors: Irfansha Shaik, Maximilian Heisinger, Martina Seidl, and Jaco van de Pol

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
When using a QBF solver for solving application problems encoded to quantified Boolean formulas (QBFs), mainly two things can potentially go wrong: (1) the solver could be buggy and return a wrong result or (2) the encoding could be incorrect. To ensure the correctness of solvers, sophisticated fuzzing and testing techniques have been presented. To ultimately trust a solving result, solvers have to provide a proof certificate that can be independently checked. Much less attention, however, has been paid to the question how to ensure the correctness of encodings. The validation of QBF encodings is particularly challenging because of the variable dependencies introduced by the quantifiers. In contrast to SAT, the solution of a true QBF is not simply a variable assignment, but a winning strategy. For each existential variable x, a winning strategy provides a function that defines how to set x based on the values of the universal variables that precede x in the quantifier prefix. Winning strategies for false formulas are defined dually. In this paper, we provide a tool for validating encodings using winning strategies and interactive game play with a QBF solver. As the representation of winning strategies can get huge, we also introduce validation based on partial winning strategies. Finally, we employ winning strategies for testing if two different encodings of one problem have the same solutions.
Cite as

Irfansha Shaik, Maximilian Heisinger, Martina Seidl, and Jaco van de Pol. Validation of QBF Encodings with Winning Strategies. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 24:1-24:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{shaik_et_al:LIPIcs.SAT.2023.24,
  author =	{Shaik, Irfansha and Heisinger, Maximilian and Seidl, Martina and van de Pol, Jaco},
  title =	{{Validation of QBF Encodings with Winning Strategies}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{24:1--24:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.24},
  URN =		{urn:nbn:de:0030-drops-184863},
  doi =		{10.4230/LIPIcs.SAT.2023.24},
  annote =	{Keywords: QBF, Validation, Winning Strategy, Equivalence, Certificates}
}
  • Refine by Type
  • 6 Document/PDF
  • 5 Document/HTML

  • Refine by Publication Year
  • 5 2025
  • 1 2023

  • Refine by Author
  • 3 Shaik, Irfansha
  • 3 van de Pol, Jaco
  • 2 Seidl, Martina
  • 1 Biere, Armin
  • 1 Chu, Zhufei
  • Show More...

  • Refine by Series/Journal
  • 6 LIPIcs

  • Refine by Classification
  • 2 Computing methodologies → Planning for deterministic actions
  • 2 Hardware → Quantum computation
  • 1 Computing methodologies → Artificial intelligence
  • 1 Hardware → Theorem proving and SAT solving
  • 1 Mathematics of computing → Combinatorial optimization
  • Show More...

  • Refine by Keyword
  • 2 Parallel Plans
  • 1 Automated Reasoning
  • 1 Boolean satisfiability problem
  • 1 Certificates
  • 1 Circuit Mapping
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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