Minimum Unsatisfiable 3-CNF Formulae I am currently interested in obtaining (or constructing) and studying 3-CNF formulae which are unsatisfiable, and are of minimum size. That is, they must consist of as few clauses (m = 8 preferably) as possible, and as few distinct variables (n = 4 or more) as possible, such that removing at least one clause will render the formula satisfiable.

More formally, any qualifying 3-CNF formula F must satisfy the following conditions:


F is unsatisfiable
F has a minimum amount (4+) of distinct variables (or their negation)
F has a minimum amount of clauses (8+)
every proper subset of F is satisfiable (allowing removal of any arbitrary clause or clauses).
F has no 2 clauses that are reducible to a 2-CNF clause
e.g. (i, j, k) &amp; (i, j, ~k) is NOT allowed ( they reduce to (i,j) )


For example, with n=4, there exists many minimal 8-clause 3-CNF formulae that are unsatisfiable. For one, by looking at the 4-hypercube and trying to cover it with edges (2-faces), one can construct the following unsatisfiable formula:

1. (~A,  B,  D)
2. (~B,  C,  D)
3. ( A, ~C   D)
4. ( A, ~B, ~D)
5. ( B, ~C, ~D)
6. (~A,  C, ~D)
7. ( A,  B,  C)
8. (~A, ~B, ~C)


This qualifies as a minimum unsatisfiable 3-CNF formula because:


It is unsatisfiable:


Clauses 1-3 are equivalent to:  D or A=B=C
Clauses 4-6 are equivalent to: ~D or A=B=C
They imply A=B=C, but by clauses 7 and 8, this is a contradiction.

There are only 4 distinct variables.
There are only 8 clauses.
Removing any clause renders it satisfiable.
No 2 clauses are 'reducible' to a 2-CNF clause.


So I guess my overall questions here are, in order of importance to me:


What are some other small minimum formulae which meet the above conditions?
(i.e. for say, 4,5,6 variables and 8,9,10 clauses)
Is there some sort of database or "atlas" of such minimum formulae?
What nonrandom algorithms exist for constructing them outright, if any?
What are some insights into these formulae's characteristics? Can they be counted or estimated, given n (# variables) and m (# clauses)?


Thank-you in advance for your replies.
I welcome any answer or comment.
Take the formula in your example, remove the clause $\lnot A \lor \lnot B \lor \lnot C$ and add the following $2$ clauses:  

$\lnot A \lor \lnot B \lor \lnot E$
$\lnot B \lor \lnot C \lor E$ 

You will get a minimal unsatisfiable formula with $n=5$, $m=9$ obeying condition 5.  

In general, you may randomly pick a clause $l_1 \lor l_2 \lor l_3$ and split it in $2$ clauses:  

$l_1 \lor l_2 \lor v$
$l_2 \lor l_3 \lor \lnot v$  

where $v$ is a new variable. Each time you do so, both $n$ and $m$ are incremented by $1$. Repeating this process allows you to "stretch" the initial unsatisfiable core, and to obtain minimal unsatisfiable formulas (obeying condition 5) whose $r=\frac{m}{n}$ tends to $1$ as $n$ grows (which is pretty rare, as formulas with $r=1$ are satisfiable with high probability).