Publication result detail

Antichain with SAT and Tries

VARGOVČÍK, P.; HOLÍK, L.

Original Title

Antichain with SAT and Tries

English Title

Antichain with SAT and Tries

Type

Paper in proceedings outside WoS and Scopus

Original 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.

English 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.

Keywords

SAT, alternating automata, antichain, trie

Key words in English

SAT, alternating automata, antichain, trie

Authors

VARGOVČÍK, P.; HOLÍK, L.

RIV year

2025

Released

27.08.2024

Publisher

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

Location

Dagstuhl

ISBN

978-3-95977-334-8

Book

27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Edition

Leibniz International Proceedings in Informatics (LIPIcs)

ISBN

1868-8969

Periodical

Leibniz International Proceedings in Informatics

Volume

2024

Number

305

State

Federal Republic of Germany

Pages from

1

Pages to

15

Pages count

15

URL

https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.15

BibTex

@inproceedings{BUT194224,
  author="Pavol {Vargovčík} and Lukáš {Holík}",
  title="Antichain with SAT and Tries",
  booktitle="27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)",
  year="2024",
  series="Leibniz International Proceedings in Informatics (LIPIcs)",
  journal="Leibniz International Proceedings in Informatics",
  volume="2024",
  number="305",
  pages="1--15",
  publisher="Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
  address="Dagstuhl",
  doi="10.4230/LIPIcs.SAT.2024.15",
  isbn="978-3-95977-334-8",
  url="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.15"
}