UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Generation of Hard Non-Clausal Random Satisfiability Problems

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 Green open access

[thumbnail of Navarro_aaai05.pdf]
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
Downloads since deposit
0Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item