A QSAT Benchmark Based on Vertex-Folkman Problems (Student Abstract)

Solving times with 3 different QSAT solvers that support the QDIMACS format, namely DepQBF [7], RAReQS [6], and caqe [8] are summarized in Table 1 . This table also includes information about some of the flags we considered for each solver that seemed promising in the sense that they improved the solving time for certain instances: for DepQBF we tried traditional QCDCL and for caqe we tried disabling expansion refinement. One can notice from Table 1 that RAReQS seems to outperform the other solvers at any parameter setting, though at the time of this writing we have not investigated if this is always the case and what is the reason. Table 2 shows the running times of the QFUN [5] (with and without strategy learning), CQESTO [4] and QuAbS 1 [2] QSAT solvers which take circuits in the QCIR-14 format as input. We looked at the task of listing all solution of graph searches up to order 8 without isolators. The comparison is between sat-to-sat's model enumeration feature [3], our own implementation of a simple AllQSAT model enumerator for the QDIMACS format based on DepQBF's C API using a blocking-clause approach, and QFun's top-level winning move enumeration feature. The results are shown in Table 3 .