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

DOI

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)

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  - 10.2991/amsm-16.2016.8
ID  - Wang2016/05
ER  -