DROPS

Artifact

Software

eSLIM

Authors: Franz-Xaver Reichl, Friedrich Slivovsky, and Stefan Szeider

Abstract

Cite as

Franz-Xaver Reichl, Friedrich Slivovsky, Stefan Szeider. eSLIM (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22464,
   title = {{eSLIM}}, 
   author = {Reichl, Franz-Xaver and Slivovsky, Friedrich and Szeider, Stefan},
   note = {Software, This work was supported by the Vienna Science and Technology Fund (WWTF) under grant 10.47379/ICT19060, and the Austrian Science Fund (FWF) under grant 10.55776/W1255., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:9d2862aedfe458cfb06d4d43da6c0f46ed578c91;origin=https://github.com/fxreichl/eSLIM;visit=swh:1:snp:ebfe92c3c6e3f45b9d69b59b4a1873264e9dcebd;anchor=swh:1:rev:779e64b93465754590fc1321d595ed48c8e39587}{\texttt{swh:1:dir:9d2862aedfe458cfb06d4d43da6c0f46ed578c91}} (visited on 2024-11-28)},
   url = {https://github.com/fxreichl/eSLIM},
   doi = {10.4230/artifacts.22464},
}

Document

DOI: 10.4230/LIPIcs.SAT.2024.23

eSLIM: Circuit Minimization with SAT Based Local Improvement

Authors: Franz-Xaver Reichl, Friedrich Slivovsky, and Stefan Szeider

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

Abstract

eSLIM is a tool for circuit minimization that utilizes Exact Synthesis and the SAT-based local improvement method (SLIM) to locally improve circuits. eSLIM improves upon the earlier prototype CIOPS that uses Quantified Boolean Formulas (QBF) to succinctly encode resynthesis of multi-output subcircuits subject to don't cares. This paper describes two improvements. First, it presents a purely propositional encoding based on a Boolean relation characterizing the input-output behavior of the subcircuit under don't cares. This allows the use of a SAT solver for resynthesis, substantially reducing running times when applied to functions from the IWLS 2023 competition, where eSLIM placed second. Second, it proposes circuit partitioning techniques in which don't cares for a subcircuit are captured only with respect to an enclosing window, rather than the entire circuit. Circuit partitioning trades completeness for efficiency, and successfully enables the application of exact synthesis to some of the largest circuits in the EPFL suite, leading to improvements over the current best implementation for several instances.

Cite as

Franz-Xaver Reichl, Friedrich Slivovsky, and Stefan Szeider. eSLIM: Circuit Minimization with SAT Based Local Improvement. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 23:1-23:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{reichl_et_al:LIPIcs.SAT.2024.23,
  author =	{Reichl, Franz-Xaver and Slivovsky, Friedrich and Szeider, Stefan},
  title =	{{eSLIM: Circuit Minimization with SAT Based Local Improvement}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{23:1--23:14},
  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.23},
  URN =		{urn:nbn:de:0030-drops-205458},
  doi =		{10.4230/LIPIcs.SAT.2024.23},
  annote =	{Keywords: QBF, Exact Synthesis, Circuit Minimization, SLIM}
}

Document

DOI: 10.4230/LIPIcs.SAT.2022.20

Pedant: A Certifying DQBF Solver

Authors: Franz-Xaver Reichl and Friedrich Slivovsky

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

Abstract

Pedant is a solver for Dependency Quantified Boolean Formulas (DQBF) that combines propositional definition extraction with Counterexample-Guided Inductive Synthesis (CEGIS) to compute a model of a given formula. Pedant 2 improves upon an earlier version in several ways. We extend the notion of dependencies by allowing existential variables to depend on other existential variables. This leads to more and smaller definitions, as well as more concise repairs for counterexamples. Additionally, we reduce counterexamples by determining minimal separators in a conflict graph, and use decision tree learning to obtain default functions for undetermined variables. An experimental evaluation on standard benchmarks showed a significant increase in the number of solved instances compared to the previous version of our solver.

Cite as

Franz-Xaver Reichl and Friedrich Slivovsky. Pedant: A Certifying DQBF Solver. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 20:1-20:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{reichl_et_al:LIPIcs.SAT.2022.20,
  author =	{Reichl, Franz-Xaver and Slivovsky, Friedrich},
  title =	{{Pedant: A Certifying DQBF Solver}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{20:1--20:10},
  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.20},
  URN =		{urn:nbn:de:0030-drops-166941},
  doi =		{10.4230/LIPIcs.SAT.2022.20},
  annote =	{Keywords: DQBF, DQBF Solver, Decision Procedure, Certificates}
}

Search Results

Documents authored by Reichl, Franz-Xaver

eSLIM

Abstract

Cite as

eSLIM: Circuit Minimization with SAT Based Local Improvement

Abstract

Cite as

Pedant: A Certifying DQBF Solver

Abstract

Cite as

Thanks for your feedback!

Could not send message