Proceedings of the 2016 International Conference on Applied Mathematics, Simulation and Modelling

Algorithm for Computing Backbones of Propositional Formulae Based on Solved Backbone Information

Authors
Zipeng Wang, Yiping Bao, Junhao Xing, Xinyu Chen, Sihan Liu
Corresponding Author
Zipeng Wang
Available Online May 2016.
DOI
https://doi.org/10.2991/amsm-16.2016.8How to use a DOI?
Keywords
propositional satisfiability; backbone
Abstract

The problem of propositional satisfiability (SAT) has found a number of applications in both theoretical and practical computer science. However, in many applications, knowing a formulae's satisfiability alone is not enough to solve problems. Often, some other characteristics of formulae need to be known. In 1997, the definition of backbone occur - a set of variables which are true in any assignment of SAT, which starts the research of solution structure. Gradually, backbone has been recognized having great effect in rapidly solving intelligent planning and automated reasoning problems. First of all, this article reviews three existing algorithms for computing backbone, finding that no algorithm uses solved backbone as information. Based on this idea, we bring up a new algorithm for computing backbone of propositional formulae using solved backbone information. This article utilizes latest SAT competition data on original fastest algorithm (one test per time of 30 chuck) and the new algorithm. According to the experiment results, the new algorithm can have 10% advance on rate at the set of data which contain 80% or more chuck so it has practical application value.

Copyright
© 2016, the Authors. Published by Atlantis Press.
Open Access
This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

Volume Title
Proceedings of the 2016 International Conference on Applied Mathematics, Simulation and Modelling
Series
Advances in Computer Science Research
Publication Date
May 2016
ISBN
978-94-6252-198-8
ISSN
2352-538X
DOI
https://doi.org/10.2991/amsm-16.2016.8How to use a DOI?
Copyright
© 2016, the Authors. Published by Atlantis Press.
Open Access
This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Cite this article

TY  - CONF
AU  - Zipeng Wang
AU  - Yiping Bao
AU  - Junhao Xing
AU  - Xinyu Chen
AU  - Sihan Liu
PY  - 2016/05
DA  - 2016/05
TI  - Algorithm for Computing Backbones of Propositional Formulae Based on Solved Backbone Information
BT  - Proceedings of the 2016 International Conference on Applied Mathematics, Simulation and Modelling
PB  - Atlantis Press
SP  - 32
EP  - 35
SN  - 2352-538X
UR  - https://doi.org/10.2991/amsm-16.2016.8
DO  - https://doi.org/10.2991/amsm-16.2016.8
ID  - Wang2016/05
ER  -