Abstract
Even though the CDCL algorithm and current SAT solvers perform tremendously well for many industrial instances, the performance is highly sensitive to specific parameter settings. Slight modifications may cause completely different solving behaviors for the same benchmark. A fast run is often related to learning of 'good' clauses. Our tool CoPAn allows the user for an in-depth analysis of conflicts and the process of creating learnt clauses. Particularly we focus on isomorphic patterns within the resolution operation for different conflicts. Common proof logging output of any CDCL solver can be adapted to configure the analysis of CoPAn in multiple ways. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Kottler, S., Zielke, C., Seitz, P., & Kaufmann, M. (2012). CoPAn: Exploring recurring patterns in conflict analysis of CDCL SAT solvers (Tool presentation). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7317 LNCS, pp. 449–455). https://doi.org/10.1007/978-3-642-31612-8_36
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
