脚本宝典收集整理的这篇文章主要介绍了文献学习-Efficient All-UIP Learned Clause Minimization，脚本宝典觉得挺不错的，现在分享给大家，也给大家做个参考。
Efficient All-UIP Learned Clause Minimization
Mathias Fleury and Armin Biere Johannes Kepler UniversITy, Linz, Austria {armin.biere, mathias.fleury}@jku.at
| Abstract. In 2020 Feng & Bacchus revisited VARiants of the all-UIP learning strategy, which considerably imPRoved PErformance of their version of CADical submitted to the SAT Competition 2020, particularly on large planning instances. We improve on their algorithm by tightly integrating this idea with learned clause minimization. This yields a clean shrinking algorithm with complexity linear in the size of the implication graph. It is fast enough to unconditionally shrink learned clauses until completion. We further define trail redundancy and show that our version of shrinking removes all redundant literals. Independent experiments with the three SAT solvers CaDiCaL, Kissat, and Satch confirm the effectiveness of our approach. | |
|
Learned clause minimization [18] is a standard feature in modern SAT solvers. It allows to learn shorter clauses which not only reduces memory usage but arguably also helps to prune the seArch space.译文：它允许学习更短的子句，这不仅减少内存使用，而且可以帮助削减搜索空间。 However, completeness of minimization was never formalized nor proven. Using Horn SAT [9] we define trail redundancy through entailment with respect to the reasons in the trail and show that the standard minimization algorithm removes all redundant literals (Sect. 2). 译文：然而，最小化的完整性从来没有被形式化或证明过。使用Horn SAT[9]，我们根据轨迹中的原因通过蕴涵定义了轨迹冗余，并证明了标准最小化算法消除了所有冗余文字(第2节)。 |
|
|
Minimization, in its original form [18], only removes literals From the initial deduced clause during conflict analysis, i.e., the 1st-unique-implication-point clause [21]. In 2020 Feng & Bacchus [11] revisited the all-UIP heuristics with the goal to reduce the size of the deduced clause even further by allowing to add new literals. 译文：2020年，Feng & Bacchus[11]重新审视了全uip启发式，目标是通过允许添加新的字面量来进一步减少推导出的子句的大小。
In this paper we call such advanced minimization techniques shrinking. In order to avoid spending too much time in such shrinking procedures the authors of [11] had to limit its effectiveness. They also described and implemented several variants in the SAT solver CaDiCaL [2]. One variant was winning the planning track of the SAT Competition 2020. The benchmarks in this track require to learn clauses with many literals on each decision level. 译文：在本文中，我们称这种先进的极小化技术为收缩。为了避免在这种收缩过程中花费太多的时间，[11]的作者不得不限制其有效性。他们还描述和实现了SAT求解器CaDiCaL[2]中的几个变体。其中一个变化是赢得了2020年SAT竞赛的规划轨道。本课程的基准要求学习在每个决策级别上具有许多字面量的子句。 |
|
|
As Feng & Bacchus [11] consider minimization and all-UIP shrinking separately, they apply minimization First, then all-UIP shrinking, and finally again minimization (depending on the deployed strategy/variant), while we integrate both techniques into one simple algorithm. 译文：由于Feng和Bacchus[11]分别考虑最小化和全uip收缩，他们首先应用最小化，然后全uip收缩，最后再次最小化(取决于部署的策略/变量)，而我们将这两种技术集成到一个简单的算法中。 In contrast, their variants process literals of the deduced clause from highest to lowest decision level and eagerly introduce literals on lower levels. Thus their approach has to be Guarded against actually producing larger clauses and can not be run unconditionally (Sect. 3). 译文：相反，它们的变体将推导子句的字面量从最高决策层处理到最低决策层，并急切地在较低的决策层引入字面量。因此，他们的方法必须防止实际产生更大的条款，不能无条件地运行(第3节)。 |
|
|
We integrate minimization and shrinking in one procedure with linear complexity in the size of the implication graph (Sect. 4). Processing literals of the deduced clause from lowest to highest level allows us to reuse the minimization cache, without compromising on completeness, thus making it possible to run the shrinking algorithm unconditionally until completion. On the theoretical side we prove that our form of shrinking fulfills the trail redundancy criteria。 译文：我们将最小化和收缩集成到一个过程中，该过程具有隐含图大小的线性复杂性(第4节)。从最低层到最高层处理推导子句的字面量允许我们重用最小化缓存，而不损害完整性，这样就可以无条件地运行收缩算法直到完成。在理论方面，我们证明了我们的收缩形式满足trail冗余准则。 |
|
| Experiments with our SAT solvers Kissat, CaDiCaL, and Satch show the effectiveness of our approach and all-UIP shrinking in general. Shrinking decreases the number of learned literals, particularly on the recent planning track. We also study the amount of time used by the different parts of the transformation from a conflicting clause to the shrunken learned clause (Sect. 5).译文：用我们的SAT求解器Kissat、CaDiCaL和Satch进行的实验显示了我们方法的有效性和总体上的全uip收缩。收缩减少了学习文字的数量，特别是在最近的计划轨道上。我们还研究了从冲突条款到缩减的学习条款的不同部分所使用的时间(第5节)。 | |
|
Regarding related work we refer to the HandBook of Satisfiability [7], particularly for an introduction to CDCL [17], the main algorithm used by state-of-theart SAT solvers. This work is based on the classical minimization algorithm [18], which Van Gelder [19] improved by making it linear (in the number of literals) in the implication graph without changing the resulting minimized clause. 译文：关于相关工作，我们参考了《满足手册[7]》，特别是对CDCL[17]的介绍，这是目前最先进的SAT求解器使用的主要算法。本文基于经典的最小化算法[18]，Van Gelder[19]对该算法进行了改进，使其在蕴涵图中线性化(字面量的数量)，而不改变得到的最小化子句。
The original all-UIP scheme [21] was never considered to be efficient enough to be part of SAT solvers, until the work by Feng & Bacchus [11]. We refer to their work for a detailed discussion on all-UIPs. Note that, Feng & Bacchus [11] consider their algorithm to be independent of minimization, more like a post-processing step, while we combine shrinking and minimization for improved efficiency. The technical report with the proofs of all theorems is available [13]. 译文：最初的全uip方案[21]从未被认为是有效的，足以成为SAT解决方案的一部分，直到Feng和Bacchus[11]的工作。我们参考他们的工作来详细讨论所有ui。注意，Feng & Bacchus[11]认为他们的算法与最小化无关，更像是一个后处理步骤，而我们将缩小和最小化结合起来以提高效率。所有定理证明的技术报告[13]。 |
|
|
References 1. Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: IJCAI. pp. 399–404 (2009), http://ijcai.org/Proceedings/09/Papers/074. pDF 2. Biere, A.: CaDiCaL, Lingeling, Plingeling, Treengeling and YalSAT entering the SAT Competition 2018. In: Heule, M., J¨arvisalo, M., Suda, M. (eds.) Proc. of SAT Competition 2018 – Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2018-1, pp. 13–14. University of Helsinki (2018) 3. Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Tech. rep., FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University (aug 2021) 4. Biere, A.: The SAT solver Satch. Git repository (2021), https://github.COM/ arminbiere/satch, last Accessed: March 2021 5. Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., J¨arvisalo, M., Suda, M. (eds.) Proc. of SAT Competition 2020 – Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51–53. University of Helsinki (2020) 6. Biere, A., Fr¨ohlich, A.: Evaluating CDCL variable scoring schemes. In: Heule, M., Weaver, S.A. (eds.) SAT 2015. LNCS, vol. 9340, pp. 405–422. Springer (2015). https://doi.org/10.1007/978-3-319-24318-4 29 7. Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009) 8. Cherkassky, B.V., Goldberg, A.V., Silverstein, C.: Buckets, heaps, lists, and monotone priority queues. SIAM J. Comput. 28(4), 1326–1346 (1999). https://doi.org/10.1137/S0097539796313490 9. Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. LOG. Program. 1(3), 267–284 (1984). https://doi.org/10.1016/0743-1066(84)90014-1 10. E´en, N., S¨orensson, N.: An extensible SAT-solver. In: SAT. LNCS, vol. 2919, pp. 502–518. Springer (2003). https://doi.org/10.1007/978-3-540-24605-3 37 11. Feng, N., Bacchus, F.: Clause size reduction with all-UIP learning. In: SAT. LNCS, vol. 12178, pp. 28–45. Springer (2020). https://doi.org/10.1007/978-3-030-51825- 7 3 12. Fleury, M.: Formalization of logical calculi in Isabelle/HOL. Ph.D. thesis, Saarland University, Saarbr¨ucken, Germany (2020), https://tel.archives-ouvertes.fr/ tel-02963301 13. Fleury, M., Biere, A.: Efficient all-UIP learned clause minimization (extended version). Tech. Rep. 21/3, Johannes Kepler University Linz, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2021). https://doi.org/10.350/fmvtr.2021- 3, https://doi.org/10.350/fmvtr.2021-3 14. Hickey, R., Feng, N., Bacchus, F.: Cadical-trail, Cadical-alluip, Cadical-alluip-trail and Maple-LCM-Dist-alluip-trail at the SAT Competition. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., J¨arvisalo, M., Suda, M. (eds.) Proc. of SAT Competition 2020 – Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, p. 10. University of Helsinki (2020) Efficient All-UIP Learned Clause Minimization 17 15. M¨ohle, S., Biere, A.: Backing backtracking. In: SAT. LNCS, vol. 11628, pp. 250–266. Springer (2019). https://doi.org/10.1007/978-3-030-24258-9 18 16. Nadel, A., Ryvchin, V.: Chronological backtracking. In: SAT. LNCS, vol. 10929, pp. 111–121. Springer (2018). https://doi.org/10.1007/978-3-319-94144-8 7 17. Silva, J.P.M., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 131–153. IOS Press (2009). https://doi.org/10.3233/978-1-58603-929-5-131 18. S¨orensson, N., Biere, A.: Minimizing learned clauses. In: SAT. LNCS, vol. 5584, pp. 237–243. Springer (2009). https://doi.org/10.1007/978-3-642-02777-2 23 19. Van Gelder, A.: Improved conflict-clause minimization leads to improved propositional proof traces. In: SAT. LNCS, vol. 5584, pp. 141–146. Springer (2009). https://doi.org/10.1007/978-3-642-02777-2 15 20. Van Gelder, A.: Generalized conflict-clause strengthening for satisfiability solvers. In: SAT. Lecture Notes in Computer Science, vol. 6695, pp. 329–342. Springer (2011). https://doi.org/10.1007/978-3-642-21581-0 26 21. Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in Boolean satisfiability solver. In: ICCAD. pp. 279–285. IEEE Computer Society (2001). https://doi.org/10.1109/ICCAD.2001.968634 |
|
以上是脚本宝典为你收集整理的文献学习-Efficient All-UIP Learned Clause Minimization全部内容，希望文章能够帮你解决文献学习-Efficient All-UIP Learned Clause Minimization所遇到的问题。
本图文内容来源于网友网络收集整理提供，作为学习参考使用，版权属于原作者。
如您有任何意见或建议可联系处理。小编QQ：384754419，请注明来意。