Generation of Hard Non-Clausal Random Satisfiability Problems
Abstract
We present the results from experiments with a new family of random formulas for the satisfiability problem. Our pro-posal is a generalisation of the random k-SAT model that introduces non-clausal formulas and exhibits interesting fea-tures such as experimentally observed sharp phase transition and the easy-hard-easy pattern. The experimental results pro-vide some insights on how the use of different clausal trans-lations can affect the performance of satisfiability solving al-gorithms. We also expect our model to provide diverse and challenging benchmarks for developers of SAT procedures for non-clausal formulas.
Cite
Text
Pérez and Voronkov. "Generation of Hard Non-Clausal Random Satisfiability Problems." AAAI Conference on Artificial Intelligence, 2005.Markdown
[Pérez and Voronkov. "Generation of Hard Non-Clausal Random Satisfiability Problems." AAAI Conference on Artificial Intelligence, 2005.](https://mlanthology.org/aaai/2005/perez2005aaai-generation/)BibTeX
@inproceedings{perez2005aaai-generation,
title = {{Generation of Hard Non-Clausal Random Satisfiability Problems}},
author = {Pérez, Juan Antonio Navarro and Voronkov, Andrei},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2005},
pages = {436-442},
url = {https://mlanthology.org/aaai/2005/perez2005aaai-generation/}
}