Research on Random Generation of Test Instances with Controlled Attributes.

点击翻译按钮获取中文摘要

1. To test the performance of local-search-based SAT algorithms, we used new types of generators which can generate random SAT instances with controlled attributes such as the number of solutions. Then we presented the following result at the IJCAI95 conference : Among several different strategies of local search, the weighting strategy is overwhelmingly faster than the others. Furthermore, by examining the weighted local search from several angles, we introduced a more sophisticated weighting strategy, i.e., adding new clauses, and presented at the AAAI96 conference that the new strategy is faster than the simple weighting strategy.2. The process of SAT-instance generation is similar to the reverse process of Resolution, which is a proof system for the family of unsatisfiable CNF predicates. By making use of this similarity, we proved that Read-Once Resolution (ROR) is NP-complete, where ROR is one of the weakest system among Resolution-type systems. Since our test-instance generators are considerably more complicated than the reverse of Resolution, we could claim the security of our generators. This result was presented at the conference of IEEE Structure in Complexity in 1995. Another contribution of the result is as follows : It is well known that Resolution is very efficient practically, however, the computational complexity remained open. Of theoretical interest is the somewhat surprisingly result : In spite of its simplisity and a weak power, ROR is still intractable.3. Almost all the results of the research on instance generation with controlled attributes were published in "Cliques, Coloring, and Satisfiability (DIMACS Series 26)". In this DIMACS volume, a lot of researchers reported the performance of many types of SAT algorithms by using SAT instances generated by our generators. Thus, we contributed for selecting efficient strategies from the SAT algorithms.