启发式极性决策算法解SAT问题.pdfVIP

孛国瓣攀嚣辑：信息辩学 2007年第37卷第12期：1597—1606 《中隧猎学》杂恚社 SCIENCEIN http：／／www．scichina．com CHINAPRESS 启发式极性决策算法解SAT问题 荆明娥p 周 电1，2唐璞山1周晓方1 张 华2 ofElectrical (1．复旦大学微电子研究院，专用集成电路国家重点实验室，上海201203；2．Department ofTexasat Engineering，TheUniversity Dallas，Texas75083，US) 摘要 提出了一种启发式极性决策的可满足性问题(SAT)新算法．该算法继承 了当前SAT解决器的许多策略：快速BCP、子句记录、重启动有哪些信誉好的足球投注网站等．同时，该 算法通过预先根据Kamaugh鬻的覆盖分布计算交量援性，将其加入到DPLL酶决 策过程中，大大降低了有哪些信誉好的足球投注网站过程中的冲突次数．实验表明采用该算法的解决 实铡。尤其是对于Bart基准系刿中的每个实镶，DiffSat都能够在0。03S内解 决，而Zchaff和MiniSat在给定的900S内不能够解决大部分实例．而且，DiffSat 解决器在莱些实铡上媳特性远远侥予具有代表性熊基于不完全随机算法的怨决 器DLM． 关键词 霹瀵是蛙问题DPLL宠全算法变量决策 l 引言 生成、时序分析、逻辑验证、等价性验证等。因此，高效实用的SAT算法是目前研究的热点¨。 满是实例上的整体效采不如不完全篱法．而在许多应用领域，如EDA的等价性验证或者淄性 检验需要证明一个实例不满足，因此，DPLL完全算法受到更为广泛的关注【23】．在引入冲突学 习，两个溉察变燕的BCP等燕略后，DPLL算法取得了缀大的突破。诤多当前最有效的解决器 数璃爱期：2006-10-16；接受毯羯：2006-12-06 科学基众(批准号：KLHl202005)和上海市自然科学基金(批准号：06ZRl4016)资助项目 $联系人，E—mail：mejing@fudan．edu．cn 1)http：／／fmv．jku。at／sat-race一2006tiadex．hmal 1598 中国科学E辑信息科学 第37卷 24 很长时间(LL女Hh)内仍然不能够给出问题的解或者证明无解． 本文提出了一种启发式极性决策的完全算法，对于许多满足的实例，基于新算法的解决 器DiffSat比当前的完全算法有更好的特性．同时，DiffSat能够证明实例的不可满足性． 本文的组织结构如下：第2部分回顾了DPLL的基本框架，重点讨论了决策策略．第3部 的变量极性取值联系起来，最后将其集成到DPLL过程中，应用于分支变量的极性决策．第4 特性．最后给出了本文的结论． 2 DPLL算法及变量极性决策 给定一个命题公式，Boole可满足性问题判定是否存在一组变量赋值使得公式为真．如果 这样的赋值存在，则公式是可满足的，否则公式不满足． normal 通常可满足性问题用合取范式(CNF,con{unctiveform)表示．合取范式由若干个子 句“相与”(^)组成，每个子旬由若干个文字“相或”(v)构成．子句用C表示，每个文字是由变 量的正相位(正极性)或反相位(反极性)构成．例如公式(1)是一合取范式． C=(而vz3)A(XV_2VX4)^(而v_2)． (1) 基本的DPLL算法是一个变量决策和有哪些信誉好的足球投注网站的迭 代过程，如算法1所示．所