Summary of QBF Session
(prepared by Massimo Narizzano, University of Genoa, http://www.mrg.dist.unige.it/~mox/)
This is a brief summary of the points made during the QBF workshop
panel discussion in Cincinnati on May, 7 2002. What follows are some of
the points done during the discussion following the panel presentations.
The topics covered by the panelists, H.K. Buning, I. Gent,
E. Giunchiglia and T.Walsh, are not reported.
The discussion following the panel presentations was about
- the possibility of having a QBF competition
- the possibility of having new Benchmarks
- the possibility of having QBF Standard Format
- the possibility of developing Incomplete QBF Solvers
- where the Next QBF Workshop will be held
- Since the SAT competition had a lot of success, someone proposed the
possibility of having a QBF competition the next year.
All the people agreed that having a QBF Competition as in SAT is a
not good idea because the field is not mature enough. However, there
was consensus about having a comparative non-competitive evalutation.
- Connected to the problem of the comparative evaluation, the point
that there are not many benchmarks available was raised. The solution
pointed out was to have a call for benchmarks, similar to the one
done for the SAT 2002 competition.
- Also connected to the comparative evaluation, the point that every
solver has a different input syntax was raised.
The community want to suggest a standard format to present
problems to a QBF solver. After a brief discussion on the Q-DIMACS
format and Rintanen's format, there was more consensus on using the
Q-DIMACS format. Massimo (myself) agreed to convert all the available
benchmarks on qbflib in Q-DIMACS format,and to make available the converter
from Rintanen's to Q-DIMACS format.
- A more technical discussion was on ``How to construct an
Incomplete QBF Solver''. This discussion started from the
consideration that there are no QBF incomplete solvers available, and
that it is not trivial how to construct one.
Some ideas were briefly discussed.
- It was decided that the next QBF Workshop will be held in Genoa in
connection with SAT - 2003