depqbf ☆

« Back to VersTracker

Description:
Solver for quantified boolean formulae (QBF)

Type: Formula | Latest Version: 6.03@0 | Tracked Since: Dec 17, 2025

Links: Homepage | formulae.brew.sh

Category: Developer tools

Tags: qbf solver formal-verification logic sat academic

Install: brew install depqbf

About:
DepQBF is a high-performance solver for quantified boolean formulae (QBF), also known as fully true quantified boolean formulae (TQBF). It implements a highly efficient Q-resolution calculus engine to solve complex satisfiability problems involving both existential and universal quantifiers. The tool is valuable for formal verification, automated reasoning, and computational logic research where standard SAT solvers are insufficient.

Key Features:

High-performance Q-resolution calculus engine
Supports standard QDIMACS input format
Produces certified proofs for unsatisfiable instances
Command-line interface for integration into toolchains

Use Cases:

Formal verification of hardware and software systems
Solving problems in computational logic and knowledge representation
Academic research in automated reasoning and theorem proving

Alternatives:

CAQE – Another top-performing QBF solver using abstraction-based approach
GhostQ – Solver utilizing hoare logic and interpolation techniques
quabs – QBF solver based on conflict-driven clause learning (CDCL)

License: GPL-3.0-or-later

Bottles available for: arm64_tahoe, arm64_sequoia, arm64_sonoma, arm64_ventura, arm64_monterey, arm64_big_sur, sonoma, ventura, monterey, big_sur, catalina, arm64_linux, x86_64_linux

Version History

Detected	Version	Rev	Change	Commit
Sep 15, 2025 8:21am		0	VERSION_BUMP	b43abe55