| MiniSAT求解器在判定可满足性问题中的应用 |
| |
| 引用本文： | 曾维鹏,蔡莉莎,吴恒玉,林尔敏.MiniSAT求解器在判定可满足性问题中的应用[J].辽宁高职学报,2013(7):73-74,83. |
| |
| 作者姓名： | 曾维鹏 蔡莉莎 吴恒玉 林尔敏 |
| |
| 作者单位： | 海南软件职业技术学院,海南琼海571400 |
| |
| 基金项目： | 海南软件职业技术学院2011年度基金资助项目（Hr201105）;海南软件职业技术学院学院2013年度基金资助项目（Hr201301）;海南软件职业技术学院2011年度基金资助项目（Hr201109） |
| |
| 摘 要： | 目前布尔逻辑已成为计算机科学的重要理论基础之一，是研究人类思维规律的重要工具。可满足性问题是典型的NP问题，SAT求解器的开发使得判定可满足性问题更加自动化。以与门电路为例．描述了如何将电路问题转换成可满足性SAT问题并使用MiniSAT求解器进行求解，包括输入格式、选项以及输出格式要求。
|
| 关 键 词： | MiniSAT求解器 可满足性 合取范式 |
Application of MiniSAT Slover for Judging Satisfactory |
| |
| ZENG Wei-peng,CAI Li-sha,WU Heng-yu,LIN Er-min.Application of MiniSAT Slover for Judging Satisfactory[J].Liaoning Higher Vocational Technical Institute Journal,2013(7):73-74,83. |
| |
| Authors: | ZENG Wei-peng CAI Li-sha WU Heng-yu LIN Er-min |
| |
| Institution: | (Hainan College of Soaware Technology, Qionghai 571400, China) |
| |
| Abstract: | 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. |
| |
| Keywords: | MiniSAT solver satisfactory conjunctive normal form |
| 本文献已被 维普 等数据库收录！ |
