CAJ | 학술논문

命题逻辑可满足性(SAT)问题是计算机科学中的一个重要问题.近年来许多学者在这方面进行了大量的研究,提出了不少有效的算法.但是,很多实际问题如果用一组一阶逻辑公式来描述,往往更为自然.当解释的论域是一个固定大小的有限集合时,一阶逻辑公式的可满足性问题可以等价地归约为SAT问题.为了利用现有的高效SAT工具,提出了一种从一阶逻辑公式生成SAT问题实例的算法,并描述了一个自动的转换工具,给出了相应的实验结果.还讨论了通过增加公式来消除同构从而减小搜索空间的一些方法.实验表明,这一算法是有效的,可以用来解决数学研究和实际应用中的许多问题.
명제라집가만족성(SAT)문제시계산궤과학중적일개중요문제.근년래허다학자재저방면진행료대량적연구,제출료불소유효적산법.단시,흔다실제문제여과용일조일계라집공식래묘술,왕왕경위자연.당해석적론역시일개고정대소적유한집합시,일계라집공식적가만족성문제가이등개지귀약위SAT문제.위료이용현유적고효SAT공구,제출료일충종일계라집공식생성SAT문제실례적산법,병묘술료일개자동적전환공구,급출료상응적실험결과.환토론료통과증가공식래소제동구종이감소수색공간적일사방법.실험표명,저일산법시유효적,가이용래해결수학연구화실제응용중적허다문제.
To solve the satisfiability (SAT) problem in propositional logic, many algorithms have been proposed in recent years. However, practical problems are often more naturally described as satisfying a set of first-order formulas. When the domain of interpretation is finite and its size is a fixed positive integer, the satisfiability problem in the first-order logic can be reduced to SAT. To facilitate the use of SAT solvers, this paper presents an algorithm for generating SAT instances from first-order clauses, and describes an automatic tool performing the transformation, together with some experimental results. Several different ways of adding formulas are also discussed to eliminate symmetries, which will reduce the search space. Experiments show that the algorithm is effective and can be used to solve many problems in mathematics and real-world applications.