# Complexity of "discrete-time" SAT

I'm interested in the complexity of deciding satisfiability of the following family of formulae:

$$\exists j. I[j(0)] \land \forall t. S[j(t),j(t+1)]$$

where:

• $$j:\mathbb{N} \to \{0,1\}^n$$ has finite support, that is, there exists some $$x$$ such that $$j(l) = 0^n$$ for all $$l \ge x$$.
• $$I, S$$ are propositional formulae.
• $$t$$ is a "temporal" variable to be interpreted over the natural numbers.

Membership in PSPACE via a nondeterministic PSPACE algorithm:

verify that S[0^n,0^n] is true
guess j such that I[j]
while(j != 0^n ){
guess j' such that S[j,j']
j:=j'
}


You can also remark that the threshold $$x$$ never needs to be more than $$2^n$$, otherwise you have $$j(t)=j(t')$$ for some $$t, and then we could directly jump at time $$t$$ from $$j(t)$$ to $$j(t'+1)$$ and reach the threshold sooner.

PSPACE-hardness:

Let $$M$$ be a PSPACE Turing Machine running in space $$p(n)$$. A configuration of $$M$$ is the content of the tape, and the position and state of the reading head. You can encode such a configuration via a list $$j$$ of $$N=k\cdot p(n)$$ boolean variables, using a fixed number $$k$$ of variables per tape cell. This $$k$$ depends on the alphabet and number of states of $$M$$: for each cell the $$k$$ bits tell you the letter in the cell, and whether the reading head is present there in some state $$q$$. Then, it suffices to have $$I[j]$$ accept iff $$j$$ is the initial configuration, and $$S[j,j']$$ accepts in these three cases: either $$j\to j'$$ is a valid transition, or $$j$$ is an accepting configuration and $$j'=0^N$$, or $$j=j'=0^N$$. This way, your instance is satisfiable iff $$M$$ accepts, so you've encoded an arbitrary PSPACE problem as an instance of your satisfiability problem.

• could you explain how you build $S$ to accept when $j \to j'$ is a valid transition? Sep 8, 2022 at 11:51
• You can do a big disjunction, where each disjunct expresses that a transition $\delta$ is being performed at a position $p$ of the tape. Such a disjunct just needs to say that the variables encoding the positions $p-1,p,p+1$ match the transition $\delta$, and all other variables are identical between $j$ and $j'$. The whole formula has polynomial size, since you have polynomially many possible pairs $(p,\delta)$. The part about other positions being left unchanged can actually be shared between all disjuncts, no need to repeat it. Sep 8, 2022 at 11:55