基于代数几何的可满足性问题连续求解方法研究

《基于代数几何的可满足性问题连续求解方法研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、＇＇挺－义亩門．＇々八＇：．．：為带＇％１＾．Ｖ１？‘学校代码１０６０８机指．；．或、．＾．ｉ．ｖ－式：；＇Ｖ＾，；？＇２０１３０８１２０３巧２、、兰学号荀，、／定：￣￣乂辱寒匡：：＇心‘密级公开严：．名；巧；式Ｍ’’一‘＾，？；？ｓ；矿乂，ｒ＇＇—＇，，＾，１．：欢：＇．若？＇，＞弓＇／４巧＾氏＾矣於葦广ＧｕａｎｘｉＵｎｉｖｅｒｓｉｔｏｒＮａｔｉｏｎａｌｉｔｉｅｓ＠ｇｙｆ硕壬学佐备文選．＞、－乂．．＼，Ｖｒ

2、基于代数几何的可满足性问趣连续求解方法研究，一人＇—‘二；－勺《瓜，，＿＞一＇—－＇＂＇＇‘．一乎户二。。，一：馬；／乎．７．１：；＾苗研究生巧名：斩庆庚Ｍ－ＶＩ导师姓名职觀：吴尽巧教授／！ｔ学科专业：计算机应用技术所届学院：信息科学与工程学院§ｆ年级：２０１３级Ｃ／丈论文完成时间：２０１６年４月‘＇户．／．．立．；：声；；．｜‘刀某摩＾．．參嗎论文独创性声明本人郑重声明：所提交的学位论文，是本人在导师的指导下，独立撰写完成的。除文中己经注明引用

3、的内容外，本论文不含其他个人或其他机构己经发表或撰写娃的研究成果，也没有劃窃、抄袭等违反学术道德规范的侵权行为。对本文的研究做出重要贡献的个Ａ和集体，均已在文中明确方式标明。本人愿意承担由本声明而引起的法律责任。、研究生签名：曰期；＞４年６月曰寺良良论文使用授权声明本人完全了解广西民族大学有关保留、使用学位论文的规定。学校有极保留并向国家有关部口或机构送交学位论文的复印件和电子文档，可采用影印、缩印或其他复制手段保存、汇编学位论文。除在保密期内的保密论文外，允许学位论文被查阅和借阅，可公布（包

4、括刊登）论文的全—部或部分巧容。研巧生签名：知若曰期：抑長年（月／〇曰奇气导师签名：一曰期；如／＾年｜（月／。曰广西民族大学硕士学位论文摘要基于代数几何的可满足性问题连续求解方法研究摘要布尔可满足性问题（SAT问题）是计算科学里的理论问题，目前已经被广泛应用于设计验证和测试产生、等价性校验、性质检验以及微处理验证、软件验证和调试等诸多问题。代数几何方法用于解决布尔可满足性问题时，是把布尔问题转化成求多项式组的零点问题，这样把传统用来解决SAT问题时的逻辑判断问题转化成了计算问题，为SAT问题的求解带来了新的数学方法

5、。在连续建模方面，本文主要基于两种模型，即物理模型和代数几何建模；在零点判定方面，本文采用了Gröbner基和三角列两种求解方法，最终构建了一种完整且实用的SAT问题的连续求解框架。通过实例计算，验证了本文提出的方法是可行的。此外在解决一些实际问题时，由于SAT问题中的CNF公式表达能力有限，因此，这就需要表达能力更强的一阶逻辑公式来表示，本文采用了代数几何的方法对实数域上多项式理论下的可满足性问题模理论（SMT问题）展开研究，主要的思路是把实数域上的多项式理论模型中含有量词的多项式公式通过量词消去转化成与之等价的无量词多项式公式，这

6、样原模型就转化成了不含有量词的一个公式。由于每一个子句都是多项式公式，此时找出满足模型的赋值就相当于求所有的子句组成的方程组的解，这样又把判定问题转化成了计算问题，之后再对方程组进行求解，如果方程组在实数域上有解，就证明了原模型是可满足的；否则，原模型不可满足。本文用代数几何方法对可满足性问题的建模、求解进行了研究，并对实数域上多项式的可满足性模理论进行了研究，这些都为可满足性问题带来了新思路和新方法，最后又通过实例证明了这些方法的可行性与正确性。关键词：布尔可满足问题Gröbner基三角列代数几何零点判定可满足性模理论I广西民族大学

7、硕士学位论文ABSTRACTThecontinuesolutionofSATwithalgebraicgeometryABSTRACTBooleansatisfiabilityproblem,knownasSAT,isoneofthebasictheoreticalproblemsofcomputerscience,whichhasbeenstudiedinlongtimeandwidelyappliedintheverificationandtestingofdiscreteeventsystems,softwarevalidati

8、on,debugging,andmanyotherregions.WestudythealgebraicgeometrymethodtosolveaSATproblem,e.g.,expressingaconcreteS