Anatomy of Alternating Quantifier Satisfiability (Work in progress)

Phan Anh Dung, Nikolaj Bjørner, David Monniaux

    Research output: Contribution to conferencePaperResearchpeer-review

    184 Downloads (Pure)


    We report on work in progress to generalize an algorithm recently introduced in [10] for checking satisfiability of formulas with quantifier alternation. The algorithm uses two auxiliary procedures: a procedure for producing a candidate formula for quantifier elimination and a procedure for eliminating or partially eliminating quantifiers. We also apply the algorithm for Presburger Arithmetic formulas and evaluate it on formulas from a model checker for Duration Calculus [8]. We report on experiments on different variants of the auxiliary procedures. So far, there is an edge to applying SMT-TEST proposed in [10], while we found that a simpler approach which just eliminates quantified variables per round is almost as good. Both approaches offer drastic improvements to applying default quantifier elimination.
    Original languageEnglish
    Publication date2012
    Number of pages10
    Publication statusPublished - 2012
    Event10th International Workshop on Satisfiability Modulo Theories (SMT 2012) - Manchester, United Kingdom
    Duration: 30 Jun 20121 Jul 2012


    Workshop10th International Workshop on Satisfiability Modulo Theories (SMT 2012)
    CountryUnited Kingdom
    Internet address

    Fingerprint Dive into the research topics of 'Anatomy of Alternating Quantifier Satisfiability (Work in progress)'. Together they form a unique fingerprint.

    Cite this