The number of clauses in an unsatisfiable CNF

Question

I am interested in generalisations of the following observation:

An unsatisfiable $k$-CNF has at least $2^k$ clauses.

A special case of the observation is when $k=n$, where $n$ is the number of variables. In this case, the clause-variable incidence graph is a complete bipartite graph.

I am particularly interested in the question:

Is there a lower bound on the number of clauses in a CNF $\phi$, in terms of the number of variables of $\phi$, when the clause-variable incidence graph of $\phi$ is $2K_2$-free (i.e. is a bipartite chain graph)?

But I am also interested in any generalisation of that question, or references to papers on questions about CNFs with this extremal flavour.

EDIT: Thanks to Christian Komusiewicz for highlighting that my question was ambiguous. The lower bound I'm after should be a function of the number of variables.

Answer 1

For arbitrarily large number $n$ of variables, the following CNF formula $\phi$ is not satisfiable, has only three clauses, and a $2K_2$-free clause-variable incidence graph:

$C_1=(x_1)$, $C_2=(\neg x_1)$, $C_3=(x_1,\ldots,x_n)$.

Thus, to get more interesting lower bounds one needs to make assumption about the minimum clause size or about the size of classes of clauses that contain the same variables (i.e. that have identical neighborhoods in the clause-variable incidence graph).

Observe that when the minimum clause size is $k$, then the example above can be adapted to give formulas with $2^k+1$ clauses and arbitrarily large number of variables $n$ that are not satisfiable. Moreover, when the number of clauses is $m<2^k+1$, then the formula is satisfiable even for arbitrarily large $n>k$: Let $C_m$ be the clause that has is incident with the largest set of variables. Since $n>k$, there is a variable $y$ that is not contained in the variable set of $C_1$, the clause with the smallest set of incident variables. Now, as for $k$-CNF formulas, the clauses $C_1,\ldots,C_{m-1}$ can be satisfied via an assignment of the first $k$ variables (which they all contain) and $C_m$ can be satisfied via the appropriate assignment of $y$.