HordeQBF: a modular and massively parallel QBF solver

DOI10.1007/978-3-319-40970-2_33MaRDI QIDQ2818039zbMATH OpenOpenAlexFDO

Authors Tomáš Balyo, Florian Lonsing

Publication date 5 September 2016

Published in Theory and Applications of Satisfiability Testing – SAT 2016 (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1604.03793

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Abstract: The recently developed massively parallel satisfiability (SAT) solver HordeSAT was designed in a modular way to allow the integration of any sequential CDCL-based SAT solver in its core. We integrated the QCDCL-based quantified Boolean formula (QBF) solver DepQBF in HordeSAT to obtain a massively parallel QBF solver---HordeQBF. In this paper we describe the details of this integration and report on results of the experimental evaluation of HordeQBF's performance. HordeQBF achieves superlinear average and median speedup on the hard application instances of the 2014 QBF Gallery.

Recommendations

• HordeSat: a massively parallel portfolio SAT solver
• \(\mathsf{MPIDepQBF}\): towards parallel QBF solving without knowledge sharing
• DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
• Formal Methods in Computer-Aided Design
• Using SAT in QBF

Cites work

• \(\mathsf{MPIDepQBF}\): towards parallel QBF solving without knowledge sharing
• A high-performance, portable implementation of the MPI message passing interface standard
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Clause elimination for SAT and QSAT
• Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
• Enhancing search-based QBF solving by dynamic blocked clause elimination
• HordeSat: a massively parallel portfolio SAT solver
• scientific article; zbMATH DE number 5510691 (Why is no real title available?)
• scientific article; zbMATH DE number 1950260 (Why is no real title available?)
• Integrating dependency schemes in search-based QBF solvers
• PSATO: A distributed propositional prover and its application to quasigroup problems
• QBF Resolution Systems and Their Proof Complexities
• Resolution for quantified Boolean formulas
• Theory and Applications of Satisfiability Testing
• Unified QBF certification and its applications

Cited in

(3)

• The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
• \(\mathsf{MPIDepQBF}\): towards parallel QBF solving without knowledge sharing
• HordeSat: a massively parallel portfolio SAT solver

Describes a project that uses

Uses Software

• QUBE
• HordeSat
• MiniSat
• PSATO
• semprop
• Bloqqer
• QMiraXT
• HordeQBF
• MPIDepQBF
• PicoSAT
• Quaffle
• MPI/MPICH
• DepQBF
• SATO

This page was built for publication: HordeQBF: a modular and massively parallel QBF solver

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2818039)