Is such variant of SAT always satisfiable?

Let we have a SAT instance where every clause has length $\ge3$ (when length $2$ is allowed, it can be unsatisfiable) and each pair of literals appear only once.

Non-example: $(x\lor y\lor z)\land(x\lor y\lor t)$. Here a pair $\{x,y\}$ appears twice.

Example: $(x\lor y\lor z)\land(x\lor\overline y\lor\overline z)$. $\{x,y\}$ and $\{x,\overline y\}$ count as different pairs.

Another example is a clause $(x\oplus y\oplus z)$ reduced to CNF.

So, do there exist an unsatisfiable formula under these restrictions?

• Have you seen: MU(k)? – Evil Sep 10 '17 at 23:44
• @Evil, how that does help? I hadn't found a proof/counterexample there. – rus9384 Sep 11 '17 at 0:08
• @Evil, it's interesting that if number of clauses is bounded by $n + \log n$, where $n$ is number of variables, then formula is in $\mathsf{coNP}$. – rus9384 Sep 11 '17 at 0:31
• Well, I thought that it might be interesting to you, it defines minimal unsatisfiable formula with different constraints so it might be connected, and yes it doesn't answer your question, just the article I thought about after reading your question so only comment. – Evil Sep 11 '17 at 0:47
• Try coding something up to generate random formulas that satisfy this constraint? My guess would be that if $n$, the number of variables, is large enough, and if you keep adding randomly chosen clauses (that don't violate the constraint) until you can't add any more (without violating the constraint), then with high probability such a randomly chosen formula will be unsatisfiable. Why don't you code it up, test it, and see what happens? – D.W. Sep 11 '17 at 5:38