基于MiniSat的多项式方程组求解实现-论文.pdf

《基于MiniSat的多项式方程组求解实现-论文.pdf》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、第29卷第6期重庆理工大学学报(自然科学)2015年6月Vo1．29No．6JournalofChongqingUniversityofTechnology(NaturalScience)Jun．2015doi：10．3969／j．issn．1674-8425(z)．2015．06．015基于MiniSat的多项式方程组求解实现邹湘景，彭伟(国防科技大学计算机学院，长沙410073)摘要：在许多分析验证研究中，经常要对问题中的多项式组进行求解。当多项式方程组规模较大时，求解比较困难，大大限制了分析研究的效率。针对该问题设计了一种算法

2、，将具有一定格式的多项式转化为合取范式形式，使多项式求解问题转化为SAT求解问题。利用SAT求解器MiniSat对二元域上的多项式组进行求解，使得密码分析过程更加高效。实验结果表明：该算法能正确地将多项式进行转化，并能快速利用MiniSat求出结果。关键词：可满足性问题；MiniSat；多项式；合取范式中图分类号：TP302文献标识码：A文章编号：1674—8425(2015)06—0075—07RealizationofSolvingPolynomialSystemofEquationsBasedonMiniSatZOUXiang

3、-jing，PENGWei(CollegeofComputer，NationalUniversityofDefenseTechnology，Changsha410073，China)Abstract：InmanyresearchworksO±formalanalysisandverification，itisoftenrequiredtosolvethepolynomialequationsassociatedwithaproblem．Whenthescaleofthepolynomialequationsislarge，itisd

4、ifficulttogetthesolution，whichgreatlylimitstheeficiencyofanalysis．Tosolvetheproblem，analgorithmwasdesignedinthispaperwhichtransformspolynomi~equationswithacertainformatintoconjunctivenormalforms，thustheproblemofsolvingpolynomialequationscanbeturnedtosolveabooleansatisf

5、iabilityproblem(SAT)．TheSATsolverMiniSatwasappliedtosolvethepolynomialequationsinGF(2)SOthatasolutioncanbefoundquicklyandmaketheanalysismoreeficient．Ex—perimentresultsshowthattheproposedalgorithmcanconvertpolynomialequationscorrectly，andasolutioncanbefoundquicklywithMi

6、niSat．Keywords：booleansatisfiabilityproblem；MiniSat；polynomialequations；conjunctivenormalform当前计算机理论界与逻辑学界共同关注的一个重1背景要问题。SAT问题是第一个被证明的NP完全问题，许多重要而且比较难解决的分析验证与组布尔函数的可满足性问题(即SAT问题)是合问题都可转化成SAT问题，因此对SAT问题的收稿日期：2015—03—22基金项目：国防科技大学预研项目；国家自然科学基金资助项目(61271252，61272010)作者简介：

7、邹湘景(1986～)，男，湖南岳阳人，硕士研究生，主要从事计算机网络信息安全研究；彭伟(1973一)，男，研究员，主要从事计算机网络和网络安全研究。引用格式：邹湘景，彭伟．基于MiniSat的多项式方程组求解实现[J]．重庆理工大学学报：自然科学版，2015(6)：75—81．Citationformat：ZOUXiang-jing，PENGWei．RealizationofSolvingPolynomialSystemofEquationsBasedonMiniSat[J]．JournalofChongqingUniversity

8、ofTechnology：NaturalScience，2015(6)：75—81．76重庆理工大学学报研究在理论和实践方面都非常有意义。许多优秀的SAT求解器的设计实现(例如MiniSat等)使得2相关研究SAT问题能够较快求解。S