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)]$


  • $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.

1 Answer 1


Your problem is PSPACE-complete:

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']

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<t'\leq x$, and then we could directly jump at time $t$ from $j(t)$ to $j(t'+1)$ and reach the threshold sooner.


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.

  • $\begingroup$ could you explain how you build $S$ to accept when $j \to j'$ is a valid transition? $\endgroup$ Sep 8, 2022 at 11:51
  • 1
    $\begingroup$ 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. $\endgroup$
    – Denis
    Sep 8, 2022 at 11:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.