We have seen various languages proven to be outside of REG and CFL by corresponding pumping lemmas.

Has something similar been done for SAT?

  • 1
    $\begingroup$ In general terminology, there is only finitely many symbols in a REG or CFL. However, there are infinitely many symbols in SAT since the number of different variables can be as arbitrarily large. To make this question clear, can you specify a formal definition of REG and CFL that allows infinitely many symbols and infinitely many production rules? $\endgroup$ – John L. Nov 4 '18 at 19:00
  • 2
    $\begingroup$ @Apass.Jack , it might make more sense to define SAT using only a finite list of symbols. The easiest way would have a symbol v for a variable, and then concatenate, so vv would be one's second variable, vvv would be the third one and so on. At least with this formulation, I'suspect that proving that the resulting language is non-context free as the original poster asked should be doable. $\endgroup$ – JoshuaZ Nov 4 '18 at 19:39
  • $\begingroup$ @JoshuaZ, nice suggestion. Then it seems easy to see various SAT are regular languages. $\endgroup$ – John L. Nov 4 '18 at 19:50
  • $\begingroup$ @Apass.Jack What do you mean? Are you implying that 3SAT is regular? I don't find that easy to prove (I somehow expect it not to be regular). $\endgroup$ – chi Nov 5 '18 at 10:39
  • $\begingroup$ @JoshuaZ, how much does this replacement of different terminals by v, vv, vvv, etc preserve (the intrinsic and extrinsic) properties of a grammar? $\endgroup$ – John L. Nov 5 '18 at 15:07

One possible encoding of SAT is as a string over the alphabet $\{x,\land,\lor,\lnot,0,1\}$ which encodes a satisfiable CNF. This language is not regular since intersecting it with an appropriate regular expression, we obtain the language semantically representing $x_i \land \lnot x_i$, which is essentially the language of squares $ww$, classically known to be non-regular. The same argument also shows that UNSAT is not context-free. It is highly likely that similar arguments (perhaps using fancier template formulas) would show that SAT is also not context-free.

  • $\begingroup$ Can you give a clue what that appropriate regular expression looks like? $\endgroup$ – John L. Nov 7 '18 at 7:13
  • $\begingroup$ You can take $x(0+1)^+ \land \lnot x(0+1)^+$. $\endgroup$ – Yuval Filmus Nov 7 '18 at 7:14
  • $\begingroup$ Do you mean $x0 \wedge \lnot x1$ is of form $w\wedge \lnot w$? $\endgroup$ – John L. Nov 7 '18 at 7:21
  • $\begingroup$ No, since $0 \neq 1$. $\endgroup$ – Yuval Filmus Nov 7 '18 at 7:23
  • $\begingroup$ is 1 in $(0+1)^+$? Is that $(0\mid 1) (0\mid 1)^*$? $\endgroup$ – John L. Nov 7 '18 at 7:27

Your Answer

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