Skip to main content
Erschienen in: Progress in Artificial Intelligence 3/2021

13.03.2021 | Regular Paper

Existence versus exploitation: the opacity of backdoors and backbones

verfasst von: Lane A. Hemaspaandra, David E. Narváez

Erschienen in: Progress in Artificial Intelligence | Ausgabe 3/2021

Einloggen

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Boolean formulas often have what are known as hidden structures. We study the complexity of whether such structures (of certain sizes) exist in a formula, the complexity of getting one’s hands on the structure’s information, and whether even when in hand the information can be efficiently exploited. In particular, backdoors and backbones of Boolean formulas are important hidden structural properties. A natural goal, already in part realized, is that solver algorithms seek 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 tale. 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 information to being able to get one’s hands on it and/or being able to exploit it. We construct backdoor- and backbone-based cases where, if \(\mathrm {P}\ne \mathrm {NP}\), such assumptions fail. For example, if \(\mathrm {P}\ne \mathrm {NP}\), then (a) there are easily recognizable families of Boolean formulas with strong backdoors that are easy to find, yet for which it is hard to determine whether the formulas are satisfiable, and (b) there are easily recognizable sets of Boolean formulas for which it is hard to determine whether they have a large backbone.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Fußnoten
1
Recall that if F is unsatisfiable, then “A determines F” means, perhaps somewhat confusingly as regards the plain English meaning of “determines,” that A proclaims F’s unsatisfiability.
 
2
Here we assume that a clause \(\{x\}\) precedes a clause \(\{y\}\) in lexicographical order if x precedes y in lexicographical order.
 
3
We have not been able to find Corollary (to the Proof) 4.2 in the literature. Certainly, two things that on their surface might seem to be the claim we are making in Corollary (to the Proof) 4.2 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) 4.2’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) 4.2 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. [25] 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 [37] 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.
 
Literatur
1.
Zurück zum Zitat Ansótegui, C., Bonet, M., Giráldez-Cru, J., Levy, J., Simon, L.: Community structures in industrial SAT instances. J. Artif. Intell. Res. 66, 443–472 (2019)MathSciNetCrossRef Ansótegui, C., Bonet, M., Giráldez-Cru, J., Levy, J., Simon, L.: Community structures in industrial SAT instances. J. Artif. Intell. Res. 66, 443–472 (2019)MathSciNetCrossRef
2.
Zurück zum Zitat Bellare, M., Goldwasser, S.: The complexity of decision versus search. SIAM J. Comput. 23(1), 97–119 (1994)MathSciNetCrossRef Bellare, M., Goldwasser, S.: The complexity of decision versus search. SIAM J. Comput. 23(1), 97–119 (1994)MathSciNetCrossRef
3.
Zurück zum Zitat Berman, P.: Relationship between density and deterministic complexity of NP-complete languages. In: Proceedings of the 5th International Colloquium on Automata, Languages, and Programming. Lecture Notes in Computer Science, July 1978, vol. 62, pp. 63–71. Springer (1978) Berman, P.: Relationship between density and deterministic complexity of NP-complete languages. In: Proceedings of the 5th International Colloquium on Automata, Languages, and Programming. Lecture Notes in Computer Science, July 1978, vol. 62, pp. 63–71. Springer (1978)
4.
Zurück zum Zitat Borodin, A., Demers, A.: Some comments on functional self-reducibility and the NP hierarchy. Technical Report TR 76-284, Department of Computer Science, Cornell University, Ithaca, NY, July (1976) Borodin, A., Demers, A.: Some comments on functional self-reducibility and the NP hierarchy. Technical Report TR 76-284, Department of Computer Science, Cornell University, Ithaca, NY, July (1976)
5.
Zurück zum Zitat Buhrman, H., Hitchcock, J.: NP-hard sets are exponentially dense unless coNP\(\,\subseteq \,\)NP/poly. In: Proceedings of the 23rd Annual IEEE Conference on Computational Complexity, June 2008, pp. 1–7. IEEE Computer Society Press (2008) Buhrman, H., Hitchcock, J.: NP-hard sets are exponentially dense unless coNP\(\,\subseteq \,\)NP/poly. In: Proceedings of the 23rd Annual IEEE Conference on Computational Complexity, June 2008, pp. 1–7. IEEE Computer Society Press (2008)
6.
Zurück zum Zitat Cai, J., Chakaravarthy, V., Hemaspaandra, L., Ogihara, M.: Competing provers yield improved Karp–Lipton collapse results. Inf. Comput. 198(1), 1–23 (2005)MathSciNetCrossRef Cai, J., Chakaravarthy, V., Hemaspaandra, L., Ogihara, M.: Competing provers yield improved Karp–Lipton collapse results. Inf. Comput. 198(1), 1–23 (2005)MathSciNetCrossRef
7.
Zurück zum Zitat Chen, W., Whitley, D.: Decomposing SAT instances with pseudo backbones. In: Proceedings of the 17th European Conference on Evolutionary Computation in Combinatorial Optimization. Lecture Notes in Computer Science, March 2017, vol. 10197, pp. 75–90. Springer (2017) Chen, W., Whitley, D.: Decomposing SAT instances with pseudo backbones. In: Proceedings of the 17th European Conference on Evolutionary Computation in Combinatorial Optimization. Lecture Notes in Computer Science, March 2017, vol. 10197, pp. 75–90. Springer (2017)
8.
Zurück zum Zitat Cook, S.: The complexity of theorem-proving procedures. In: Proceedings of the 3rd ACM Symposium on Theory of Computing, May 1971, pp. 151–158. ACM Press (1971) Cook, S.: The complexity of theorem-proving procedures. In: Proceedings of the 3rd ACM Symposium on Theory of Computing, May 1971, pp. 151–158. ACM Press (1971)
9.
Zurück zum Zitat Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 7, 394–397 (1962)MathSciNetCrossRef Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 7, 394–397 (1962)MathSciNetCrossRef
10.
11.
Zurück zum Zitat 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)MathSciNetCrossRef 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)MathSciNetCrossRef
12.
Zurück zum Zitat Dowling, W., Gallier, J.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Log. Program. 1(3), 267–284 (1984) Dowling, W., Gallier, J.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Log. Program. 1(3), 267–284 (1984)
13.
Zurück zum Zitat Friedrich, T., Krohmer, A., Rothenberger, R., Sutton, A.: Phase transitions for scale-free SAT formulas. In: Proceedings of the 31st AAAI Conference on Artificial Intelligence, February 2017, pp. 3893–3899. AAAI Press (2017) Friedrich, T., Krohmer, A., Rothenberger, R., Sutton, A.: Phase transitions for scale-free SAT formulas. In: Proceedings of the 31st AAAI Conference on Artificial Intelligence, February 2017, pp. 3893–3899. AAAI Press (2017)
15.
Zurück zum Zitat Gaspers, S., Misra, N., Ordyniak, S., Szeider, S., Živný, S.: Backdoors into heterogeneous classes of SAT and CSP. J. Comput. Syst. Sci. 85, 38–56 (2017) Gaspers, S., Misra, N., Ordyniak, S., Szeider, S., Živný, S.: Backdoors into heterogeneous classes of SAT and CSP.  J. Comput. Syst. Sci. 85, 38–56 (2017)
16.
Zurück zum Zitat Hartmanis, J., Hemachandra, L.: Complexity classes without machines: on complete languages for UP. Theor. Comput. Sci. 58(1–3), 129–142 (1988)MathSciNetCrossRef Hartmanis, J., Hemachandra, L.: Complexity classes without machines: on complete languages for UP. Theor. Comput. Sci. 58(1–3), 129–142 (1988)MathSciNetCrossRef
17.
Zurück zum Zitat Hemaspaandra, E., Hemaspaandra, L., Menton, C.: Search versus decision for election manipulation problems. ACM Trans. Comput. 12, 1–42 (2020)MATH Hemaspaandra, E., Hemaspaandra, L., Menton, C.: Search versus decision for election manipulation problems. ACM Trans. Comput. 12, 1–42 (2020)MATH
18.
Zurück zum Zitat Hemaspaandra, L.: Computational social choice and computational complexity: BFFs? In: Proceedings of the 32nd AAAI Conference on Artificial Intelligence, February 2018, pp. 7971–7977. AAAI Press (2018) Hemaspaandra, L.: Computational social choice and computational complexity: BFFs? In: Proceedings of the 32nd AAAI Conference on Artificial Intelligence, February 2018, pp. 7971–7977. AAAI Press (2018)
19.
Zurück zum Zitat Hemaspaandra, L., Narváez, D.: The opacity of backbones. Technical Report, Computing Research Repository, June 2016. Revised, January (2017). arXiv:1606.03634 Hemaspaandra, L., Narváez, D.: The opacity of backbones. Technical Report, Computing Research Repository, June 2016. Revised, January (2017). arXiv:​1606.​03634
20.
Zurück zum Zitat Hemaspaandra, L., Narváez, D.: The opacity of backbones. In: Proceedings of the 31st AAAI Conference on Artificial Intelligence, February 2017, pp. 3900–3906. AAAI Press (2017) Hemaspaandra, L., Narváez, D.: The opacity of backbones. In: Proceedings of the 31st AAAI Conference on Artificial Intelligence, February 2017, pp. 3900–3906. AAAI Press (2017)
21.
Zurück zum Zitat Hemaspaandra, L., Narváez, D.: Existence versus exploitation: the opacity of backbones and backdoors under a weak assumption. In: Proceedings of the 45th International Conference on Current Trends in Theory and Practice of Computer Science. Lecture Notes in Computer Science, January 2019, vol. 11376, pp. 247–259. Springer (2019) Hemaspaandra, L., Narváez, D.: Existence versus exploitation: the opacity of backbones and backdoors under a weak assumption. In: Proceedings of the 45th International Conference on Current Trends in Theory and Practice of Computer Science. Lecture Notes in Computer Science, January 2019, vol. 11376, pp. 247–259. Springer (2019)
22.
Zurück zum Zitat Hemaspaandra, L., Ogihara, M.: The Complexity Theory Companion. Springer, Berlin (2002)CrossRef Hemaspaandra, L., Ogihara, M.: The Complexity Theory Companion. Springer, Berlin (2002)CrossRef
23.
Zurück zum Zitat Hemaspaandra, L., Williams, R.: An atypical survey of typical-case heuristic algorithms. SIGACT News 43(4), 71–89 (2012)CrossRef Hemaspaandra, L., Williams, R.: An atypical survey of typical-case heuristic algorithms. SIGACT News 43(4), 71–89 (2012)CrossRef
24.
Zurück zum Zitat Hemaspaandra, L., Zimand, M.: Strong self-reducibility precludes strong immunity. Math. Syst. Theory 29(5), 535–548 (1996)MathSciNetCrossRef Hemaspaandra, L., Zimand, M.: Strong self-reducibility precludes strong immunity. Math. Syst. Theory 29(5), 535–548 (1996)MathSciNetCrossRef
25.
Zurück zum Zitat Kilby, P., Slaney, J., Thiébaux, S., Walsh, T.: Backbones and backdoors in satisfiability. In: Proceedings of the 20th National Conference on Artificial Intelligence, July 2005, pp. 1368–1373. AAAI Press (2005) Kilby, P., Slaney, J., Thiébaux, S., Walsh, T.: Backbones and backdoors in satisfiability. In: Proceedings of the 20th National Conference on Artificial Intelligence, July 2005, pp. 1368–1373. AAAI Press (2005)
26.
Zurück zum Zitat Kochemazov, S., Zaikin, O.: ALIAS: A modular tool for finding backdoors for SAT. In: Proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing. Lecture Notes in Computer Science, June 2018, vol. 10929, pp. 419–427. Springer (2018) Kochemazov, S., Zaikin, O.: ALIAS: A modular tool for finding backdoors for SAT. In: Proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing. Lecture Notes in Computer Science, June 2018, vol. 10929, pp. 419–427. Springer (2018)
27.
Zurück zum Zitat Mahaney, S.: Sparse complete sets for NP: solution of a conjecture of Berman and Hartmanis. J. Comput. Syst. Sci. 25(2), 130–143 (1982)MathSciNetCrossRef Mahaney, S.: Sparse complete sets for NP: solution of a conjecture of Berman and Hartmanis. J. Comput. Syst. Sci. 25(2), 130–143 (1982)MathSciNetCrossRef
28.
Zurück zum Zitat 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, May 2004, pp. 96–103 (2004) 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, May 2004, pp. 96–103 (2004)
29.
Zurück zum Zitat Papadimitriou, C.: Computational Complexity. Addison-Wesley, Boston (1994)MATH Papadimitriou, C.: Computational Complexity. Addison-Wesley, Boston (1994)MATH
30.
Zurück zum Zitat Rothe, J.: Complexity of certificates, heuristics, and counting types, with applications to cryptography and circuit theory. Habilitation thesis, Friedrich-Schiller-Universität Jena, Institut für Informatik, Jena, Germany, June (1999) Rothe, J.: Complexity of certificates, heuristics, and counting types, with applications to cryptography and circuit theory. Habilitation thesis, Friedrich-Schiller-Universität Jena, Institut für Informatik, Jena, Germany, June (1999)
31.
Zurück zum Zitat Schaefer, T.: The complexity of satisfiability problems. In: Proceedings of the 10th ACM Symposium on Theory of Computing, May 1978, pp. 216–226. ACM Press (1978) Schaefer, T.: The complexity of satisfiability problems. In: Proceedings of the 10th ACM Symposium on Theory of Computing, May 1978, pp. 216–226. ACM Press (1978)
32.
33.
Zurück zum Zitat Semenov, A., Zaikin, O., Otpuschennikov, I., Kochemazov, S., Ignatiev, A.: On cryptographic attacks using backdoors for SAT. In: Proceedings of the 32nd AAAI Conference on Artificial Intelligence, February 2018, pp. 6641–6648. AAAI Press (2018) Semenov, A., Zaikin, O., Otpuschennikov, I., Kochemazov, S., Ignatiev, A.: On cryptographic attacks using backdoors for SAT. In: Proceedings of the 32nd AAAI Conference on Artificial Intelligence, February 2018, pp. 6641–6648. AAAI Press (2018)
34.
35.
Zurück zum Zitat Tardos, G.: Query complexity, or why is it difficult to separate NP\({\rm }^{A}{}\cap \,\)coNP\({\rm }^{A}\) from P\({\rm {{}}}^{A}\) by random oracles \({A}\). Combinatorica 9, 385–392 (1989)MathSciNetCrossRef Tardos, G.: Query complexity, or why is it difficult to separate NP\({\rm }^{A}{}\cap \,\)coNP\({\rm }^{A}\) from P\({\rm {{}}}^{A}\) by random oracles \({A}\). Combinatorica 9, 385–392 (1989)MathSciNetCrossRef
36.
37.
Zurück zum Zitat Willams, R., Gomes, C., Selman, B.: Backdoors to typical case complexity. In: Proceedings of the 18th International Joint Conference on Artificial Intelligence, August 2003, pp. 1173–1178. Morgan Kaufmann (2003) Willams, R., Gomes, C., Selman, B.: Backdoors to typical case complexity. In: Proceedings of the 18th International Joint Conference on Artificial Intelligence, August 2003, pp. 1173–1178. Morgan Kaufmann (2003)
Metadaten
Titel
Existence versus exploitation: the opacity of backdoors and backbones
verfasst von
Lane A. Hemaspaandra
David E. Narváez
Publikationsdatum
13.03.2021
Verlag
Springer Berlin Heidelberg
Erschienen in
Progress in Artificial Intelligence / Ausgabe 3/2021
Print ISSN: 2192-6352
Elektronische ISSN: 2192-6360
DOI
https://doi.org/10.1007/s13748-021-00234-6

Weitere Artikel der Ausgabe 3/2021

Progress in Artificial Intelligence 3/2021 Zur Ausgabe