Antichain with SAT and Tries

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F24%3APU155308" target="_blank" >RIV/00216305:26230/24:PU155308 - isvavai.cz</a>

Result on the web

<a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.15" target="_blank" >https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.15</a>

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Antichain with SAT and Tries

Original language description

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.

Czech name

—

Czech description

—

Type

O - Miscellaneous

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/LL1908" target="_blank" >LL1908: Efficient Finite Automata for Automated Reasoning</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Publication year

2024

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů