A QSAT Benchmark Based on Vertex-Folkman Problems (Student Abstract)

Authors

  • David E. Narváez Rochester Institute of Technology

DOI:

https://doi.org/10.1609/aaai.v34i10.7213

Abstract

The purpose of this paper is to draw attention to a particular family of quantified Boolean formulas (QBFs) stemming from encodings of some vertex Folkman problems in extremal graph theory. We argue that this family of formulas is interesting for QSAT research because it is both conceptually simple and parametrized in a way that allows for a fine-grained diversity in the level of difficulty of its instances. Additionally, when coupled with symmetry breaking, the formulas in this family exhibit backbones (unique satisfying assignments) at the top-level existential variables. This benchmark is thus suitable for addressing questions regarding the connection between the existence of backbones and the hardness of QBFs.

Downloads

Published

2020-04-03

How to Cite

Narváez, D. E. (2020). A QSAT Benchmark Based on Vertex-Folkman Problems (Student Abstract). Proceedings of the AAAI Conference on Artificial Intelligence, 34(10), 13881-13882. https://doi.org/10.1609/aaai.v34i10.7213

Issue

Section

Student Abstract Track