From: mutation@dorsai.com (Florian Lengyel)
Subject: Loop invariants of satisfiability algorithms
Organization: The Dorsai Embassy +1.718.729.5018
X-Newsreader: Tin 1.1 PL4
Date: Thu, 8 Oct 1992 07:40:54 GMT


What are the possible loop invariants of an algorithm for the satisfiability of Boolean formulas in conjuntive normal form?

Consider a more general case of the problem: satisfiability of Boolean
expressions. Suppose that this algorithm is specified as follows:

	< "E" is a Boolean expression >
        < Invariant: I >
	< Bound: t >
        do B -> S od
	< E >

Under the assumption that the variables of the boolean expression E
can range over the state space of this algorithm, we have:

	1. The loop invariant I is total.
If not, then let (x_0, ... , x_{n-1}) be a point at which I is undefined,
and let E be the satisfiable formula y_i = x_i for 0 <= i < n. By the
correctness of the algorithm and the satisfiability of E, the algorithm
terminates in a state satisfying ~B /\ I /\ E, which contradicts the
assumption that I is undefined at the only point which satisfies E.

	2. The loop invariant I is identically true.

Suppose otherwise, then ~I is a satisfiable boolean expression. Taking
E = ~I, the algorithm terminates in a state satisfying ~B /\ I /\ ~I,
which is absurd.

	3. The predicate transformer which assigns to a Boolean
expression E the loop guard B has no satisfiable fixed points. 
If so, then taking E to be a fixed point of this predicate transformer,
if E were satisfiable then the algorithm would terminate in a state
satisfying ~B /\ I /\ E, or equivalently, since E is a fixed point,
~E /\ I /\ E, again a contradiction.

	With that in mind, I can state the question that I really
wanted to ask first:

        Given a specification of SAT, as follows:

	< E is a Boolean formula in cnf >
	< Invariant I >
	< Bound t>
	do B -> S od
	< E >

	What are the possible loop invariants I? In particular,
	is I identically true?

3. Above suggests to me that the only possible choice for the loop\
guard is ~E. In the case of the SAT algorithm above, without loss of
polynomial time, the loop guard can be strengthened to B /\ ~E.
If the loop invariant I is everywhere TRUE, then B can be taken to
be ~E. Here I will admit that I am assuming that ~B /\ I => E, so that
with I identically true, ~B => E. With B strengthened as above, we
have B => ~E; these implications together yield B <=> ~E.

If the loop invariant is identically true, and the loop guard is
actually the negation of the formula one is trying to satisfy, this
suggest to me that the SAT algorithm will have a worst case complexity
equal to the number of possible truth value assignments to a given
formula, to my mind at any ratem, because in maintaining the trivial
loop invariant I = TRUE, the SAT algorithm may enumerate any truth
value assignment to the formula E. Another way of looking at this is
that such a trivial invariant fails to favor one truth value assignment 
over any other during the execution of SAT. 

Actually, I glossed over a few details in 2. I was assuming that the
invariant I was unquantified. The presence of only existential
quantifiers in I does not present any obstacle: they could be
eliminated using skolem functions, which can be taken to be uniformizing
functions if one reasonably assumes that the matrix of I is com[putable.
With existential quantifiers out of the way, we are back to the same
argument as 2. This leads to the dichotomy:
 
	Either the loop invariant I is identiacally TRUE,
	or I contains at least one universal quantifier.

Now, I claim that if I contained a universal quantifier nontrivially,
then in fact no recursive algorithm could maintain I as an invariant.
I leave it to the reader to determine the effect of predicate transformers
such as assignment, if ... fi, and do ... od on the arithmetical
hierarchy to see why this would be the case.

I am interested in your comments, criticisms, in vast and far reaching
extensions of these modest results in which the extender can claim
full credit for conceiving all of them, or at least in generously
pointing out that I might have had a small part in their creation,
but most certainly not in their true and final form, and so on.
For the record, all of this is 
	(c) 1991, 1992 by Florian Lengyel.


-- 
MUTATION@DORSAI.COM
FLORIAN@NEOTERIC.COM
Xref: sparky comp.theory:2170 sci.math:13030