This is the second of the two proofs in Schaefer’s paper that will get us the Sift reduction.
The problem: Avoidance Truth Assignment. (My name for it). This problem does not appear in the G&J appendix. It is named “Gavoid (POS CNF)” in Schaefer’s paper.
The description: Given a CNF formula with no negated literals (and not necessarily 3 literals per clause), players take turns choosing a variable to make true. A player loses if after their play the formula becomes true, even if all unchosen variables are set to false. Does player 1 have a forced win?
Example: Suppose the formula was (x1 ∨ x2) ∧ (x1 ∨ x3) ∧ (x2 ∨ x3 ∨ x4). Then player 1 could force a win by choosing x2, which makes clauses 1 and 3 true. The player who chooses x3 will lose, so player 2 should pick one of x2 or x4. But then player 1 chooses the other, leaving player 2 forced to pick x3, making the second clause (and the whole formula) true.
Reduction: Schaefer reduces from Pre-Partitioned Truth Assignment. So we start with a logical formula given as a set of clauses, and the variables are partitioned into two sets, one for each player. We’ll call player 1’s variables x1 .. xn and player 2’s variables y1 through yn. We’ll assume (or modify the formula to make it happen) that each clause contains at least one x variable, and that every variable occurs both positively and negatively as a literal someplace in the formula.
Our new formula will have:
- 4 copies of each variable (xi turns into xi, ~xi, xi‘, and ~xi‘
- One clause (xi ∨ ~xi) for each x variable
- One clause (yi ∨ ~yi ∨ yi‘) for each y variable
- For each clause in the original formula: if it contains an unnegated variable xi (or yi), then our new clause will contain xi and xi‘. (Or yi and yi‘). If it contains a negated literal, we’ll use the 2 “negated” variables instead. This clause will probably have more than 3 elements in it, but that’s ok.
Shaefer notes that if we hit a point in the game where we have:
- An even number of unplayed variables, and
- An odd number of unplayed distinct variables remaining in every clause.
- An odd number of unplayed variables, and
- An even number of unplayed distinct variables remaining in every clause
..then the player who’s turn it is can win by picking some unsatisfied clause and picking any variable that does not satisfy it. So the strategy for the first player is to create the first situation (by satisfying all clauses with an even number of variables), and the strategy for the second player is to create the second situation (by satisfying all clauses with an odd number of variables). Since the first kind of clause we made (with the x variables) has an even number of variables, player 1 will want to satisfy those clauses as fast as possible. Similarly, since the second kind of clause we made (with the y variables) has an odd number of variables, palyer 2 will want to satisfy those clauses as quickly as possible. If this happens, we are exactly imitating the Pre-Partitioned Truth Assignment game.
The remainder of the reduction is a detailed proof explaining the above argument in detail (showing, for example, what happens when players do not play this way).
Difficulty: 8 Maybe they’re getting a little easier for me because I’ve been doing so much of them. Or maybe because I’m still skipping all of the low-level details.