Downloads



Welcome User's manual Features Downloads Experimental Results Back on my researches


Here are the binary versions of qbfl for Linux x86. Please send me an email if you need a binary for another platform. The source code of the generators is available on demand (beware : most of the comments are in french :)).

  1. qbfl.1.7 (last version)
  2. qbfl.1.5
  3. qbfl.1.3
  4. qbfl.1.1
  5. qbfl.1.0
  6. qbfl.0.3
  7. qbfl.0.2
  8. qbfl.0.1

qbfl is a QBF-solver that uses a SAT-solver called Limmat (version 1.3) as a SAT oracle :

Limmat


It's possible to obtain the following informations (and other ones) on the site consecrated to QBFs :

QBFLib


The solvers that participated to QBF 2003 comparative evaluation :
Solver Contribuited by Translators from QDIMACS to solver input format
Evaluate M. Cadoli, M. Giovanardi, M. Schaerf not available
Decide J. Rintanen QDIMACS to Rintanen
OpenQbf D. Le Berre reads the QDIMACS format
qbfl F. Letombe reads the QDIMACS format
QKN H. K. Büning, M. Karpinski, A. Flögel not available
Quaffle L. Zhang , S. Malik QDIMACS to Quaffle
Quantor A. Biere reads the QDIMACS format
QuBE E. Giunchiglia, M. Narizzano, A. Tacchella reads the QDIMACS format
QSolve R. Feldmann, B. Monien, S. Schamberger QDIMACS to QSolve
SEMPROP R. Letz QDIMACS to SEMPROP
WatchedCSBJ I. Gent , A. Rowley reads the QDIMACS format
WalkQSAT I. Gent , H. Hoos , A. Rowley reads the QDIMACS format

Disponable Benchmarks :
Author
Benchmark Description
C. Scholl and B. Becker
CEfPI, description Checking Equivalence for Partial Implementation problems (true and false)
Guoqiang Pan
MLK Translated formulas from modal logic K. The source benchmark is F. Massaci's TANCS 2000 easy portion. See the author's CADE-19 paper for details
M. Narizzano      
Random Problems, description

k = 2
n = 50 , n = 100 , n = 150

2QBF-5CNF

all true and false instances

k = 3
n = 50 , n = 100 , n = 150

3QBF-5CNF

all true and false instances

k = 4
n = 50 , n = 100 , n = 150

4QBF-5CNF

all true and false instances

k = 5
n = 50 , n = 100 , n = 150

5QBF-5CNF

all true and false instances

A. Ayari
Adder circuit problems (all true)
Adder circuit problems (all false)
D-FlipFlop circuit problems (all false)
Mutex Protocol protocol verification problems (all true)
Szymanski Protocol protocol verification problems (all true)
Von Neumann (all false)
All all Ayari's benchmarks (true and false)
C. Castellini
Toilet A bomb in the toilet, with flushing and indeterminism (all true)
Toilet A bomb in the toilet, with flushing and indeterminism (all false)
Toilet C bomb in the toilet, with flushing but without indeterminism (all true)
Toilet C bomb in the toilet, with flushing but without indeterminism (all false)
Toilet G bomb in the toilet, without flushing and indeterminism (all true)
All all Castellini's benchmarks (true and false)
R. Letz
True Instances a small set of true instances which are hard for tree-based QBF procedures
False Instances a small set of false instances which are hard for tree-based QBF procedures
All all Letz's benchmarks (true and false)
J. Rintanen
Blocks world planning problems in the blocks world (all true)
Blocks world planning problems in the blocks world (all false)
Chain planning problems (all true)
Impl a chain of implications (all true)
Logn instances of conditional planning (all false)
R3cnf (all true)
R3cnf (all false)
Toilet bomb in the toilet planning problems (all true)
Toilet bomb in the toilet planning problems (all false)
All all Rintanen's benchmarks (true and false)
M. Narizzano
Robot Problems, description

d = 2
s = 1 , s = 2 , s = 3 , s = 4 , s = 5 , s = 6 , s = 7 , s = 8 , s = 9 , s = 10

all true and false instances
   

d = 3
s = 1 , s = 2 , s = 3 , s = 4 , s = 5 , s = 6 , s = 7 , s = 8 , s = 9 , s = 10

all true and false instances
   

d = 4
s = 1 , s = 2 , s = 3 , s = 4 , s = 5 , s = 6 , s = 7 , s = 8 , s = 9 , s = 10

all true and false instances
   

d = 5
s = 1 , s = 2 , s = 3 , s = 4 , s = 5 , s = 6 , s = 7 , s = 8 , s = 9 , s = 10

all true and false instances


Letombe Florian