# SAT Solver Front-End: Strategy to order Quantifiers

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. • Welcome to CS.SE! Nice question! Not an answer to your question, but a small note: Existential quantifiers at outermost scope can be handled through Skolemazation. In other words,$\exists x \in S . f(x)$is satisfiable iff$x \in S \land f(x)$is satisfiable. If you choose an appropriate encoding of each logic variable $x into boolean variables $x_1,\dots,x_k$, this means that existential quantifiers at outermost scope are almost free.
– D.W.
Mar 17 '18 at 16:08