静态信息挖掘与使用——文献学习--Variable Ordering for Efficient SAT Search by Analyzing Constraint-Variable Dependencies

This paper presents a new technique to derive an initial static variable ordering for efficient SAT search. Our approach not only exploits variable activity and connectivity information simultaneously, but it also analyzes how tightly the variables are related to each other.译文：本文提出了一种新的技术来推导初始静态变量的排序，以实现高效的SAT搜索。译文：我们的方法不仅同时利用变量活动和连接信息，而且还分析变量之间的紧密关系。

For this purpose,a new metric is proposed - the degree of correlation among pairs of variables. Variable activity and correlation information is modeled (implicitly) as a weighted graph.译文：为此，提出了一种新的度量——变量对之间的关联度。变元活跃度和相关性的信息被建模(隐式)为一个加权图。

A topological analysis of this graph generates
an order for SAT search. Also, the effect of decision-assignments on
clause-variable dependencies is taken into account during this analysis.
An algorithm called ACCORD (ACtivity - CORrelation - ORDering) is
proposed for this purpose. Using efficient implementations of the above,
experiments are conducted over a wide range of benchmarks. The results
demonstrate that: (i) the variable order generated by our approach significantly
improves the performance of SAT solvers; (ii) time to derive this
order is a fraction of the overall solving time. As a result, our approach
delivers faster performance as compared to contemporary approaches.