Studies on Averagingly Fast Combinatorial Algorithms and Experimental Evaluation of Their Performances

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

1. Our algorithms for generating test instances to evaluate the performances of SAT algorithms have been implemented. The generator consists of two independent generators, one for yes-instances and the other for no-instances. Also, the generator takes, as its input, several parameters such as the literal distribution, literal/vaviable ratio and the maximum number of solutions. Instances generated by our generator were included in the official benchmark of DIMACS and are being widely used.2. As for the local search method for SAT, we introduced a new approach based on weighting clauses, which made a speed-up of 100 times or more when the number of vaviables is 40.3. The same approach has been applied to the evaluation of logic optimizers. The idea of generating test circuits is to transform an initial (simple) circuit into a (complex) test circuit by applying repeatedly basic transformation rules that do not change the realized logic function. The first version was implemented and was used to test the common optimizer, SIS.Our paper was accepted for presentation at 31st ACM/IEEE DAC.