CAJ | 학술논문

目前布尔逻辑已成为计算机科学的重要理论基础之一，是研究人类思维规律的重要工具。可满足性问题是典型的N P问题，SA T 求解器的开发使得判定可满足性问题更加自动化。以与门电路为例，描述了如何将电路问题转换成可满足性SA T 问题并使用M iniSA T 求解器进行求解，包括输入格式、选项以及输出格式要求。
목전포이라집이성위계산궤과학적중요이론기출지일，시연구인류사유규률적중요공구。가만족성문제시전형적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.