CoPAn

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) or 7z (13MB) file.

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. 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.

Related Publications

If you have questions or any kind of feedback to the above software please don't hesitate to contact Paul, Stephan or Christian via
algoCoPAninformatik.unituebingen.de

--> Our website has moved permanently to https://uni-tuebingen.de/fakultaeten/mathematisch-naturwissenschaftliche-fakultaet/fachbereiche/informatik/lehrstuehle/algorithmik/home/!

Impressum Datenschutzerklärung

Universität Tübingen	Fakultät > Wilhelm-Schickard-Institut > Algorithmik > Forschung > Algorithm Engineering > CoPAn: Conflict Pattern Analysis

	Software \| HowTo \| Related Publications CoPAn 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) or 7z (13MB) file. 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. 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. Related Publications If you have questions or any kind of feedback to the above software please don't hesitate to contact Paul, Stephan or Christian via algoCoPAninformatik.unituebingen.de --> Our website has moved permanently to https://uni-tuebingen.de/fakultaeten/mathematisch-naturwissenschaftliche-fakultaet/fachbereiche/informatik/lehrstuehle/algorithmik/home/!
Impressum Datenschutzerklärung