Publication Details
Antiprenexing for WSkS: A Little Goes a Long Way
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Lengál Ondřej, Ing., Ph.D. (DITS)
Valeš Ondřej, Ing.
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
antiprenexing, automata, preprocessing, weak monadic second-order logic, WSkS
We study light-weight techniques for preprocessing of WSkS formulae in an
automata-based decision procedure as implemented, e.g., in Mona. The techniques
we use are based on antiprenexing, i.e., pushing quantifiers deeper into
a formula. Intuitively, this tries to alleviate the explosion in the size of the
constructed automata by making it happen sooner on smaller automata (and have the
automata minimization reduce the output). The formula transformations that we use
to implement antiprenexing may, however, be applied in different ways and extent
and, if used in an unsuitable way, may also cause an explosion in the size of the
formula and the automata built while deciding it. Therefore, our approach uses
informed rules that use an estimation of the cost of constructing automata for
WSkS formulae. The estimation is based on a model learnt from runs of the
decision algorithm on various formulae. An experimental evaluation of our
technique shows that antiprenexing can significantly boost the performance of the
base WSkS decision procedure, sometimes allowing one to decide formulae that
could not be decided before.
@inproceedings{BUT168130,
author="Vojtěch {Havlena} and Lukáš {Holík} and Ondřej {Lengál} and Ondřej {Valeš} and Tomáš {Vojnar}",
title="Antiprenexing for WSkS: A Little Goes a Long Way",
booktitle="EPiC Series in Computing",
year="2020",
series="Proceedings of LPAR-23",
number="73",
pages="298--316",
publisher="EasyChair",
address="Manchester",
doi="10.29007/6bfc",
issn="2398-7340",
url="https://www.fit.vut.cz/research/publication/12287/"
}