How does one show that a certain property cannot be expressed in 2-CNF (2-SAT)?  Are there any games, such as pebble games?  It seems that the classical black pebble game and the black-white pebble game are unsuitable for this (they are PSPACE complete, according to Hertel and Pitassi, SIAM J of Computing, 2010).Or any techniques other than games?Edit:  I was thinking of properties that involve counting (or cardinality) of an unknown predicate (SO predicate, as finite model theorists would say).  For example, as in Clique or unweighted Matching.(a) Clique: Is there a clique $C$ in the given graph $G$ such that $|C| \ge$ some given number $K$? $~$ (b) Matching: Is there a matching $M$ in $G$ such that $|M| \ge K$?Can 2-SAT count?  Does it have a counting mechanism?  Seems doubtful.
Properties expressible in 2-CNF or 2-SAT
sat;lower bounds;combinatorial game theory
A family of bitvectors is the class of solutions to a 2-SAT problem if and only if it has the median property: if you apply the bitwise majority function to any three solutions you get another solution. See e.g. https://en.wikipedia.org/wiki/Median_graph#2-satisfiability and its references. So if you can find three solutions for which this is not true, then you know it cannot be expressed in 2-CNF.