并行SAT求解器中的学习子句最小化
Learned Clause Minimization in Parallel SAT Solvers
摘要：
学习子句最小化（LCM）可以提高现代SAT求解器的性能，特别是在解决困难SAT实例。尽管LCM方法在顺序求解器中取得了成功，但它们并没有广泛地应用于并行SAT求解器中。在本文中，我们探讨了潜在的LCM并行SAT求解器定义多个LCM方法的基础上，子句vivification，比较它们在不同的SAT求解器的运行时间，并讨论性能的收益和损失的原因。结果表明，LCM只提高性能的并行SAT求解器的SAT实例的一小部分。更常见的是，应用LCM会降低性能。只有某些LCM方法能够提高并行SAT求解器的整体性能。
英文摘要：
Learned clauses minimization (LCM) let to performance improvements of modern SAT solvers especially in solving hard SAT instances. Despite the success of LCM approaches in sequential solvers, they are not widely incorporated in parallel SAT solvers. In this paper we explore the potential of LCM for parallel SAT solvers by defining multiple LCM approaches based on clause vivification, comparing their runtime in different SAT solvers and discussing reasons for performance gains and losses. Results show that LCM only boosts performance of parallel SAT solvers on a fraction of SAT instances. More commonly applying LCM decreases performance. Only certain LCM approaches are able to improve the overall performance of parallel SAT solvers.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
