TAOCP 7.2.2.2 Exercise 102

Section 7.2.2.2: Satisfiability

Exercise 102. [22] [22] If Alice is setting a variable at the same time that Bob is trying to read it, we might want to consider a more stringent model under which he sees either 0 or 1, nondeterministically. (E.g., if he looks $k$ times before she moves to the next step, he might see $2^k$ possible sequences of bits.) Explain how to handle this model of "flickering" variables by modifying the clauses of exercise 87.

Verified: no
Solve time: 1m53s

Solution

Exercise 87 represents a finite execution of a protocol by Boolean variables describing the values of signals and the control locations at successive instants. A clause in that construction has the form of a constraint on the next state, together with clauses forcing the next state to agree with the deterministic transition relation of the program.

The only change needed for a flickering variable is in the clauses that describe a read operation. Suppose that a variable $x$ has value $x_t$ in state $t$, and that a process reads $x$ while constructing the clauses for its transition from state $t$ to state $t+1$. In the original model, the read value is forced to equal $x_t$. If the process has a Boolean variable $r_t$ representing the value obtained by the read, the original clauses contain the equivalence

$$ r_t \iff x_t . $$

This equivalence is replaced by a nondeterministic choice. The read value must be either $0$ or $1$, independently of the current value of $x$, so the two clauses

$$ (r_t \vee \bar r_t) $$

and

$$ (\bar r_t \vee r_t) $$

are tautologies and impose no restriction. Equivalently, the clauses defining $r_t$ are deleted, and $r_t$ is treated as a fresh Boolean variable in the transition clauses. The variable $x_t$ continues to describe the actual stored value of the signal, but it no longer constrains the value observed by the reader.

For a transition whose guard depends on several reads, each read variable is replaced in the same way. If a step examines $k$ flickering variables, introduce fresh variables

$$ r_1,\ldots,r_k $$

for the observed values and remove the clauses that identify $r_i$ with the corresponding stored variables. The remaining transition clauses use $r_1,\ldots,r_k$ exactly as the original clauses used the ordinary read values.

This modification gives precisely the required model. Every execution allowed by the original model is still allowed, because a read variable may nondeterministically choose the value equal to the stored signal. Conversely, every satisfying assignment of the modified clauses specifies a sequence of observations $r_t$ and stored states $x_t$. Since every $r_t$ is an arbitrary Boolean value, it represents one possible outcome of the flickering read. The assignment therefore corresponds to an execution in which each read returns either $0$ or $1$ independently of the writer's simultaneous update.

The example in the statement also agrees with this construction. If Alice changes a variable while Bob reads it repeatedly $k$ times before Alice advances, the $k$ fresh read variables have two possible values each, giving

$$ 2^k $$

possible observation sequences. The SAT instance obtains exactly these possibilities because the clauses no longer identify the read variables with the changing stored variable.

Thus the bounded model checking clauses of exercise 87 are modified only by replacing deterministic read constraints with unconstrained Boolean read variables. The state-update clauses remain unchanged. ∎