Performance Test of Local Search Algorithms Using New Types of Random CNF Formulas

Abstract

New types of test-instance generators have been developed for generating random CNF (Conjunctive Normal Form) formulas with controlled attributes. In this paper, we use these generators to test the performance of local-search-based SAT algorithms. For this purpose, the generator which produces formulas having exactly one satisfying truth assignment is especially desirable. It is shown that (i) among several different strategies of local search, the weighting strategy is overwhelmingly faster than the others and that (ii) local search works significantly better for instances of larger clause/variable ratio, which allows us to come up with a new strategy for making local search even faster.

Cite

Text

Cha and Iwama. "Performance Test of Local Search Algorithms Using New Types of Random CNF Formulas." International Joint Conference on Artificial Intelligence, 1995.

Markdown

[Cha and Iwama. "Performance Test of Local Search Algorithms Using New Types of Random CNF Formulas." International Joint Conference on Artificial Intelligence, 1995.](https://mlanthology.org/ijcai/1995/cha1995ijcai-performance/)

BibTeX

@inproceedings{cha1995ijcai-performance,
  title     = {{Performance Test of Local Search Algorithms Using New Types of Random CNF Formulas}},
  author    = {Cha, Byungki and Iwama, Kazuo},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {1995},
  pages     = {304-311},
  url       = {https://mlanthology.org/ijcai/1995/cha1995ijcai-performance/}
}