Pérez, JAN;
Voronkov, A;
(2005)
Generation of Hard Non-Clausal Random Satisfiability Problems.
In: Veloso, MM and Kambhampati, S, (eds.)
AAAI 2005.
(pp. 436 - 442).
AAAI Press / The MIT Press
![[thumbnail of Navarro_aaai05.pdf]](https://discovery.ucl.ac.uk/style/images/fileicons/application_pdf.png) Preview |
PDF
Navarro_aaai05.pdf Download (130kB) |
Abstract
We present the results from experiments with a new family of random formulas for the satisfiability problem. Our proposal is a generalization 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.
| Type: | Proceedings paper |
|---|---|
| Title: | Generation of Hard Non-Clausal Random Satisfiability Problems |
| ISBN: | 1-57735-236-X |
| Open access status: | An open access version is available from UCL Discovery |
| Publisher version: | http://www.informatik.uni-trier.de/~ley/db/conf/aa... |
| Language: | English |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/1361367 |
Archive Staff Only
 |
View Item |
