文献学习——MUStICCa: MUS Extraction with Interactive Choice of Candidates

Existing algorithms for minimal unsatisfiable subset (MUS)
extraction are defined independently of any symbolic information, and
in current implementations domain experts mostly do not have a chance
to influence the extraction process based on their knowledge about the
encoded problem.　译文：在目前的实现中，领域专家大多没有机会影响提取过程。

The MUStICCa tool introduces a novel graphical user
interface for interactive deletion-based MUS finding, allowing the user to
inspect and influence the structure of extracted MUSes.

The tool is centered around an explicit visualization of the explored
part of the search space, representing unsatisfiable subsets (USes) as
selectable states.

While inspecting the contents of any US, the user
can select candidate clauses to initiate deletion attempts.

译文：当检查任何US的内容时，用户可以选择候选子句来发起删除尝试。

The reduction
steps can be enhanced by a range of state-of-the-art techniques such
as clause-set refinement, model rotation, and autarky reduction．

MUStICCa
compactly represents the criticality information derived for the
different USes in a shared data structure, which leads to significant savings
in the number of solver calls when multiple MUSes are explored.

For automatization, our tool includes a reduction agent mechanism into
which arbitrary user-implemented deletion heuristics can be plugged.　

With a remarkable amount of recent work (e.g. [13,3,17]) on algorithms for computing
minimal explanations of SAT formula unsatisfiability and a broad range
of applications (e.g. [15,12]), the field of minimal unsatisfiable subset (MUS) extraction
has become an emerging research field in the SAT community, leading
to the introduction of a MUS track in the SAT competition 2011 [16].

译文：最小不可满足子集(MUS)提取领域已经成为SAT社区的一个新兴研究领域，导致2011年SAT竞赛[16]引入了一个MUS轨道。

The algorithms for MUS extraction can be characterized as constructive, destructive
or dichotomic [6,14], but they all focus solely on the amount of clauses
or clause sets (called groups) [2] present in the minimal explanation.

We introduce a completely new approach to guiding the destructive MUS
extraction algorithm by Nadel [11]. 译文：我们介绍了一种全新的方法来指导nadel[11]的破坏性MUS提取算法

The central idea of destructive MUS extraction,
which was first proposed more than 20 years ago [4,1], is to perform
a series of reduction steps, moving into smaller unsatisfiable subsets F until all subsets F ? F are satisfiable.

The idea of interactive MUS extraction
is to give a user full control over the individual reduction steps, providing an
interface for interactively focusing on or eliminating parts of the search space. 译文：交互式MUS提取的思想是让用户完全控制单个缩减步骤，提供一个界面，以交互方式关注或消除部分搜索空间。

Within our MUStICCa tool, this is done by reverting to intermediate results, the
non-minimal unsatisfiable subsets, and exploring new parts of the search space
by choosing alternative deletion candidates. 译文：这是通过恢复中间结果，即非最小不可满足子集，并通过选择替代删除候选来探索搜索空间的新部分来实现的。

This feature will not only help domain
experts (who usually have good intuitions about the clauses relevant for
good explanations) to find meaningful explanations of unsatisfiability, but also
researchers and students in analysing unsatisfiable instances and evaluating the
effects of different heuristics for selecting deletion candidates.

译文：这一特性不仅有助于领域专家(他们通常对好的解释相关的条款有良好的直觉)找到不满足的有意义的解释，而且有助于研究人员和学生分析不满足的实例，评估不同启发式选择删除候选的效果。

By default, MUStICCa’s graphical user interface (see Figure 1) consists of
three main view components.

The central view is a representation of the current
knowledge about the search space. Explored USes are inspected in a separate US
view which also provides the interface for starting reduction steps. The third view
is responsible for administering automated reduction agents.

Our tool automatically
avoids unnecessary deletion tests by efficiently representing and reusing all
the clause criticality information that was gained anywhere in the search space.

The paper is organized as follows: Section 2 introduces the user interface, describes
the main features, and gives some pointers to interesting implementation
details. Section 3 describes some of our practical experiences with using the tool
for an application.We conclude with a short summary in Section 4.

The tool can
be downloaded from http://algo.inf.uni-tuebingen.de/?site=forschung/
sat/MUStICCa.