Descriptive complexity of 3SAT

Question

lately I'm reading about descriptive complexity, which I find is a fascinating branch of computational complexity. I found many formulas in $\exists$$SO$ that describe problems with graphs but none that describes the 3SAT language.

Thinking about it, I came to an "atomic" description like this:

$\exists$$v$$\forall$$C$ $(P(C))$

Where $v$ is a literal, $C$ is a clause (i.e. the $OR$ of 3 literals) and $P(C)$ means that $C$ is true.

However I'm not satisfied with this definition, I don't think it captures the complexity of the 3SAT language, especially the dependence of the variables on one another. Can you tell me a correct formula to describe this decision problem? Thank you.

Answer 1

The language consists of ternary relations $R_1, \dots, R_4$, which represent the clauses as follows:

• $(x,y,z)\in R_1$ iff there is a clause $(x\lor y\lor z)$;
• $(x,y,z)\in R_2$ iff there is a clause $(x\lor y\lor \neg z)$;
• $(x,y,z)\in R_3$ iff there is a clause $(x\lor \neg y\lor \neg z)$;
• $(x,y,z)\in R_4$ iff there is a clause $(\neg x\lor \neg y\lor \neg z)$.

($\lor$ commutes so you don't need to consider other patterns of negation.)

The formula then says "There exists a set $T$ of variables such that, if the variables in $T$ are set to true and the ones not in $T$ are set to false, the formula is satisfied." That is,

$$\begin{align*} \exists T\,\forall x\forall y\forall z\, \big[&\big(R_1(x,y,z)\rightarrow (T(x)\lor T(y)\lor T(z))\big)\\ &\quad \land \big(R_2(x,y,z)\rightarrow (T(x)\lor T(y)\lor \neg T(z))\big)\\ &\quad \land \dots\big]\,. \end{align*}$$