# Descriptive complexity of 3SAT

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

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

$$\existsv\forallC$$ $$(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.

• It depends on the way the 3SAT language is represented and the related $\sigma$-structure you choose. On ordered structures (i.e. strings) it's not so simple. – Vor Jul 19 '19 at 10:12

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*}