Hidden structure in unsatisfiable random 3-SAT: an empirical study

Recent advances in prepositional satisfiability (SAT) include studying the hidden structure of unsatisfiable formulas, i.e. explaining why a given formula is unsatisfiable. Although theoretical work on the topic has been developed in the past, only recently two empirical successful approaches have been proposed: extracting unsatisfiable cores and identifying strong backdoors. An unsatisfiable core is a subset of clauses that defines a subformula that is also unsatisfiable, whereas a strong backdoor defines a subset of variables which assigned with all values allow concluding that the formula is unsatisfiable. The contribution of This work is two-fold. First, we study the relation between the search complexity of unsatisfiable random 3-SAT formulas and the sizes of unsatisfiable cores and strong backdoors. For this purpose, we use an existing algorithm which uses an approximated approach for calculating these values. Second, we introduce a new algorithm that optimally reduces the size of unsatisfiable cores and strong backdoors, thus giving more accurate results. Experimental results indicate that the search complexity of unsatisfiable random 3-SAT formulas is related with the size of unsatisfiable cores and strong backdoors.