关于变元极性选择策略

New Boolean satisfiability problem heuristic strategy: Minimal Positive Negative Product Strategy

@article{DBLP:journals/corr/abs-2310-18370,
  author       = {Qun Zhao and
                  Xintao Wang and
                  Menghui Yang},
  title        = {New Boolean satisfiability problem heuristic strategy: Minimal Positive
                  Negative Product Strategy},
  journal      = {CoRR},
  volume       = {abs/2310.18370},
  year         = {2023},
  url          = {https://doi.org/10.48550/arXiv.2310.18370},
  doi          = {10.48550/ARXIV.2310.18370},
  eprinttype    = {arXiv},
  eprint       = {2310.18370},
  timestamp    = {Thu, 02 Nov 2023 17:30:29 +0100},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2310-18370.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

 摘要：

This study presents a novel heuristic algorithm called the "Minimal Positive Negative Product Strategy" to guide the CDCL algorithm in solving the Boolean satisfiability problem. It provides a mathematical explanation for the superiority of this algorithm over widely used heuristics such as the Dynamic Largest Individual Sum (DLIS) and the Variable State Independent Decaying Sum (VSIDS). Experimental results further confirm the effectiveness of this heuristic strategy in problem-solving.

最小正负产品策略启发式的数学解释。

 主要技术路线介绍：

If a heuristic algorithm learns fewer clauses compared to others during problem-solving, it clearly indicates improved efficiency.译文：如果启发式算法在解决问题时学习的子句比其他算法少，则明显表明效率提高了。

This study shifts the focus from clause removal back to proposing a heuristic strategy superior to Chaff’s VSIDS. Firstly, the study introduces a straightforward method Positive Negative Product (PN product) to assess the complexity of SAT problems and validates its effectiveness. Secondly, it discusses how to improve DLIS and VSIDS by building upon the PN product. Finally, it demonstrates the effectiveness of the new heuristic strategy Minimal Positive Negative Product Strategy through experimentation. When solving SAT problems of similar complexity, it learns fewer clauses, affirming the success of this improvement.译文：这项研究将重点从子句删除转移回提出一种优于箔条干扰的虚拟入侵检测系统的启发式策略。首先， 本研究引入了一种简单的方法&正负乘积法来评估SAT的复杂性 问题并验证其有效性。其次，讨论了如何通过在 PN产品。最后，证明了新的启发式策略最小正负乘积的有效性 通过实验制定策略。当解决类似复杂性的SAT问题时，它学习的从句更少，肯定 这一改进的成功。