Unsatisfiable random formulas are hard to certify

We prove that every property of 3CNF formulas that implies unsatisfiability and is expressible in Datalog has asymptotic probability zero when formulas are randomly generated by taking 6n non-trivial clauses of exactly three literals uniformly and independently. Our result is a consequence of designing a winning strategy for Duplicator in the existential k-pebble game on the structure that encodes the 3CNF formula and a fixed template structure encoding a satisfiable formula. The winning strategy makes use of certain extension axioms that we introduce and hold almost surely on a random 3CNF formula. An interesting feature of our result is that it brings the fields of propositional proof complexity and finite model theory together. To make this connection more explicit, we show that Duplicator wins the existential pebble game on the structure encoding the pigeonhole principle and the template structure above. Moreover, we also prove that there exists a 2k-Datalog program expressing that an input 3CNF formula has a resolution refutation of width k. As a consequence to our result and the known size-width relationship in resolution, we obtain new proofs of the exponential lower bounds for resolution refutations of random 3CNF formulas and the pigeonhole principle.