Published on Wed Jun 14 2017

Existence versus Exploitation: The Opacity of Backbones and Backdoors Under a Weak Assumption

Lane A. Hemaspaandra, David E. Narváez

Backdoors and backbones of Boolean formulas are hidden structural properties. solver algorithms seek to substantially better performance by exploiting these structures. The present paper is not intended to improve the performance of SAT solvers, but rather is a cautionary paper.

0
0
0
Abstract

Backdoors and backbones of Boolean formulas are hidden structural properties. A natural goal, already in part realized, is that solver algorithms seek to obtain substantially better performance by exploiting these structures. However, the present paper is not intended to improve the performance of SAT solvers, but rather is a cautionary paper. In particular, the theme of this paper is that there is a potential chasm between the existence of such structures in the Boolean formula and being able to effectively exploit them. This does not mean that these structures are not useful to solvers. It does mean that one must be very careful not to assume that it is computationally easy to go from the existence of a structure to being able to get one's hands on it and/or being able to exploit the structure. For example, in this paper we show that, under the assumption that P NP, there are easily recognizable families of Boolean formulas with strong backdoors that are easy to find, yet for which it is hard (in fact, NP-complete) to determine whether the formulas are satisfiable. We also show that, also under the assumption P NP, there are easily recognizable sets of Boolean formulas for which it is hard (in fact, NP-complete) to determine whether they have a large backbone.

Sat Jun 11 2016
Artificial Intelligence
The Opacity of Backbones
This paper approaches, using structural complexity theory, the question of whether there is a chasm between knowing an object exists and getting one's hands on the object or its properties. We show that, under the widely believed assumption that integer factoring is hard, there exist sets of formulas that have
0
0
0
Fri Oct 28 2011
Artificial Intelligence
Backdoors to Acyclic SAT
Backdoor sets are certain key variables of a CNF formula F that make it easy to solve the formula. By assigning truth values to the variables in a backdoor set, the formula gets reduced to one or several solvable formulas. We study the problem of finding backdoor sets of size at most k with respect to the base class of CNF formulas with acyclic incidence graphs.
0
0
0
Fri Oct 28 2011
Artificial Intelligence
Backdoors to Satisfaction
A backdoor set is a set of variables of a propositional formula such that fixing the truth values of the variables in the backdoor set moves the formula into a decidable class. If we know a small backdoor set we can reduce the question of whether the given formula is satisfiable to the
0
0
0
Thu Jan 05 2017
Artificial Intelligence
Understanding the complexity of #SAT using knowledge compilation
Two main techniques have been used so far to solve the #P-hard problem #SAT. We show that every beta-acyclic formula can be represented by a polynomial size circuit corresponding to the first method.
0
0
0
Fri Apr 27 2012
Artificial Intelligence
Strong Backdoors to Bounded Treewidth SAT
For SAT and its counting version #SAT, hidden structure has been exploited in terms of decomposability and strong backdoor sets. Decomposability can be considered as the treewidth of a graph associated with the given CNF formula. A strong backdoor set is a set of variables such that each possible partial assignment to this set moves the formula into a fixed class.
0
0
0
Tue May 22 2018
Artificial Intelligence
QBF as an Alternative to Courcelle's Theorem
We propose reductions to quantified Boolean formulas (QBF) as a new approach to showing fixed-parameter linear algorithms. We demonstrate the feasibility of this approach by giving new new algorithms for several well-known problems from artificial intelligence.
0
0
0