16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'04)
Hidden Structure in Unsatisfiable Random 3-SAT: An Empirical Study
Boca Raton, Florida
November 15-November 17
ISBN: 0-7695-2236-X
Recent advances in propositional satisfiability (SAT) include studying the hidden structure of unsatisfiable formulas, i.e., explaining why a given formula is unsatisfiable. Although theoretical work o n 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 sub-formula 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 paper 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.
Citation:
Inês Lynce, João Marques-Silva, "Hidden Structure in Unsatisfiable Random 3-SAT: An Empirical Study," ictai, pp.246-251, 16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'04), 2004