MiniSAT求解器在判定可满足性问题中的应用  

Application of MiniSAT Slover for Judging Satisfactory

作　　者：曾维鹏[1] 蔡莉莎[1] 吴恒玉[1] 林尔敏[1] 

机构地区：[1]海南软件职业技术学院,海南琼海571400

出　　处：《辽宁高职学报》2013年第7期73-74,83,共3页Journal of Liaoning Higher Vocational

基　　金：海南软件职业技术学院2011年度基金资助项目(Hr201105);海南软件职业技术学院2011年度基金资助项目(Hr201109);海南软件职业技术学院学院2013年度基金资助项目(Hr201301)

摘　　要：目前布尔逻辑已成为计算机科学的重要理论基础之一,是研究人类思维规律的重要工具。可满足性问题是典型的NP问题,SAT求解器的开发使得判定可满足性问题更加自动化。以与门电路为例,描述了如何将电路问题转换成可满足性SAT问题并使用MiniSAT求解器进行求解,包括输入格式、选项以及输出格式要求。Boolean logic has become one of the important theoretical bases in computer science. It is an important tool for studying human thinking in law. Satisfactory problem is typical NP problem. The development of SAT solver makes the judgment of satisfactory problem automation. Taking AND circuit as an example, this paper describes how to transform circuit problem into satisfactory SAT problem, and how to use MiniSAT solver to solve, including input format, option and output format.

关 键 词：MiniSAT求解器 可满足性 合取范式 

分 类 号：TP302[自动化与计算机技术—计算机系统结构]