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 (Co
alysis) 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.
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) or
7z (13MB) file.
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.
However, for an easy start a package with the output of SApperloT for twenty
instances can be downloaded as tar.gz file (196MB)
or as 7z file (138MB).
You may also want to use a modified version of the MiniSat2.2
core solver that can produce the required output files.
If you have questions or any kind of feedback to the above software please don't hesitate to contact Paul, Stephan