Algorithms for Deciding Counting Quantifiers over Unary Predicates
Abstract
We study algorithms for fragments of first order logic ex- tended with counting quantifiers, which are known to be highly complex in general. We propose a fragment over unary predicates that is NP-complete and for which there is a nor- mal form where Counting Quantification sentences have a single Unary predicate, thus call it the CQU fragment. We provide an algebraic formulation of the CQU satisfiability problem in terms of Integer Linear Programming based on which two algorithms are proposed, a direct reduction to SAT instances and an Integer Linear Programming version extended with a column generation mechanism. The latter is shown to lead to a viable implementation and experiments shows this algorithm presents a phase transition behavior.
Cite
Text
Finger and De Bona. "Algorithms for Deciding Counting Quantifiers over Unary Predicates." AAAI Conference on Artificial Intelligence, 2017. doi:10.1609/AAAI.V31I1.11129Markdown
[Finger and De Bona. "Algorithms for Deciding Counting Quantifiers over Unary Predicates." AAAI Conference on Artificial Intelligence, 2017.](https://mlanthology.org/aaai/2017/finger2017aaai-algorithms/) doi:10.1609/AAAI.V31I1.11129BibTeX
@inproceedings{finger2017aaai-algorithms,
title = {{Algorithms for Deciding Counting Quantifiers over Unary Predicates}},
author = {Finger, Marcelo and De Bona, Glauber},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2017},
pages = {3878-3884},
doi = {10.1609/AAAI.V31I1.11129},
url = {https://mlanthology.org/aaai/2017/finger2017aaai-algorithms/}
}