DROPS

Artifact

Software

Abstract

Cite as

Pavol Vargovčík. AntiSAT (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

@misc{dagstuhl-artifact-22499,
   title = {{AntiSAT}}, 
   author = {Vargov\v{c}{\'\i}k, Pavol},
   note = {Software, version 0.1.0., Czech Ministry of Education, Youth and Sports ERC.CZ LL1908 FIT BUT FIT-S-23-8151, swhId: \href{https://archive.softwareheritage.org/swh:1:rev:5901055e699e7b95ba3dec63d11445fcd791f5de}{\texttt{swh:1:rev:5901055e699e7b95ba3dec63d11445fcd791f5de}} (visited on 2024-11-28)},
   url = {https://github.com/p4l1ly/antisat/tree/5901055e699e7b95ba3dec63d11445fcd791f5de},
   doi = {10.4230/artifacts.22499},
}

Document

DOI: 10.4230/LIPIcs.SAT.2024.15

Antichain with SAT and Tries

Authors: Lukáš Holík and Pavol Vargovčík

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

Abstract

We introduce a SAT-enabled version of an antichain algorithm for checking language emptiness of alternating finite automata (AFA) with complex transition relations encoded as compact logical formulae. The SAT solver is used to compute predecessors of AFA configurations, and at the same time, to evaluate the subsumption of newly found configurations in the antichain of the previously found ones. The algorithm could be naively implemented by an incremental SAT solver where the growing antichain is represented by adding new clauses. To make it efficient, we 1) force the SAT solver to prioritize largest/subsumption-strongest predecessors (so that weaker configurations are not even generated), and 2) store the antichain clauses in a special variant of a trie that allows fast subsumption testing. The experimental results suggest that the resulting emptiness checker is very efficient compared to the state of the art and that our techniques improve the performance of the SAT solver.

Cite as

Lukáš Holík and Pavol Vargovčík. Antichain with SAT and Tries. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 15:1-15:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{holik_et_al:LIPIcs.SAT.2024.15,
  author =	{Hol{\'\i}k, Luk\'{a}\v{s} and Vargov\v{c}{\'\i}k, Pavol},
  title =	{{Antichain with SAT and Tries}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{15:1--15:24},
  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.15},
  URN =		{urn:nbn:de:0030-drops-205372},
  doi =		{10.4230/LIPIcs.SAT.2024.15},
  annote =	{Keywords: SAT, Trie, Antichain, Alternating automata, Subset query}
}

Search Results

Documents authored by Vargovčík, Pavol

AntiSAT

Abstract

Cite as

Antichain with SAT and Tries

Abstract

Cite as

Thanks for your feedback!

Could not send message