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:

• Replace all connectives with | (logical or) and & (logical and), and "p

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.)

StackExchange Computer Science Q#89457, answer score: 3