主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2019年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
黄拙,张健.由一阶逻辑公式得到命题逻辑可满足性问题实例.软件学报,2005,16(3):327-335
由一阶逻辑公式得到命题逻辑可满足性问题实例
Generating SAT Instances from First-Order Formulas
投稿时间:2003-09-17  修订日期:2004-01-08
DOI:
中文关键词:  可满足性问题  一阶逻辑  命题逻辑
英文关键词:satisfiability problem  first-order logic  propositional logic
基金项目:Supported by the National Science Fund for Distinguished Young Scholars of China under Grant No.60125207 (国家杰出青年科学基金)
作者单位
黄拙 中国科学院,软件研究所,计算机科学重点实验室,北京,100080
中国科学院,研究生院,北京,100039 
张健 中国科学院,软件研究所,计算机科学重点实验室,北京,100080 
摘要点击次数: 4151
全文下载次数: 3450
中文摘要:
      命题逻辑可满足性(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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利