Detail publikace

Antichain with SAT and Tries

VARGOVČÍK, P.; HOLÍK, L. Antichain with SAT and Tries. 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics, LIPIcs. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2024. p. 1-15. ISBN: 978-3-95977-334-8. ISSN: 1868-8969.
Název česky
Antiřetězce a stromovitosti pro AFA prázdnost
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Vargovčík Pavol, Ing. (UITS)
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
URL
Klíčová slova

SAT, alternující autoamty, antiřetězce, stromovitosti

Abstrakt

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.

Anotace

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.

Rok
2024
Strany
1–15
Časopis
Leibniz International Proceedings in Informatics, LIPIcs, roč. 2024, č. 305, ISSN 1868-8969
Sborník
27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Řada
Leibniz International Proceedings in Informatics (LIPIcs)
Konference
The 27th International Conference on Theory and Applications of Satisfiability Testing, Pune, IN
ISBN
978-3-95977-334-8
Vydavatel
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Místo
Dagstuhl
DOI
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, 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"
}
Nahoru