由一阶逻辑公式得到命题逻辑可满足性问题实例
DOI:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

Supported by the National Science Fund for Distinguished Young Scholars of China under Grant No.60125207 (国家杰出青年科学基金)


Generating SAT Instances from First-Order Formulas
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    命题逻辑可满足性(SAT)问题是计算机科学中的一个重要问题.近年来许多学者在这方面进行了大量的研究,提出了不少有效的算法.但是,很多实际问题如果用一组一阶逻辑公式来描述,往往更为自然.当解释的论域是一个固定大小的有限集合时,一阶逻辑公式的可满足性问题可以等价地归约为SAT问题.为了利用现有的高效SAT工具,提出了一种从一阶逻辑公式生成SAT问题实例的算法,并描述了一个自动的转换工具,给出了相应的实验结果.还讨论了通过增加公式来消除同构从而减小搜索空间的一些方法.实验表明,这一算法是有效的,可以用来解决数学研究和实际应用中的许多问题.

    Abstract:

    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.

    参考文献
    相似文献
    引证文献
引用本文

黄拙,张健.由一阶逻辑公式得到命题逻辑可满足性问题实例.软件学报,2005,16(3):327-335

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2003-09-17
  • 最后修改日期:2004-01-08
  • 录用日期:
  • 在线发布日期:
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号