Reward function: **This is the most involved part of the MDP. Given a sequence of 3**m literals of L**, the following** 3cnf **formula is considered:**

$$\begin{array}{c}{{C(l_{1}^{1},l_{2}^{1},l_{3}^{1},\ldots,l_{1}^{m},l_{2}^{m},l_{3}^{m})=}}\\ {{\{l_{1}^{1}\lor l_{2}^{1}\lor l_{3}^{1},\ldots,l_{1}^{m}\lor l_{2}^{m}\lor l_{3}^{m}\}.}}\end{array}$$

Given that the number of possible distinct clauses over L **is less than (2**n)
3**, any set**
of clauses can be represented as a sequence of 3m literals, where m **= (2**n)
3**. The**
function C encodes all sets of clauses over L **as sequences of literals.** The only sequences having reward different than zero are those composed of a sequence s of 3m literals of E**, followed by either** sat or unsat**, followed by a sequence** s
′ =
l1, . . . , ln, where each liis either xi or ¬xi**. Namely, the sequence (**s, unsat, s′**) has**
reward 2; the sequence (s,sat, s′) has reward 1 if the set of clauses C(s**) is not satisfied**
by the only model of s
′, and 2n+1 **otherwise;**
Note that most of the states have reward 0. While the expected **reward is calculated**
over all reached states, r **is defined in such a way that, if a state has nonzero reward, then** all previous and succeeding states have reward zero. The reward function r **is defined this** way for the sake of making the proof simpler; however, the expected reward is calculated over all states, including "intermediate" ones.

This MDP has a single optimal policy: execute A for 3m **times, then execute either** U
or S, and then execute a1, . . . , an. The choice between U and S **that gives the greatest**
expected reward depends on the result of the execution of A**. Namely, each possible result**
of the execution of the first 3m **actions corresponds to a set of clauses. The next action of** the optimal policy is U if the set is unsatisfiable and S **if it is satisfiable.**
This is the definition of the MDP M**. The instance of the next-action problem is**
composed of an MDP, a horizon in unary, a state, and an action, **and the problem is to** check whether the action is optimal in the state. The horizon we consider is T **= (2**n)
3+n+1, the state is the one s corresponding to the sequence of literals such that C(s**) = Π, and the** action is S. It is not possible to prove that the function f defined by f(Π) = hM**, T, s, S**i is a reduction from satisfiability to the next-action problem.

Theorem 1 If f(Π) = hM, T, s, Si, then M **has an unique (stationary or history-dependent)**
optimal policy w.r.t. the horizon T, and Π is satisfiable if and only if S is the action to execute from s in the optimal policy of M **with horizon** T.

Proof. All MDPs defined as above have policies with positive reward: **the policy of executing**
A3mU a1, . . . , an **has expected reward equal to 2, since all its leaves have reward 2 and all**
internal nodes have reward 0. Such a sequence of actions can be executed by a stationary policy because the history can be inferred from the current state.

The sequences of actions that end up in a state with a positive **reward are very similar**
to each other. Indeed, they all begin with 3m times the action A. Then, either U or S are executed, followed by the sequence a1, . . . , an**. The only difference between these sequences**
is this choice between U or S.

The optimal policies therefore execute A in the first 3m **time points, regardless of the**
generated state. They then execute either U or S, and then execute a1, . . . , an**. The choice**