On the Imbalance of Distributions of Solutions of CNF-Formulas and its Impact on Satisfiability Solvers

Speckenmeyer, Ewald and Böhm, Max and Heusch, Peter (1997) On the Imbalance of Distributions of Solutions of CNF-Formulas and its Impact on Satisfiability Solvers.
Published In: Satisfiability problem : theory and applications ; DIMACS workshop March 11 - 13, 1996, DIMACS series in discrete mathematics and theoretical computer science. 35 American Math. Soc. 1997, pp. 669-676.

Abstract

Let F be Boolean formulas in conjunctive normal form with n variables, r clauses, every clause has length s. We show that if F is split into two subformulas F_{v} and F_{overline{v}} by setting v true and false in F, then the expected number of solutions of one of the two subformulas F_{v} and F_{overline{v}} is significantly higher than that in the other subformula, when dealing with classes of formulas where the great majority of formulas is satisfiable. We discuss practical consequences of this result.


Actions:
Download: [img] Postscript - Preprinted Version
Download (182kB) | Preview
Editorial actions: View Item View Item (Login required)
Deposit Information:
ZAIK Number: zpr96-235
Depositing User: Archive Admin
Date Deposited: 02 Apr 2001 00:00
Last Modified: 19 Jan 2012 09:37
URI: http://e-archive.informatik.uni-koeln.de/id/eprint/235