You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

GhostQ

Issue title: SAT 2018 Competitions and Evaluations

Subtitle: System Description

Guest editors: Martina Seidl and Luca Pulina

Article type: Research Article

Authors: Klieber, William

Affiliations: Carnegie Mellon University, Pittsburgh, Pennsylvania, USA. E-mail: [email protected]

Keywords: QBF, DPLL, non-clausal, Plaisted-Greenbaum encoding

DOI: 10.3233/SAT190117

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 11, no. 1, pp. 65-72, 2019

Received 1 November 2018
|
Revision received 1 March 2019
|
Published: 1 September 2019
Get PDF open access

Abstract

GhostQ is a DPLL-based non-CNF QBF solver. This paper describes a noteworthy feature of GhostQ that has not yet been described in the peer-reviewed literature: support for Plaisted-Greenbaum encoding. For CNF inputs, GhostQ attempts to perform reverse engineering on the CNF formula to create an equivalent circuit representation. Support for reversing the Plaisted-Greenbaum transformation was added to the existing capability for reversing the Tseitin transformation.

Show more