Detail výsledku
Antichain with SAT and Tries
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.
SAT, alternating automata, antichain, trie
Zavádíme SAT-verzi antichainového algoritmu pro kontrolu jazykové prázdnoty střídavých konečných automatů (AFA) se složitými přechodovými relacemi zakódovanými jako kompaktní logické formule. Řešitel SAT se používá k výpočtu předchůdců konfigurací AFA a zároveň k výpočtu jejich před zároveň k vyhodnocení subsumpce nově nalezených konfigurací v antiřetězci dříve nalezených konfigurací. Algoritmus lze naivně implementovat pomocí inkrementálního SAT solveru, kde je rostoucí antiřetězec reprezentován přidáváním nových klauzulí. Abychom jej zefektivnili, 1) vynutíme si SAT řešitele, aby upřednostňoval největší/nejsilnější předchůdce (takže slabší konfigurace se ani negenerují), a 2) ukládáme klauzule antiřetězce do speciální varianty tria, která umožňuje rychlé testování subsumpce. Experimentální výsledky naznačují, že výsledná kontrola prázdnoty je velmi efektivní ve srovnání se současným stavem techniky a že naše techniky zlepšují výkonnost SAT řešiče.
@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, LIPIcs",
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",
issn="1868-8969",
url="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.15"
}Reliable, Secure, and Intelligent Computer Systems, VUT, Vnitřní projekty VUT, FIT-S-23-8151, zahájení: 2023-03-01, ukončení: 2026-02-28, řešení
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)