Algorithms for Deriving Minimum Unsatisfiable Boolean Subformulae

ZHANG Jian-min; SHEN Sheng-yu; LI Si-kun

您当前的位置：

首页 >

文章列表页 >

Algorithms for Deriving Minimum Unsatisfiable Boolean Subformulae

更新时间：2025-07-16

- Algorithms for Deriving Minimum Unsatisfiable Boolean Subformulae
- Acta Electronica Sinica Vol. 37, Issue 5, Pages: 993-999(2009)
- 作者机构：
  
  国防科学技术大学计算机学院,湖南,长沙,410073
- 作者简介：
- 基金信息：
- DOI：
  CLC： TP391
- Published：2009
- 稿件说明：
移动端阅览
ZHANG Jian-min, SHEN Sheng-yu, LI Si-kun. Algorithms for Deriving Minimum Unsatisfiable Boolean Subformulae[J]. Acta Electronica Sinica, 2009, 37(5): 993-999.
DOI：

ZHANG Jian-min, SHEN Sheng-yu, LI Si-kun. Algorithms for Deriving Minimum Unsatisfiable Boolean Subformulae[J]. Acta Electronica Sinica, 2009, 37(5): 993-999. DOI：

摘要

解释布尔公式不可满足的原因在众多领域都具有非常重要的理论与应用价值

而最小不可满足子公式能够为公式不可满足的原因提供精确的解释

帮助自动化工具迅速定位错误

诊断问题失败的缘由.针对最小不可满足子式的求解问题

提出并证明了布尔公式最小不可满足性与极大可满足性之间的关系.基于二者的关系

提出了求解最小布尔不可满足子式的贪心遗传算法与蚁群算法

并且通过实验与当前最好的方法分支-限界算法进行了对比

结果表明:两种算法在运算效率以及单位时间内剔除的短句数上都显著优于分支-限界算法

而贪心遗传算法优于蚁群算法.

Abstract

Explaining the causes of infeasibility of Boolean formulae has practical applications in various fields.A smallest-cardinality unsatisfiable subformula can provide a succinct explanation of infeasibility

and help automatic tools to rapidly locate the errors

and determine the underlying reasons for the failure.We present the relationship between maximal satisfiability and minimum unsatisfiability.Based on the relationship

a compounded greedy genetic algorithm and an ant colony algorithm are proposed to derive a minimum unsatisfiable subformula.We report experimental results on practical benchmarks

as compared with the best known branch-and-bound algorithm.The results show that two algorithms strongly outperform the branch-and-bound algorithm

and the compounded greedy genetic algorithm outperforms the ant colony algorithm on both efficiency and size of unsatisfiable subformulae.

关键词

Keywords

references

Views

1062

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Detection of Weak Fault Signals for EMU Bearings Under Strong Noise

Solving QoS Multicast Routing Problem Based on the Combination of ant Colony Algorithm and Genetic Algorithm

A New Network Traffic Prediction Model Based on Ant Colony Algorithm in Cognitive Networks

Ant Colony Chaos Genetic Algorithm for Mapping Task Graphs to a Network on Chip

Related Author

JI Ai-min

CHEN Xi-hui

LIN Xin-hai

XU Xing

SUN Xin-wei

HUANG Jing-xiong

XIE Wei-xin

KANG Li

Related Institution

CSR Qishuyan Locomotive and Vehicle Technology Research Institute Co.， Ltd.

School of Mechanical and Electrical Engineering， Hohai University

Air Defence InstituteZhengzhouHenan 450052China

ATR Key Laboratory of National DefenseShenzhen UniversityShenzhenGuangdong 518060China

School of Electronic EngineeringGuilin Institute of Electronic TechnologyGuilinGuangxi 541004China

⁰