Generating Hard Random Boolean Formulas and Disjunctive Logic Programs

Generating Hard Random Boolean Formulas and Disjunctive Logic Programs

Giovanni Amendola, Francesco Ricca, Miroslaw Truszczynski

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
Main track. Pages 532-538. https://doi.org/10.24963/ijcai.2017/75

We propose a model of random quantified boolean formulas and their natural random disjunctive logic program counterparts. The model extends the standard models for random SAT and 2QBF. We provide theoretical bounds for the phase transition region in the new model, and show experimentally the presence of the easy-hard-easy pattern. Importantly, we show that the model is well suited for assessing solvers tuned to real-world instances. Moreover, to the best of our knowledge, our model and results on random disjunctive logic programs are the first of their kind.
Keywords:
Constraints and Satisfiability: Satisfiability
Knowledge Representation, Reasoning, and Logic: Logics for Knowledge Representation