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

摘要

目前布尔逻辑已成为计算机科学的重要理论基础之一，是研究人类思维规律的重要工具。可满足性问题是典型的N P问题，SA T 求解器的开发使得判定可满足性问题更加自动化。以与门电路为例，描述了如何将电路问题转换成可满足性SA T 问题并使用M iniSA T 求解器进行求解，包括输入格式、选项以及输出格式要求。%B oolean logic has becom e one of the im portant theoretical bases in com puter science. It is an im portant tool for studying hum an thinking in law . Satisfactory problem is typical N P problem . The developm ent of SA T solver m akes the judgm ent of satisfactory problem autom ation. Taking A N D circuit as an exam ple, this paper describes how to transform circuit problem into satisfactory SA T problem , and how to use M iniSA T solver to solve, including input form at, option and output form at.