| Author | Benchmarks | | M. Mneimneh and K. A. Sakallah | The following Quantified Boolean Formulas (QBFs) encode the problem of computing the sequential depth (diameter) for some of the ISCAS89 circuits. For a detailed description of the problems see the related paper: M. Mneimneh, and K. Sakallah, "Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution," Sixth International Conference on Theory and Applications of Satisfiability Testing, 2003. Each file name has the following format [circuit_name]_d[n]_[s/u].qcnf where - [circuit_name] : name of ISCAS89 circuit
- [n] : n is the depth
- [s/u] : s indicates that the instance should be satisfiable while u indicates that the instance should be unsatisfiable
The QBF instance for a given file name checks whether [circuit_name] has a new state at depth [n]? If the answer is YES, the instance is satisfiable. Othewise, it is unsatisfiable. - all, all the problems below in a single (huge) .tar.gz file.
- s1196, s1269, s27, s298, s3271, s3330, s386, s499, s510, s641, s713, s820, .tar of some of the ISCAS89 circuits divided by name.
| | I. P. Gent and A. Rowley | These problems are QBF encodings of the famous "Connect 4" (Forza 4) game, in some of its possible variants. On a grid of width W and height H, the player has to place N tokens of the same colour, either in a row, or in a column, or diagonally. When W=7, H=6, and N=4, this is exactly the Connect 4 game. In order to translate the instances into QBFs, we had to specify who is to win the game. The name of the instances is cf_N_WxH_R.qdimacs, where: - W,H and N are the parameters of the Connect N game
- R is the result: 'r' if the red wins, 'w' if the white wins, and 'd' if there is a draw.
For more information, see the technical report about generating ConnectN problems. | | 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 |
| </TR | | M. Narizzano | | | A. Ayari | | | 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 |
|
|