Nội dung được dịch bởi AI, chỉ mang tính chất tham khảo
Sự tồn tại so với sự khai thác: tính mờ đục của các cấu trúc backdoor và backbone
Tóm tắt
Các công thức Boolean thường có những cấu trúc ẩn. Chúng tôi nghiên cứu độ phức tạp của việc liệu những cấu trúc như vậy (có kích thước nhất định) có tồn tại trong một công thức hay không, độ phức tạp của việc tiếp cận thông tin về cấu trúc đó, và liệu ngay cả khi đã nắm được thông tin, việc khai thác chúng có thể thực hiện một cách hiệu quả hay không. Cụ thể, các backdoor và backbone của các công thức Boolean là những thuộc tính cấu trúc ẩn quan trọng. Một mục tiêu tự nhiên, đã phần nào được nhận thức, là các thuật toán giải quyết tìm kiếm hiệu suất tốt hơn bằng cách khai thác các cấu trúc này. Tuy nhiên, bài báo hiện tại không nhằm cải thiện hiệu suất của các bộ giải SAT mà thực chất là một lời cảnh tỉnh. Chủ đề của bài báo này là có thể có một khoảng cách tiềm tàng giữa sự tồn tại của những cấu trúc như vậy trong công thức Boolean và khả năng khai thác hiệu quả chúng. Điều này không có nghĩa là những cấu trúc này không hữu ích cho các bộ giải; mà có nghĩa là cần rất cẩn thận để không giả định rằng việc đi từ sự tồn tại của thông tin đến khả năng tiếp cận nó và/hoặc khai thác nó là dễ dàng tính toán. Chúng tôi xây dựng các trường hợp dựa trên backdoor và backbone nơi mà, nếu $$\mathrm {P}\ne \mathrm {NP}$$, những giả định như vậy sẽ thất bại. Ví dụ, nếu $$\mathrm {P}\ne \mathrm {NP}$$, thì (a) có những họ công thức Boolean dễ nhận biết với các backdoor mạnh mà dễ tìm, nhưng rất khó để xác định xem các công thức đó có thể thỏa mãn hay không, và (b) có những tập hợp công thức Boolean dễ nhận biết mà khó để xác định xem chúng có một backbone lớn hay không.
Từ khóa
#công thức Boolean #backdoor #backbone #độ phức tạp #giải thuật SATTài liệu tham khảo
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)
Bellare, M., Goldwasser, S.: The complexity of decision versus search. SIAM J. Comput. 23(1), 97–119 (1994)
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)
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)
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)
Cai, J., Chakaravarthy, V., Hemaspaandra, L., Ogihara, M.: Competing provers yield improved Karp–Lipton collapse results. Inf. Comput. 198(1), 1–23 (2005)
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)
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)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 7, 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)
Dowling, W., Gallier, J.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Log. Program. 1(3), 267–284 (1984)
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)
Gasarch, W.: The third P =? NP poll. SIGACT News 50(1), 38–59 (2019)
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)
Hartmanis, J., Hemachandra, L.: Complexity classes without machines: on complete languages for UP. Theor. Comput. Sci. 58(1–3), 129–142 (1988)
Hemaspaandra, E., Hemaspaandra, L., Menton, C.: Search versus decision for election manipulation problems. ACM Trans. Comput. 12, 1–42 (2020)
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., 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. In: Proceedings of the 31st AAAI Conference on Artificial Intelligence, February 2017, pp. 3900–3906. AAAI Press (2017)
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., Ogihara, M.: The Complexity Theory Companion. Springer, Berlin (2002)
Hemaspaandra, L., Williams, R.: An atypical survey of typical-case heuristic algorithms. SIGACT News 43(4), 71–89 (2012)
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, July 2005, pp. 1368–1373. AAAI Press (2005)
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)
Mahaney, S.: Sparse complete sets for NP: solution of a conjecture of Berman and Hartmanis. J. Comput. Syst. Sci. 25(2), 130–143 (1982)
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)
Papadimitriou, C.: Computational Complexity. Addison-Wesley, Boston (1994)
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)
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)
Schöning, U.: Complete sets and closeness to complexity classes. Math. Syst. Theory 19(1), 29–42 (1986)
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)
Szeider, S.: Backdoor sets for DLL subsolvers. J. Autom. Reason. 35(1–3), 73–88 (2005)
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)
Valiant, L.: The relative complexity of checking and evaluating. Inf. Process. Lett. 5(1), 20–23 (1976)
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)