Optimizing backbone filtering
Optimizing backbone filtering
复制标题
优化主干过滤
DOI：
10.1016/j.scico.2019.102374
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Weikai Miao
中科院分区：
文献类型：
--
作者：
Yueling Zhang;Jincao Feng;Weikai Miao
在命题公式中，在每个赋值中将文字赋给True或False。在给定公式的每个可满足的赋值(模型)中，主干文字始终被赋值为True。主干文字是提高SAT测试和基于SAT的应用程序(如模型检查和程序分析)性能的关键。在本文中，我们提出了一种结合COV、WHIT和2LEN策略的优化方法来改进骨干计算。我们已经在EDUCIBone中实现了它。CoV和2LEN用于查找主干文字，WHIT用于查找非主干文字。Cov利用了这样的事实：对于主干文字L，在给定公式ϕ的每个模型v中必须至少存在一个子句Φ，使得对于ϕ中的每一个其他文字L，在v中对L的赋值是假的。WHIT基于这样的事实，对于给定公式Φ的模型v，对于具有L的每个子句ϕ，如果对于具有L的每个子句ϕ，也存在另一个L‘，使得对L的赋值为真，则L是非主干文字。对于直言不讳的L来说，判断L是否是骨干直言不讳的人，天真的方法就是检查L∧Φ和L∧Φ的可满足性。2LEN为L找到了一组唯一的自由文字F L，使得L∧Φ和⋀L的∈F L L的∧Φ的可满足性是相同的。实验表明，在给定公式的主干计算时间小于3000秒时，检验⋀L的∈F L的∧Φ的可满足性比检验L的∧Φ的可满足性要快。当公式计算超过3000秒时，我们停用2LEN策略。我们评估了EDUCIBone在2011至2017年的SAT比赛中使用工业配方奶粉的表现。对EDUCIBone、DUCIBone和MINIBONE-CB100进行了性能比较。结果表明，EDUCIBone求解的公式最多。对于三种工具常用的公式，EDUCIBone从公式计算主干文字的速度最快。并分别对COV、WHIT和2LEN策略的效率进行了详细的实验分析。结果表明，每种策略都对EDUCIBone的性能有贡献，并且它们都适用于各种公式。
In propositional formulas, literals are assigned to True or False in each assignment. Backbone literals are always assigned to True in every satisfiable assignment (model) of the given formula. Backbone literals are keys to improve the performance of SAT testing and SAT-based applications, such as model checking and program analysis. In this paper, we propose an optimized approach that combines COV, WHIT and 2LEN strategies to improve backbone computing. We have implemented it in EDUCIBone. COV and 2LEN are used for finding backbone literals, WHIT is used for finding non-backbone literals. COV uses the fact that for a backbone literal l, there must exist at least one clause ϕ in every model v of the given formula Φ such that for every other literal l′ in ϕ, the assignment of l′ is False in v. WHIT is based on the fact that for a literal l, and a model v of the given formula Φ, if for every clause ϕ that has l, there always exists another l′ also in ϕ such that the assignment of l′ is True, then l is a non-backbone literal. For a literal l, the naive way to decide if l is a backbone literal is to check the satisfiability of l∧ Φ and¬ l∧ Φ. 2LEN finds a set of unique free literals F l for l, such that the satisfiability of¬ l∧ Φ and⋀ l′∈ F l l′∧ Φ are the same. Experiments show that checking the satisfiability of⋀ l′∈ F l l′∧ Φ is faster than checking the satisfiability of¬ l∧ Φ when the backbone computing time of the given formula is less than 3000 seconds. We deactivate 2LEN strategy when the formula has been computed for more than 3000 seconds. We evaluate the performance of EDUCIBone on formulas from industrial tracks in SAT Competitions from 2011 to 2017. Performance comparisons are conducted among EDUCIBone, DUCIBone and minibones-cb100. Results show that EDUCIBone solves the most formulas. For the formulas that are commonly solved by the three tools, EDUCIBone is the fastest in computing backbone literals from the formulas. We also analyze the efficiency of COV, WHIT and 2LEN strategies separately with detailed experiments. Results show that every strategy contributes to the performance of EDUCIBone, and they are all applied to various kinds of formulas.