0
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Vor Jul 19 '19 at 10:12
1
$\begingroup$

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

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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