Is there a place I can find a list of known unsatisfiable cores for X variables [no more then 10] in CNF format?
Or is there an 'easy' way to find out, say I have 7 variables how many clauses [of the 7 variables] do I need for an unsatisfiable cores.
[I calculated 2-5 by hand, I am just trying to figure out 6+].
Thanks
Staque
On
The question you are asking has been dealt with in the literature, and there is even a system that does it. Here is an example: https://sun.iwu.edu/~mliffito/publications/jar_liffiton_CAMUS.pdf
The potential number of pairwise different clauses with $n$ variables and the number of sorted sets of clauses:
Your proposed list of unsatisfiable cores is intractable long for any meaningful number of variables.
A brute-force way to find such unsatisfiable cores would be to enumerate the sets with a given number of variables and clauses. To be an unsatisfiable core, the set of clauses has to be unsatisfiable as a whole. This can be checked by using a SAT solver or enumerating up to $2^n$ variable assignments.
Unsatisfiable cores are usually created or extracted with respect to a given Boolean formula rather than compiling a complete list of all conceivable cores.