Department of Computer Science

CoPAn: Conflict Pattern Analysis

Even though the CDCL algorithm and current SAT solvers perform tremendously well for many industrial instances, the performance is highly sensible to specific parameter settings.
Slight modifications of a CDCL solver may cause completely different solving behaviours for the same benchmark. A fast run of a solver is often related to the notion of learning "good clauses".
Our tool CoPAn (Conflict Pattern Analysis) allows the user for an in-depth analysis of conflicts and the associated process of producing learnt clauses. The main attention is drawn to the analysis and comparison of patterns within the resolution operation for different conflicts. Recurring patterns of resolution can be related to several properties of conflicts - configurable by the user. For basic use CoPAn expects common proof logging output of any CDCL solver.

Software

CoPAn is a tool for in-depth analysis of conflicts and the associated process of producing learnt clauses (Conflict Pattern Analysis). The tool is written in Java with the help of efficient external data structures. The package contains a preprocessor, a GUI version, a console-only version and a User-Guide. It is available for download as tar.gz (25MB).

Getting started with CoPAn

  • Be sure to read the User-Guide.
  • CoPAn expexts particular output of a CDCL SAT solver which is very similar to common proof logging output. You may also want to use a modified version of the MiniSat2.2 core solver.