Antichain with SAT and Tries

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

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.

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.