Abstract
We present the results from experiments with a new family of random formulas for the satisfiability problem. Our proposal is a generalisation of the random k-SAT model that introduces non-clausal formulas and exhibits interesting features such as experimentally observed sharp phase transition and the easy-hard-easy pattern. The experimental results provide some insights on how the use of different clausal translations can affect the performance of satisfiability solving algorithms. We also expect our model to provide diverse and challenging benchmarks for developers of SAT procedures for non-clausal formulas. Copyright © 2005, American Association for Artificial Intelligence (www.aaai.org). All rights reserved.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the National Conference on Artificial Intelligence|Proc Natl Conf Artif Intell |
| Publisher | AAAI Press |
| Pages | 436-442 |
| Number of pages | 6 |
| Volume | 1 |
| Publication status | Published - 2005 |
| Event | 20th National Conference on Artificial Intelligence and the 17th Innovative Applications of Artificial Intelligence Conference, AAAI-05/IAAI-05 - Pittsburgh, PA Duration: 1 Jul 2005 → … http://dblp.uni-trier.de/db/conf/aaai/aaai2005.html#NavarroV05http://dblp.uni-trier.de/rec/bibtex/conf/aaai/NavarroV05.xmlhttp://dblp.uni-trier.de/rec/bibtex/conf/aaai/NavarroV05 |
Conference
| Conference | 20th National Conference on Artificial Intelligence and the 17th Innovative Applications of Artificial Intelligence Conference, AAAI-05/IAAI-05 |
|---|---|
| City | Pittsburgh, PA |
| Period | 1/07/05 → … |
| Internet address |