# Short $\exists$SO sentences over strings that define an NP-complete problem

[Q1] I'm wondering if there are some "official" SHORT existential second order sentences with ONE binary relation, over strings (over a small alphabet) that define an NP-complete set.

(Something similar to 3-colorability that over graphs can be expressed with a short sentence)

All examples that come to my mind are rather LONG/complex even for simple NP-complete problems; for example we can define the instances of the STRING TO STRING CORRECTION PROBLEM $$L$$ using alphabet $$\{ e, 0, 1, \# \}$$

$$L \subseteq \{ e^k (0|1)^n \# (0|1)^m \}$$

$$w \in L$$ if the first string $$S_1$$ (binary sequence before $$\#$$) matches the second string $$S_2$$ (binary sequence after $$\#$$) up to at most $$k$$ edit/delete operations.

For example: $$ee001100\#000000$$ (with two edits we can transfor $$001100 \to 000000$$)

In order to define it we can use a SO sentence that begins with $$\exists M$$ but we need to use a lot of first order constraints and "details":

• $$\#$$ occurs once
• $$M$$ is a function (represents the copy or delete/insert operations)
• $$x$$ belongs to $$S_1$$: $$S_1(x) \equiv \exists y > x \;.\; U_{\#}(y)$$
• $$x$$ belongs to $$S_2$$: $$S_2(x) \equiv \exists y < x \;.\; U_{\#}(y)$$
• $$Diff(x,y)$$ iff chars at $$x,y$$ are different
• $$M$$ maps chars from $$S_1$$ to chars of $$S_2$$ or from a $$e$$ to a char of $$S_1,S_2$$
• order is preserved: if $$x_1, x_2 \in S_1 \land y_1,y_2 \in S_2 \land M(x_1,y_1) \land M(x_2, y_2)$$ then $$x_1 < x_2 \land y_1 < y_2$$
• all chars are copied/edited/deleted: $$\forall x \in S_i \exists y . M(x,y) \lor M(y,x)$$
• edited chars handling: if $$S_1(x) \land S_2(y) \land M(x,y) \land Diff(x,y)$$ then $$\exists z . U_{e}(z) \land ( M(z,x) \lor M(z,y)$$
• deleted chars handling: if $$S_i(x) \land \forall y . \neg ( M(x,y) \lor M(y,x) )$$ then $$\exists z . U_{e}(z) \land M(z,x)$$

[Q2.1] Can we get an even shorter sentences that define an NP-complete language if we allow ONE (existential) ternary relation or [Q2.2] more (existential) binary relations?.