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 \(\mathrm {P}\ne \mathrm {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 \(\mathrm {P}\ne \mathrm {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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
We mention in passing that there are relativized worlds (aka black-box models) in which NP sets exist for which all polynomial-time heuristics are asymptotically wrong half the time [7]; heuristics basically do no better than one would do by flipping a coin to give one’s answer. Indeed, that is known to hold with probability one relative to a random oracle, i.e., it holds in all but a measure zero set of possible worlds [7]. Although many suspect that the same holds in the real world, proving that would separate \(\mathrm {NP}\) from \(\mathrm {P}\) in an extraordinarily strong way, and currently even proving that \(\mathrm {P}\) and \(\mathrm {NP}\) differ is viewed as likely being decades (or worse) away [4].
- 2.
We have not been able to find Corollary (to the Proof) 5 in the literature. Certainly, two things that on their surface might seem to be the claim we are making in Corollary (to the Proof) 5 are either trivially true or are in the literature. However, upon closer inspection they turn out to be quite different from our claim.
In particular, if one removes the word “nontrivial” from Corollary (to the Proof) 5’s statement, and one is in the model in which every satisfiable formula is considered to have the empty collection of variables as a backbone and every unsatisfiable formula is considered to have no backbones, then the thus-altered version of Corollary (to the Proof) 5 is clearly true, since if one with those changes takes A to be the set of all Boolean formulas, then the theorem degenerates to the statement that if \(\mathrm {P}\ne \mathrm {NP}\), then SAT is (NP-complete, and) not in \(\mathrm {P}\).
Also, it is stated in Kilby et al. [8] that finding a backbone of CNF formulas is NP-hard. However, though this might seem to be our result, their claim and model differ from ours in many ways, making this a quite different issue. First, their hardness refers to Turing reductions (and in contrast our paper is about many-one reductions and many-one completeness). Second, they are not even speaking of NP-Turing-hardness—much less NP-Turing-completeness—in the standard sense since their model is assuming a function reply from the oracle rather than having a set as the oracle. Third, even their notion of backbones is quite different as it (unlike the influential Williams, Gomes, and Selman 2003 paper [11] and our paper) in effect requires that the function-oracle gives back both a variable and its setting. Fourth, our claim is about nontrivial backbones.
References
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5, 394–397 (1962)
Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960)
Dilkina, B., Gomes, C., Sabharwal, A.: Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search. Ann. Math. Artif. Intell. 70(4), 399–431 (2014)
Gasarch, W.: The second P =? NP poll. SIGACT News 43(2), 53–77 (2012)
Hemaspaandra, L., Narváez, D.: The opacity of backbones. Technical report, June 2016. arXiv:1606.03634 [cs.AI], Computing Research Repository, arXiv.org/corr/. Accessed June 2017 to December 2018. Revised January 2017
Hemaspaandra, L., Narváez, D.: The opacity of backbones. In: Proceedings of the 31st AAAI Conference on Artificial Intelligence, pp. 3900–3906. AAAI Press, February 2017
Hemaspaandra, L., Zimand, M.: Strong self-reducibility precludes strong immunity. Math. Syst. Theory 29(5), 535–548 (1996)
Kilby, P., Slaney, J., Thiébaux, S., Walsh, T.: Backbones and backdoors in satisfiability. In: Proceedings of the 20th National Conference on Artificial Intelligence, pp. 1368–1373. AAAI Press (2005)
Nishimura, N., Ragde, P., Szeider, S.: Detecting backdoor sets with respect to Horn and binary clauses. In: Informal Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing, pp. 96–103, May 2004
Szeider, S.: Backdoor sets for DLL subsolvers. J. Autom. Reasoning 35(1–3), 73–88 (2005)
Willams, R., Gomes, C., Selman, B.: Backdoors to typical case complexity. In: Proceedings of the 18th International Joint Conference on Artificial Intelligence, pp. 1173–1178. Morgan Kaufmann, August 2003
Acknowledgments
We thank the SOFSEM referees for helpful comments. Work done in part while L. Hemaspaandra was visiting ETH-Zürich and U-Düsseldorf.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Hemaspaandra, L.A., Narváez, D.E. (2019). Existence Versus Exploitation: The Opacity of Backdoors and Backbones Under a Weak Assumption. In: Catania, B., Královič, R., Nawrocki, J., Pighizzini, G. (eds) SOFSEM 2019: Theory and Practice of Computer Science. SOFSEM 2019. Lecture Notes in Computer Science(), vol 11376. Springer, Cham. https://doi.org/10.1007/978-3-030-10801-4_20
Download citation
DOI: https://doi.org/10.1007/978-3-030-10801-4_20
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-10800-7
Online ISBN: 978-3-030-10801-4
eBook Packages: Computer ScienceComputer Science (R0)