Non-CNF QBF Solving with QCIR

C. Jordan; William Klieber; Martina Seidl

Non-CNF QBF Solving with QCIR

C. Jordan, William Klieber, Martina Seidl

Institute of Formal Models and Verification

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

While it is empirically confirmed folklore that conjunctive normal form (CNF) is not the ideal input format for QBF solvers, most tool developers and therefore also the users focus on formulas in this restricted structure. One important factor for establishing non-CNF solving is the input format. To overcome drawbacks of available formats, the QCIR format has recently been presented. The QCIR format is a circuit-based input format for quantified Boolean formulas which supports structure sharing. In contrast to previous formats, the representation is very compact, yet still easy to parse and to read for the human user. In this paper, we analyze the QCIR format in detail and provide tools and benchmarks which, we hope, will make its usage attractive and motivate tool developers to support this format as well as users to formulate their encodings in this format.

Original language	English
Title of host publication	Beyond NP, Papers from the 2016 AAAI Workshop, Phoenix, Arizona, USA, February 12, 2016
Editors	Adnan Darwiche
Publisher	AAAI Press
Number of pages	7
Volume	WS-16-05
Publication status	Published - 2016

Publication series

Name	AAAI Workshops

Fields of science

102 Computer Sciences
102001 Artificial intelligence
102011 Formal languages
102022 Software development
102031 Theoretical computer science
603109 Logic
202006 Computer hardware

JKU Focus areas

Computation in Informatics and Mathematics

Cite this

@inproceedings{0efa808033c94ac98e1a90cce3b9cfe0,

title = "Non-CNF QBF Solving with QCIR",

abstract = "While it is empirically confirmed folklore that conjunctive normal form (CNF) is not the ideal input format for QBF solvers, most tool developers and therefore also the users focus on formulas in this restricted structure. One important factor for establishing non-CNF solving is the input format. To overcome drawbacks of available formats, the QCIR format has recently been presented. The QCIR format is a circuit-based input format for quantified Boolean formulas which supports structure sharing. In contrast to previous formats, the representation is very compact, yet still easy to parse and to read for the human user. In this paper, we analyze the QCIR format in detail and provide tools and benchmarks which, we hope, will make its usage attractive and motivate tool developers to support this format as well as users to formulate their encodings in this format.",

author = "C. Jordan and William Klieber and Martina Seidl",

year = "2016",

language = "English",

volume = "WS-16-05",

series = "AAAI Workshops",

publisher = "AAAI Press",

editor = "\{Adnan Darwiche\}",

booktitle = "Beyond NP, Papers from the 2016 AAAI Workshop, Phoenix, Arizona, USA, February 12, 2016",

}

TY - GEN

T1 - Non-CNF QBF Solving with QCIR

AU - Jordan, C.

AU - Klieber, William

AU - Seidl, Martina

PY - 2016

Y1 - 2016

N2 - While it is empirically confirmed folklore that conjunctive normal form (CNF) is not the ideal input format for QBF solvers, most tool developers and therefore also the users focus on formulas in this restricted structure. One important factor for establishing non-CNF solving is the input format. To overcome drawbacks of available formats, the QCIR format has recently been presented. The QCIR format is a circuit-based input format for quantified Boolean formulas which supports structure sharing. In contrast to previous formats, the representation is very compact, yet still easy to parse and to read for the human user. In this paper, we analyze the QCIR format in detail and provide tools and benchmarks which, we hope, will make its usage attractive and motivate tool developers to support this format as well as users to formulate their encodings in this format.

AB - While it is empirically confirmed folklore that conjunctive normal form (CNF) is not the ideal input format for QBF solvers, most tool developers and therefore also the users focus on formulas in this restricted structure. One important factor for establishing non-CNF solving is the input format. To overcome drawbacks of available formats, the QCIR format has recently been presented. The QCIR format is a circuit-based input format for quantified Boolean formulas which supports structure sharing. In contrast to previous formats, the representation is very compact, yet still easy to parse and to read for the human user. In this paper, we analyze the QCIR format in detail and provide tools and benchmarks which, we hope, will make its usage attractive and motivate tool developers to support this format as well as users to formulate their encodings in this format.

UR - http://www.aaai.org/ocs/index.php/WS/AAAIW16/paper/view/12601

M3 - Conference proceedings

VL - WS-16-05

T3 - AAAI Workshops

BT - Beyond NP, Papers from the 2016 AAAI Workshop, Phoenix, Arizona, USA, February 12, 2016

A2 - Adnan Darwiche, null

PB - AAAI Press

ER -

Non-CNF QBF Solving with QCIR

Abstract

Publication series

Fields of science

JKU Focus areas

Other files and links

Cite this