MPIDepQBF: Towards parallel QBF solving without knowledge sharing. Inspired by recent work on parallel SAT solving, we present a lightweight approach for solving quantified Boolean formulas (QBFs) in parallel. In particular, our approach uses a sequential state-of-the-art QBF solver to evaluate subformulas in working processes. It abstains from globally exchanging information between the workers, but keeps learnt information only locally. To this end, we equipped the state-of-the-art QBF solver DepQBF with assumption-based reasoning and integrated it in our novel solver MPIDepQBF as backend solver. Extensive experiments on standard computers as well as on the supercomputer Tsubame show the impact of our approach.
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
- Pulina, Luca; Seidl, Martina: The 2016 and 2017 QBF solvers evaluations (QBFEVAL’16 and QBFEVAL’17) (2019)
- Balyo, Tomáš; Lonsing, Florian: Hordeqbf: A modular and massively parallel QBF solver (2016)
- Tentrup, Leander: Non-prenex QBF solving using abstraction (2016)
- Jordan, Charles; Kaiser, Lukasz; Lonsing, Florian; Seidl, Martina: (\mathsfMPIDepQBF): towards parallel QBF solving without knowledge sharing (2014)