QBF Benchmarks : Sequential Depth Computation

The following Quantified Boolean Formulas (QBFs) encode the problem of computing the sequential depth (diameter) for some of the ISCAS89 circuits. The formulation follows the description in the 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 answers the question: Does [circuit_name] has a new state at depth [n]? If the answer is YES, the instance is satisfiable. Othewise, it is unsatisfiable.

Benchmarks

(Questions/Comments/Corrections, email maherm @ umich.edu)