Generating “Random” 3-SAT Instances with Specific Solution Space Structure

Pushkin R. Pari, Jane Lin, Lin Yuan, and Gang Qu

Generating good benchmarks is important for the evaluation and improvement of any algorithm for NP-hard problems such as the Boolean satisfiability (SAT) problem. Carefully designed benchmarks are also helpful in the study of the nature of NP-completeness . Probably the most well-known and successful story is the discovery of the phase transition phenomenon (Cheeseman, Kanefsky, and Taylor 1991). More recently, (Achlioptas et al. 2000) pointed out the importance of generating satisfiable problem instances. In this abstract, we consider how to create 3-SAT formulas that look like random but with specific solution structures. In particular, we show that random 3-SAT formulas do not have their solutions distributed randomly in the solution space and we further develop generators to build random 3-SAT formulas with randomly distributed solutions or fixed number of solutions.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.