PV1 ⊧ HQSpresimplifies quantified Boolean formulas and dependency quantified Boolean formulas

HQSpre, a state-of-the-art tool for simplifying quantified Boolean formulas (QBFs) and the first available preprocessor for dependency quantified Boolean formulas (DQBFs)

Application domain/field

• Simplifying
• Quantified Boolean formulas (QBFs)
• Dependency quantified Boolean formulas (DQBFs)
• Formula simplification
• Clause elimination
• Clause strengthening
• Variable elimination

Type of tool

Metatool?

Expected input

(Dependency) quantified Boolean formula ((D)QBF)

Format:

QDIMACS or DQDIMACS format

Expected output

Simplified formula

Internals

One of the motivations behind this tool is that it can be used to simplify formulas before the solver is called. This may reduce the overall computation time and may make some instances feasible to solve which cannot be solved without preprocessing. Some of the techniques used to simplify the formula depend on a SAT solver, for this they use the Antom SAT solver.