zbMATH — the first resource for mathematics

Random generation of test instances with controlled attributes. (English) Zbl 0864.90089
Johnson, David S. (ed.) et al., Cliques, coloring, and satisfiability. Second DIMACS implementation challenge. Proceedings of a workshop held at DIMACS, October 11–13, 1993. Providence, RI: American Mathematical Society. DIMACS, Ser. Discrete Math. Theor. Comput. Sci. 26, 377-393 (1996).
Summary: To evaluate the performance of SAT algorithms empirically, we have already proposed a new type of random test-instance generator with known answers and proved securities. In this paper, we mainly discuss its controllability of several attributes such as the literal distribution, the clause-size distribution and the number of satisfying truth assignments. The generation algorithm has been implemented into four different generators, which have been used to test a Davis-Putnam algorithm and a local search algorithm to examine how the former works for unsatisfiable predicates of low clause/variable ratio and how the latter’s efficiency depends on the number of solutions.
For the entire collection see [Zbl 0851.00080].

90C09 Boolean programming
68W10 Parallel algorithms in computer science
68R99 Discrete mathematics in relation to computer science