CoPAn: Exploring Recurring Patterns in Conflict Analysis of CDCL SAT Solvers (Tool Presentation)
Stephan Kottler, Christian Zielke, P.P. Seitz, Michael Kaufmann · Theory and Applications of Satisfiability Testing · 2012
Even though the CDCL algorithm and current SAT solvers perform tremendously well for many industrial instances, the perfor- mance is highly sensitive to specific parameter settings. Slight modifi- cations 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 iso- morphic 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. 1 Introduction and Motivation Though the vast success of the CDCL approach to SAT solving (12,16,6) is well-documented, it is not fully understood, why small changes in the choice of parameters may cause significantly different behavior of the solver. With the tool presented in this paper, we provide a perspective to find an answer for the question about subtle differences between successful and rather bad solver runs. Our tool CoPAn, an abbreviation for Conflict Pattern Analysis, can be used to analyse the complete learning and conflict analysis of a CDCL solver using the common proof logging output of the systems. Due to the use of efficient external data structures, CoPAn manages to cope with a big amount of logged data. The influence of learning to the SAT solvers' efficiency is undeniable (10). On the one hand new measures for the quality of learnt clauses based on the obser- vation of CDCL solvers on industrial instances (4) were proposed. On the other hand it is very promising to turn away from these static measures that cause a definitive elimination of clauses and focus on a dynamical handling of learnt clauses (3). Therefore changes in learning schemes can lead to a considerable speed-up of the solving process (see (15,4,8)). We are convinced that CoPAn can help to obtain a better understanding about when and how good clauses are learnt by the SAT solver. We provide a tool for in-depth analysis of conflicts and the associated process of producing learnt clauses.