使用工具CoPAn(冲突模式分析)深入分析冲突产生及所学从句

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.

我们的工具CoPAn(冲突模式分析)允许用户深入分析冲突和产生所学从句的相关过程。

主要关注的是对不同冲突的归结操作中的模式进行分析和比较。

反复出现的归结模式可以与冲突的几个属性相关——可由用户配置。

对于基本用途，CoPAn期望任何CDCL求解器的通用证明日志输出。

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.

 CoPAn User-Guide

Stephan Kottler, Christian Zielke, Paul Seitz, Michael Kaufmann University of T¨ubingen, Germany

1 Working with CoPAn

CoPAn is a Java tool to analyse CDCL SAT solvers. It allows the user for an indepth 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.

我们特别关注不同冲突的解析操作中的同构模式。

任何CDCL求解器的公共证明日志记录输出都可以调整为以多种方式配置CoPAn分析。

1.1 The Input

CoPAn requires a special input, containing the following files for a solver run of one instance:

• A *.clses file containing all clauses of the original formula in addition to all learnt clauses. This file may also contain information about the (possibly) deleted learnt clauses. Additional key-value pairs can be used to add userdefined properties to clauses as shown in Figure 1.

*.clses文件，包含原始公式的所有子句以及所有学过的子句。该文件还可能包含有关(可能)已删除的学过的子句的信息。可以使用其他键值对向子句添加用户定义的属性，如图1所示。

• A *.confl file containing all learnt conflicts with the clauses that cause the specific reasoning. An example is given in Figure 2.

*.conf文件中包含了所有学习到的与引起具体推理的子句的冲突。图2给出了一个示例。

Both files can be produced by common CDCL solvers with only small changes in the source code and should be named identically (excluding the file ending).

 Both files can be produced by common CDCL solvers with only small changes in the source code and should be named identically (excluding the file ending).

A line within the file (Figure 1) either states a single clause or a run of the garbage collector that deleted a subset of clauses. If the line represents a clause, it starts with an integer as identifier, followed by the list of literals defining the clause.

After the last literal of the clause, additional properties of the clause can be added using a pair of a single character and a numerical value. The single character is the identifier (key) of the additional value and has to be defined in the .config file used in CoPAn.

在子句的最后一个字面值之后，可以使用一对单个字符和一个数值来添加子句的其他属性。单个字符是附加值的标识符(键)，必须在CoPAn中使用的.config文件中定义。

If the line represents a run of the garbage collector it starts with ’GC’, followed by the ID of the last clause (written in angle brackets) that was learnt before the call to the garbage collector. The remaining line lists all deleted clauses, identified by their IDs (separated by space characters).

如果该行表示垃圾收集器的运行，则以' GC '开头，后跟在调用垃圾收集器之前学习到的最后一个子句的ID(写在尖括号中)。剩下的一行列出所有删除的子句，由它们的id标识(用空格字符分隔)。

In this example the clause with identifier ’3’ contains three literals, caused a backjump by seven levels (b 7) and has an LBD value of 2 (l 2). The last line of the shown excerpt of a *.clses file denotes that after clause ’7’ has been learnt, the garbage collector deleted the clauses ’4’ and ’3’ from the data base.

Each line within the file (Figure 2) represents one conflict. It starts with the list of clause identifiers (as specified in the .clses file). This list contains all clauses that cause a conflict via a sequence of resolutions. The integer after the colon states the ID of the clause which is learnt by this conflict. In this example the clause with ID ’861’ is learnt due to a resolution of clauses ’145’ and ’219’.

文件中的每一行(图2)表示一个冲突。它从子句标识符列表开始(在. classes文件中指定)。此列表包含通过一系列解析导致冲突的所有子句。 

If a user chooses to log and analyze additional properties for clauses the properties have to be defined in a *.config file for CoPAn.

如果用户选择记录和分析子句的附加属性，则必须在*.config配置文件中定义属性。

An example for such a file is shown in Figure 3. The purpose of an extra *.config file is to keep log files as small as possible by simultaneously having understandable property names for the GUI.

A line within the file (Figure 3) represents a key, that can be added for any defined clause in the *.clses file, as anticipated in Figure 1.

Any line starts with a single character that identifies the key, followed by the default value and an understandable name for the property. All three information are separated by a single space character, therefore the name is prohibited to contain any other space characters. The default value is used for every clause, that does not specify a value for this particular key.

任何一行都以标识键的单个字符开头，后跟默认值和属性的可理解名称。所有三个信息由一个空格字符分隔，因此名称禁止包含任何其他空格字符。默认值用于每个子句，该子句不指定此特定键的值。

 1.2 How to install CoPAn

After downloading CoPAn from http://algo.inf.uni-tuebingen.de/?site= forschung/sat/CoPAn, the package has to be extracted to any directory.

1.3 Preprocessing the input

Before CoPAn can be used to analyse resolution patterns, a preprocessing of the input files (generated by preceding solver runs) is required to create the external data structures. The bulk of computation is done at this stage to enable quick computations when working with the main tool. The preprocessing of two files (inputfilename.clses and inputfilename.confl) can be started by using the command