Local backbones

DOI10.1007/978-3-642-39071-5_28MaRDI QIDQ5326477zbMATH OpenOpenAlexFDO

Authors Ronald de Haan, Stefan Szeider, Iyad Kanj

Publication date 5 August 2013

Published in Theory and Applications of Satisfiability Testing – SAT 2013 (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1304.5479

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Classical propositional logic (03B05)

Abstract: A backbone of a propositional CNF formula is a variable whose truth value is the same in every truth assignment that satisfies the formula. The notion of backbones for CNF formulas has been studied in various contexts. In this paper, we introduce local variants of backbones, and study the computational complexity of detecting them. In particular, we consider k-backbones, which are backbones for sub-formulas consisting of at most k clauses, and iterative k-backbones, which are backbones that result after repeated instantiations of k-backbones. We determine the parameterized complexity of deciding whether a variable is a k-backbone or an iterative k-backbone for various restricted formula classes, including Horn, definite Horn, and Krom. We also present some first empirical results regarding backbones for CNF-Satisfiability (SAT). The empirical results we obtain show that a large fraction of the backbones of structured SAT instances are local, in contrast to random instances, which appear to have few local backbones.

Recommendations

• On computing backbones of propositional theories
• Algorithms for computing backbones of propositional formulae
• Publication:4488090
• Theory and Applications of Satisfiability Testing
• Towards backbone computing: a greedy-whitening based approach

Cited in

(7)

• A note on backbones in optimization and approximation
• scientific article; zbMATH DE number 1467488 (Why is no real title available?)
• On computing backbones of propositional theories
• Local branching
• The opacity of backbones
• Towards backbone computing: a greedy-whitening based approach
• Algorithms for computing backbones of propositional formulae

This page was built for publication: Local backbones

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5326477)