<p>Your problem is PSPACE-complete:</p>
<p><strong>Membership in PSPACE via a nondeterministic PSPACE algorithm:</strong></p>
<pre><code>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'
}
</code></pre>
<p>You can also remark that the threshold <span class="math-container">$x$</span> never needs to be more than <span class="math-container">$2^n$</span>, otherwise you have <span class="math-container">$j(t)=j(t')$</span> for some <span class="math-container">$t&lt;t'\leq x$</span>, and then we could directly jump at time <span class="math-container">$t$</span> from <span class="math-container">$j(t)$</span> to <span class="math-container">$j(t'+1)$</span> and reach the threshold sooner.</p>
<p><strong>PSPACE-hardness</strong>:</p>
<p>Let <span class="math-container">$M$</span> be a PSPACE Turing Machine running in space <span class="math-container">$p(n)$</span>. A configuration of <span class="math-container">$M$</span> is the content of the tape, and the position and state of the reading head. You can encode such a configuration via a list <span class="math-container">$j$</span> of <span class="math-container">$N=k\cdot p(n)$</span> boolean variables, using a fixed number <span class="math-container">$k$</span> of variables per tape cell. This <span class="math-container">$k$</span> depends on the alphabet and number of states of <span class="math-container">$M$</span>: for each cell the <span class="math-container">$k$</span> bits tell you the letter in the cell, and whether the reading head is present there in some state <span class="math-container">$q$</span>. Then, it suffices to have <span class="math-container">$I[j]$</span> accept iff <span class="math-container">$j$</span> is the initial configuration, and <span class="math-container">$S[j,j']$</span> accepts in these three cases: either <span class="math-container">$j\to j'$</span> is a valid transition, or <span class="math-container">$j$</span> is an accepting configuration and <span class="math-container">$j'=0^N$</span>, or <span class="math-container">$j=j'=0^N$</span>.
This way, your instance is satisfiable iff <span class="math-container">$M$</span> accepts, so you've encoded an arbitrary PSPACE problem as an instance of your satisfiability problem.</p>

CC BY-SA 4.0
2022-09-08T11:51:05.813Z
could you explain how you build $S$ to accept when $j \to j'$ is a valid transition?
user1868607
CC BY-SA 4.0
2022-09-08T11:55:38.307Z
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.
Denis
CC BY-SA 4.0
2022-09-07T23:57:42.010Z
2022-09-08T12:15:26.530Z
2022-09-08T12:15:26.530Z
Denis
<p>I'm interested in the complexity of deciding satisfiability of the following family of formulae:</p>
<p><span class="math-container">$\exists j. I[j(0)] \land \forall t. S[j(t),j(t+1)]$</span></p>
<p>where:</p>
<ul>
<li><span class="math-container">$j:\mathbb{N} \to \{0,1\}^n$</span> has finite support, that is, there exists some <span class="math-container">$x$</span> such that <span class="math-container">$j(l) = 0^n$</span> for all <span class="math-container">$l \ge x$</span>.</li>
<li><span class="math-container">$I, S$</span> are propositional formulae.</li>
<li><span class="math-container">$t$</span> is a &quot;temporal&quot; variable to be interpreted over the natural numbers.</li>
</ul>

<cc.complexity-theory><lo.logic><temporal-logic>
Complexity of "discrete-time" SAT
user1868607
# Complexity of "discrete-time" SAT

(Asked by: username_0 on 2022-09-07)

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.

**Tags:** cc.complexity-theory, lo.logic, temporal-logic

---

## 1 answers

### Answer by username_1 on 2022-09-07. Score: 4 | Accepted answer

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

> **Comments:**
> **username_0**: could you explain how you build $S$ to accept when $j \to j'$ is a valid transition?  
> **username_1**: 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.  

---

