SAT Solver Front-End: Strategy to order Quantifiers

Question

I am working on a small project. The goal is to implement a compiler from a quite simple, custom syntax of logical formulae (including variables over finite domains) to conjunctive normal form (CNF). The compiler should for every formula $\varphi$ from the custom language produce a standard propositional formula in conjunctive normal form (CNF), $\text{cnf}(\varphi)$.

Desiderata:

• The size of $\text{cnf}(\varphi)$ should be as small as possible compared to the size of $\varphi$.
• The two formulae $\text{cnf}(\varphi)$ and $\varphi$ should be equisatisfiable.
• For every model of $\text{cnf}(\varphi)$ it should be possible to construct a model of $\varphi$. I am not entirely sure whether that is the correct term, but I would consider the models of $\text{cnf}(\varphi)$ conservative extensions of $\varphi$. The algorithm outlined below ensures this.

Input

The input contains the usual logical connectives, terms as constants and terms as integers (with some arithmetic). Further, it may contain universal and existential quantifications of the following form:

(forall $x in {a, b} (exists $y in {$x, c} (p($x,$y))))

As you can see, variables are associated with (finite) domains. A semantically equivalent ground formula in this case would be:

((p(a,a) | p(a,c)) & (p(b,b) | p(b,c)))

A more complex example which encodes the "subgrid constraint" of sudoku:

(forall #d in [0...8]
    (forall #ro in [0...2]
        (forall #co in [0...2]
            (forall #i in [0...7]
                (forall #i1 in [#i+1...8]
                    (
                        v(((3*#ro) + (#i/3)), ((3*#co) + (#i%3)), #d)
                        ->
                        ~v(((3*#ro) + (#i1/3)), ((3*#co) + (#i1%3)), #d)
                    )
                )
            )
        )
    )
)

Conversion Algorithm

The conversion algorithm that I have implemented currently is as follows:

1. Replace all connectives with | (logical or) and & (logical and), and "push down" negation towards atoms. This yields a formula using only the two basic connectives in negation normal form (NNF).
2. Standardize variables apart, i.e. make sure that no two quantifications use the same variable name, globally.
3. "Pull out" the quantifiers, which yields a formula in prenex normal form (PNF), where the matrix is in negation normal form.
4. Expand universal quantifications into conjunctions and existential quantifications into disjunctions, to get a ground formula.
5. If the result of (4.) is in CNF, return it. Otherwise, apply Tseitin's transformation, to get a formula in CNF.

Issues and Question

I initially introduced step (3.) in order to be in a position to optimize the ordering of quantifiers in the matrix of the formula. Ideally, universal quantifiers should be "left" and existential quantifiers should be "right" in order to directly expand to CNF. There are some dependencies between quantifiers that prevent moving them over each other, but I think I got those conditions covered.

However, by introducing (3.) some of my test instances exploded. Since the connection between a quantifier and its scope is completely lost in step (3.), inevitably step (4.) will generate a huge cross product over all possible variable substitutions for all quantifiers, and for each of those, the whole formula will be ground and duplicated. This is clearly the wrong approach.

From here, I thought that it would be a good idea to go the other way and actually try to push quantifiers down, in order to minimize their scope. Then, for any clusters of quantifiers that are immediately next to each other in the formula, their order can be optimized.

My question is whether I am missing some trick that could help me, and especially what is the best (known) approach to reorder/move quantifiers. I found quite some information about QBF solving, but that does not help me much.

Edit: Since I asked this question I changed my approach. It turned out that targeting Prenex Normal Form actually was a very bad idea, since then the scope of all quantifiers is at least the size of the whole formula (except quantifiers). This just explodes. So instead of "pulling out" in step (3.) I now "push down" the quantifiers with the goal of minimizing their scope. If two quantifiers are then "next" to each other, I try to move universal quantifiers to the left and existenstial quantifiers to the right, since this way the expansion will be closer to CNF.

Answer 1

I don't think there is any way to compile efficiently to SAT. That's because your problem is (or contains) QBF, and QBF is believed to be harder than SAT: QBF is PSPACE-complete, whereas SAT is NP-complete, and it is widely believed that PSPACE != NP. If you found an efficient and general way to compile QBF formulas to SAT, then you would have proven PSPACE = NP, which seems unlikely.

What does your problem have to do with QBF? Well, we imagine that we restrict your formulas so they are over not just a finite domain, but a domain of size two. Moreover, we get rid of all integers. Then every variable is boolean, and you have boolean formula with quantifiers -- i.e., an instance of QBF.

Fortunately, there are QBF solvers. Unfortunately, they are significantly slower than SAT solvers. In any case, it looks like you should be using (or compiling to) a QBF solver, rather than a SAT solver. (If you're lucky, and there are only two alternating quantifiers, then your problem becomes 2QBF, which is considerably easier than QBF.)