快速高质量的阻塞子句分解
Fast Blocked Clause Decomposition with High Quality
摘要：
任何CNF公式都可以分解为两个阻塞子集，使得两者都可以通过BCE（阻塞子句消除）求解。为了使分解更有用，人们希望分解尽可能不平衡。实现这一目标往往需要时间。到目前为止，已经有几个分解和后处理算法，如PureDecompose，QuickDecompose，MixerMover等，我们发现，这些现有的算法往往是低效或低质量的分解。本文旨在提高分解质量，同时保持算法的运行时间控制。为了实现这一目标，我们改进了现有的BCE，并提出了两个新的变种PureDecompose，一个新的启发式分解称为LessInterfereDecompose，和一个新的后处理算法称为RsetGuidedDecompose。将这些新技术结合在一起，产生了一种名为MixDecompose的新算法。在我们的实验中，不存在PureDecompose+ MixDecompose的质量优于MixDecompose的应用程序公式。在速度方面，MixDecompose也非常快。我们的平均运行时间有点长，但最坏情况下的运行时间更短。理论上，我们的两个PureDecompose变体需要子句数量的线性时间。通过限制BCE使用的触摸列表的大小，我们可以保证MixDecompose总是在线性时间内运行。
英文摘要：
Any CNF formula can be decomposed two blocked subsets such that both can be solved by BCE (Blocked Clause Elimination). To make the decomposition more useful, one hopes to have the decomposition as unbalanced as possible. It is often time consuming to achieve this goal. So far there have been several decomposition and post-processing algorithms such as PureDecompose, QuickDecompose, EagerMover etc. We found that these existing algorithms are often either inefficient or low-quality decomposition. This paper aims at improving the decomposition quality, while keeping the runtime of algorithms under control. To achieve this goal, we improve the existing BCE, and present two new variants of PureDecompose, a new heuristic decomposition called LessInterfereDecompose, and a new post-processing algorithm called RsetGuidedDecompose. Combining these new techniques results in a new algorithm called MixDecompose. In our experiments, there is no application formula where the quality of PureDecompose+EagerMover is better than MixDecompose. In terms of speed, MixDecompose is also very fast. Our average runtime is a little longer, but the worst-case runtime is shorter. In theory, our two variants of PureDecompose requires linear time in the number of clauses. By limiting the size of the touch list used by BCE, we can guarantee always that MixDecompose runs in linear time.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
