Redundancy in Random SAT Formulas

The random k-SAT model is extensively used to compare satisfiability algorithms or to find the best settings for the parameters of some algorithm. Conclusions are derived from the performances measured on a large number of random instances. The size of these instances is, in general, small to get these experiments done in reasonable time. This assumes that the small size formulas have the same properties as the larger ones. We show that small size formulas have at least a characteristic that makes them relatively easier than the larger ones (beyond the increase in the size of the formulas). This characteristic is the redundancy. We show, experimentally, that the irredundant formulas are harder for both complete and incomplete methods. Besides, the randomly generated formulas tend to be naturally irredundant as their size becomes larger. Thus, irredundant small formulas are more suitable for testing algorithms because they better reflect the hardness of the larger ones.

• Type: Conference
• Year: 2000
• Where: AAAI
• Authors: Yacine Boufkhad, Olivier Roussel
• Keywords: AAAI 2000, Intelligent Agents, Larger Ones, Random K-SAT Model, Small Size Formulas