GhostQ: A QBF Solver

GhostQ is a non-clausal QBF solver. It has been extended to support (1) a limited amount of the CEGAR technique used in RAReQS (Recursive Abstraction Refinement QBF Solver) and (2) free variables. System description (PDF)

Download GhostQ source code:

Current stable:

GhostQ is distributed under the terms of the GNU GPL v3.

Unfortunately, the source code is rather messy at the moment. The above versions of GhostQ no longer support non-prenex input (except the old 2010 version).

The GhostQ executable can be built by running make. There is a script battery02.sh that runs a few test inputs and compares to the expected output.

The GhostQ executable reads its input in a special GhostQ input format. The script qcir-conv.py attempts to reverse-engineer QDIMACS to prenex QCIR or to the GhostQ format. The script qcir-to-gq.sh converts a QCIR file to the GhostQ format. The Gallery versions also have scripts solver-*.sh that run the solver.

Converting a large, deeply-nested QCIR formula may fail if there is insufficient stack space. This can be fixed by increasing the stack limit before running the converter (e.g., by running "ulimit -S -s unlimited" in Bash).

For formulas with free variables, the output of GhostQ is in a formula format that allows subformulas to be named and then referred to again by name. For example, in the below formula, the subformula "or(x1, x2)" is named "$1" and then referred to again by that name:

or(and(y1, $1:or(x1, x2)), and(y2, $1))

A parser for this format is in fmla.cpp. Recent versions of GhostQ also support an option "-write-qcir" to write output in the QCIR format. (An older draft of this format, limited to prenex only, is also available: qcir.pdf, qcir.tex.)

Related

Tool to convert from prenex QCIR to QDIMACS

Papers

See Will Klieber's main page. GhostQ is also described in detail in Will Klieber's Ph.D. thesis.