Redundancy in Random SAT Formulas

Knowledge Representation and Reasoning

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 17

Boolean Satisfiability

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 than 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 become larger. Thus, irredundant small formulas are more suitable for testing algorithms because they better reflect the hardness of the larger ones.