Research on Random Generation of Test Instances with Controlled Attributes.

1.为了测试基于局部搜索的SAT算法的性能，我们使用了新类型的生成器，它可以生成具有受控属性（如解的数量）的随机SAT实例。然后我们在IJCAI 95会议上提出了以下结果：在几种不同的局部搜索策略中，加权策略的速度压倒性地快于其他策略。此外，通过从多个角度检查加权局部搜索，我们引入了更复杂的加权策略，即，增加了新的条款，并在AAAI 96会议上提出了新的策略比简单的加权策略更快. SAT实例的生成过程类似于Resolution的逆过程，Resolution是一个针对不可满足CNF谓词族的证明系统。利用这种相似性，我们证明了只读一次归结（ROR）是NP-完全的，其中ROR是归结型系统中最弱的系统之一。由于我们的测试实例生成器比Resolution的反向生成器复杂得多，因此我们可以声明生成器的安全性。这一结果在1995年IEEE Structure in Complexity会议上发表。该结果的另一个贡献如下：众所周知，Resolution实际上是非常有效的，但是，计算复杂度仍然是开放的。理论上的兴趣是有点令人惊讶的结果：尽管它的简单性和弱的权力，ROR仍然是棘手的。几乎所有关于控制属性的实例生成的研究成果都发表在“团，着色和可满足性（DIMACS系列26）”中。在这本DIMACS卷中，许多研究人员通过使用我们的生成器生成的SAT实例报告了许多类型的SAT算法的性能。因此，我们有助于选择有效的战略，从SAT算法。

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.