Transcript On a random walk strategy for the Q2SAT problem

On a random walk strategy for the
Q2SAT problem
K. Subramani
Topics to be covered
1.
2.
3.
4.
5.
6.
7.
8.
9.
Definitions of 2SAT and Q2SAT problems
2 player games
Motivation
Related Work
The random walk algorithm for 2SAT
Analysis of Papadimitriou`s algorithm
Prerequisites for coin-flipping to work
How Q2SAT meets those prerequisites
Conclusion
2SAT and Q2SAT
• Given a Boolean formula
  C1  C2  C3...... Cm
where each clause has at most 2 literals from
the variable set {x1, x2, …xn}, the 2SAT
problem is to check whether this formula has
a satisfying assignment.
2SAT and Q2SAT (contd.)
• Given a Boolean formula
  C1  C2  C3...... Cm
and a quantifier string Q(x,y)
where each clause has at most 2 literals from
the variable set {x1, x2, …xn, y1,y2,…yn}, the Q2SAT
problem is to check whether the formula Q(x,y) 
a satisfying model
has
2 player games
1. Let X be the Existential player and Y be the Universal
player.
2. Assume without loss of generality that all x variables
are existentially quantified and the y variables are universally quantified.
3. Each player makes a sequence of moves non-deterministically in the order specified by Q(x,y).
4. A move is a true/false guess.
5. If at the end of the moves, the expression evaluates to
true, we say that X has a winning strategy and this
strategy is called a model for Q(x,y) 
2 Player games (contd.)
So the QBF problem in general, is to decide whether
the existential player has a winning strategy.
Motivation
1.
2.
3.
4.
5.
Algorithmic elegance.
How much can a simple strategy net us?
Deeper understanding of game theory.
First use of randomization to study QBF feasibility.
Papadimitriou got a FOCS paper out of his 2SAT
random walk algorithm! [Pap91]
Related Work
1. [Pap91] introduced the random walk algorithm for simple
2SAT.
2. [WS02] applies the random walk technique to 3SAT
problems with good empirical results.
3. Even for HornSAT (which is in P), the random walk
algorithm does not converge in a polynomial number of
steps (analytically).
(For a pathological example, see [Ros00].)
4. [APT79] solves both 2SAT and Q2SAT in linear time,
using connected components of the implication graph.
Related Work (contd.)
5. I am working on strategies which enhance
simple random walk with “greed”, i.e.,
selecting the unsatisified clause with the
fewest number of literals to fix. It works for
HornSAT, but HornSAT has an extremely
simple deterministic algorithm.
The random walk algorithm for 2SAT
Start with a random assignment for  .
If all clauses are satisfied stop.
Pick a clause which is not satisfied.
Pick one of the 2 literals in this clause at
random and `flip´ it.
5. Repeat steps (2)-(5) for 2n2 steps.
6. Say that the formula is `probably unsatisfiable.´
1.
2.
3.
4.
Analysis
Let us say that the given formula is satisfiable and focus on
a specific satisfying assignment T.
Let the initial random assignment be T´, which does
not satisfy 
Now consider a clause C which is violated by T´.
At least one of the 2 literals in C must be true in T.
Therefore flipping a literal at random results in T´getting
closer to T, with probability at least one half. Likewise,
T´could be moving away from T, with probability one
half.
Analysis (contd.)
Let Xi denote the number of flips required by the above
algorithm, assuming that the current assignment
differs from T in exactly i variables. We use the
probability law:
E[X] = E[E[X| Y]] (see [Ros00]) to conclude that
E[Xi]= ½ (E[Xi-1]+1)+ ½ (E[X i+1]+1)
Also note that E[X0]=0 and E[Xn]=1+E[X n-1], since if
by chance we start off with the correct assignment, no
flips are required, whereas if all variables are incorrect,
then a flip must move us in the right direction!
Analysis (contd.)
The above system can be solved to get
E[Xn] = n2.
Now applying Markov´s law, we can conclude
that the probability that more than 2.n2 flips
will be required is less than ½.
Prerequisites for flipping to work
1. A literal must be flippable, i.e., there are exactly 2 values
to assign to it. (Y1)
2. When a literal is flipped with probability at least one
half, we move in the right direction, and with probability
at most one half, we move in the wrong direction. (Y2)
Y1 is trivially met in existential first order logic, by all
SAT formulas, since every variable is either true or false.
However, Y2 fails for even HornSAT!
Why Q2SAT meets the prerequisites
First observe that if Y1 is met by Q2SAT then Y2 is
trivially met, since under the current assignment both
literals have been set incorrectly (assuming that both
variables are existentially quantified) and with probability
at least ½, we will move in the right direction by choosing
one at random.
Why Q2SAT meets the prerequisites
I have provided a detailed explanation of Page 4 and
Page 5 of my paper of how Y1 is met by Q2CNF formulas.
The main idea is that Q2SAT problems are guaranteed
to have simple models, if satisfiable, i.e.,
a model in which each existentially quantified variable
is either true, false, or yi or the complement of yi,
where yi is a universally quantified variable preceding
it.
Why Q2SAT meets the prerequisites
A linear scan of the clause set cuts these choices to precisely
two. We are now free to use Papadimitriou´s algorithm
and the accompanying analysis!
Conclusion
A number of interesting problems are currently open,
insofar as randomized approaches are concerned:
(a) Boolean equivalence, i.e., given 2 2CNF formulas,
do they have the same set of satisfying assignments?
(b) UNIQUE2SAT – Does a 2CNF formula have exactly
one satisfying assignment?
(c) CRITICAL2SAT – Is a 2CNF formula unsatisfiable,
but knocking off any clause makes it satisfiable?