The study of models for generating random instances of boolean satisfiability problems has received substantial attention from the artificial intelligence community in the last twenty years. The availability of generators for such models allowed to improve significantly the robustness and the performance of solvers by providing a controlled way of creating new benchmarks. Recently, we proposed two new models of random QSAT formulas in non-clausal form that properly generalize the well-known model of random k-CNF formulas and the Chen-Interian model of random 2QBFs. They also imply the first models for ran- dom disjunctive logic programs. In this website it is available an instance generation tool that implements the two new random generation models, and supports a variety of standard output formats including (Q)DIMACS, QCIR, and ASPCore 2.0. |
Citation info:
Giovanni Amendola, Francesco Ricca, Miroslaw Truszczynski
Generating Hard Random Boolean Formulas and Disjunctive Logic Programs
Proceedings of the International Joint Conference on Artificial Intelligence - IJCAI 2017.
Usage Instructions:
The generator is developed in Java, it requires a JVM 1.7 or newer.
To run the generator type:
$> java -jar RandomGenerator-1.8 [options]
The list of available options can be obtained by running:
$> java -jar RandomGenerator-1.8 -h
Download:
The JAR of the generator can be downloaded by clicking on the following link: randomgenerator-1-8-jar
(The archive is compressed with zip to load it in altervista, unzip it first!)
To easily select the parameters for generating instances you can have a lool at this guide.