文献学习--Partitioning Methods for Satisfiability Testing on Large Formulas

Methods for partitioning large propositional formulas are investigated,
with the goal of producing a set of smaller formulas whose satisfiability
can be determined within reasonable time frames by known algorithms.
CNF formula partitioning can be viewed as hypergraph partitioning,
which has been studied extensively in VLSI design. Although CNF for-
mulas have been considered as hypergraphs before, we found that this
viewpoint was not productive for partitioning, and we introduce a new
viewpoint in the dual hypergraph. Hypergraph partitioning technology
from VLSI design is adapted to this problem. The overall goal of
satisfiability testing requires criteria different from those used in VLSI
design. Several heuristics are described and investigated experimentally.
Some formulas from circuit applications that were extremely difficult or
impossible for existing algorithms have been solved. However, the
method is not useful on formulas with little or no structure, such as ran-
domly generated formulas.

在对偶超图中引入了一种新的观点。

译文：满足性测试的总体目标要求的标准与VLSI设计中使用的标准不同

译文：对几种启发式进行了描述和实验研究。

译文：该方法对于结构很少或没有结构的公式，如随机生成的公式是没有用的。

The propositional satisfiability decision problem arises frequently as a subproblem in other applications, such as automated verification and automated theorem proving. 译文：命题可满足性决策问题在自动验证和定理自动证明等应用中经常作为子问题出现。

Such applications may generate very large formulas,  some of which are beyond the capabilities of known algorithms. 译文：这样的应用程序可能会生成非常大的公式，其中一些公式超出了已知算法的能力。

Typically, these applications incorporate a satisfiability tester, as a subroutine, that performs well for most of the formulas generated by the application. 译文：通常，这些应用程序将满足性测试器作为子例程合并在一起，该子例程对应用程序生成的大多数公式执行良好。

However, for some formulas it keeps on running beyond acceptable time limits. 译文：然而，对于某些公式，它会持续运行超过可接受的时间限制。

What can the application do?

Some applications can afford to give up and try something else. In other cases, failure to solve this formula is critical and the whole application fails.

Our research is directed toward providing a satisfiability tester of last resort to be brought in on critical formulas where standard methods have failed. 译文：我们的研究是为了提供一个最后的可满足性测试器，用于标准方法失败的临界公式。

This paper summarizes results presented at CADE-13 [PVG96]. The main idea
is to partition a large difficult formula into smaller formulas that (in the worst case)
must each be solved. 译文：其主要思想是将一个大而难的公式分解成较小的公式，(在最坏的情况下)每个公式都必须求解。

However, due to the exponential behavior of all known satisfiability decision algorithms, the smaller formulas may be many orders of magnitude easier for the standard satisfiability subroutine. 译文：然而，由于所有已知的可满足性决策算法的指数行为，对于标准可满足性子程序来说，更小的公式可能更容易多个数量级。

Because of the overhead of formula partitioning, this method would only be invoked when the standard subroutine was unable to solve a problem within reasonable resource limits. 译文：由于公式划分的开销，只有当标准子例程无法在合理的资源限制内解决问题时，才会调用此方法。

The two partitioning methods (see Section 3) incorporate an existing satisfiability tester as a subroutine. 译文：这两种划分方法(见第3节)将现有的可满足性测试程序合并为子程序。

The first heuristic can be combined with any complete satisfiability algorithm.

However, the second heuristic requires limited interaction with the underlying satisfiability algorithm and can be combined with most model searching algorithms, such as variants of the DavisPutnamLovelandLogemann (DPLL) scheme [DP60, DLL62].译文：第二种启发式算法需要与底层满足度算法进行有限的交互，并且可以与大多数模型搜索算法相结合

Our study combined with an existing tester program showed greatly increased efficiency on several circuit formulas that were extremely difficult or impossible for other known methods (see Fig. 3). 译文：我们的研究结合了一个现有的测试程序，在一些电路公式上大大提高了效率，这对于其他已知方法来说是极其困难或不可能的(见图3)。

Both heuristics are based on partitioning the input formula into two or more subformulas.

Partitioning an input formula naturally fits into the hypergraph cut problem, and it represents a process that analyzes the input formula structure.

Methods from VLSI design have been adapted to this problem effectively. 译文：VLSI的设计方法已经有效地适应了这个问题。

To be useful, the cut must achieve some degree of balance in the resulting connected components and must be small in some sense. 译文：为了有用，切割必须在最终连接的部件中达到某种程度的平衡，并且在某种意义上必须很小。

Except for the hyperedges that occur in multiple subformulas, the structural analysis of the input formula results in subformulas that are independent of each other. 译文：对输入公式进行结构分析，除了多个子公式中出现超边外，还得到了相互独立的子公式。

CNF formulas have been studied as hypergraphs before [GU89, GLP93].

The normal approach is to define each clause as a hyperedge connecting all the variables, or perhaps the literals, that occur in the clause. 译文：通常的方法是将每个子句定义为连接子句中出现的所有变量或字面量的超边。

From this viewpoint the hypergraph cut problem consists of finding a favorable set of ``cut‘‘ clauses, such
that, if these clauses are removed from the formula, the remaining variables (the vertices of the hypergraph) fall into two or more groups (connected components) that are not related by any remaining clause. This natural method has not proven successful on large formulas, for reasons discussed in Section 2.

译文：从这个观点来看，超图切割问题包括找到一组有利的“切割”子句，这样，如果这些子句从公式中删除，剩下的变量(超图的顶点)就会落入两个或更多的组(连接组件)，这些组与任何剩余子句都不相关。

The approach introduced here considers the dual of the above hypergraph, which is
also a hypergraph. 译文：本文所介绍的方法考虑了上述超图的对偶，它也是一个超图。

In this new viewpoint, each variable is defined as a hyperedge connecting all the clauses in which it occurs.  译文：在这种新的观点中，每个变量都被定义为连接它所在的所有子句的超边。

Each clause is a vertex now.

In this context the hypergraph cut problem consists of finding a favorable set of cut variables, such that, if these variables are removed from the formula, the remaining clauses fall into two or more groups (connected components) that are not related by any remaining variable. 译文：在这种情况下，超图切割问题包括找到一组有利的切割变量，这样，如果这些变量从公式中移除，其余的子句就会落入两个或更多组(连通分量)，这些组与任何剩余的变量都不相关。

The reason to prefer the dual view of a hypergraph over the normal approach lies
in the eventual application. 译文：选择超图的双视图而不是常规方法的原因在于最终的应用。

At a high level, the partition is used as follows: For
each partial assignment required by the cut set, apply the assignment to the induced
subformulas F1 and F2 , making them independent. Now try to find models of F1
and F2 independently. A model in this context is a partial truth assignment that
satisfies the formula. If this process ever succeeds, a model for the entire formula
has been found. However, to demonstrate unsatisfiability it is necessary to show
that the process fails for all required partial assignments.

The difference between the two hypergraph views lies in what partial assignments are
required. For the usual view, the cut set is a set of clauses, and all partial assignments that 

satisfy this set of clauses are required. The number of variables in this cut set can be
significantly larger than the number of clauses, and the number of satisfying partial
assignments can be exponential in the number of variables involved. The number of
required partial assignments is not directly related to the cardinality of the cut set.

For the new view, the cut set is a set of variables. The required partial
assignments are all partial assignments to these variables that satisfy the clauses (if
any) that consist entirely of variables (positive or negative) in the cut set. While this
number is exponential also, it is directly related to the cardinality of the cut set, so
an algorithm to find small cut sets is more likely to achieve a useful partition.

As further motivation for the new hypergraph view, consider that a formula typi-
cally has more clauses than variables. In VLSI design, there are many more gates,
which correspond to vertices, than wires, which correspond to hyperedges. Thus we
expected that partitioning algorithms from that domain would transfer more
effectively for the new hypergraph view.