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

  1. the possibility of having a QBF competition
  2. the possibility of having new Benchmarks
  3. the possibility of having QBF Standard Format
  4. the possibility of developing Incomplete QBF Solvers
  5. where the Next QBF Workshop will be held

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. It was decided that the next QBF Workshop will be held in Genoa in connection with SAT - 2003