{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T02:11:15Z","timestamp":1742955075705,"version":"3.40.3"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031433689"},{"type":"electronic","value":"9783031433696"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T00:00:00Z","timestamp":1694563200000},"content-version":"vor","delay-in-days":255,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>KBO constraint solving is very well-known to be an NP-complete problem. Motivated by the needs of the family of SCL calculi, we consider the particular case where all terms occurring in a constraint are bound by a (single) ground term. We show that this problem and variants of this problem remain NP-complete even if the form of atoms in the constraint is further restricted. In addition, for a non-strict, partial term ordering solely based on symbol counting constraint solving remains NP-complete. Nevertheless, we provide a new simple algorithm testing KBO constraint solvability that performs well on benchmark examples.<\/jats:p>","DOI":"10.1007\/978-3-031-43369-6_5","type":"book-chapter","created":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T14:32:18Z","timestamp":1694701938000},"page":"81-98","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["KBO Constraint Solving Revisited"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-9917-7517","authenticated-orcid":false,"given":"Yasmine","family":"Briefs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2634-4154","authenticated-orcid":false,"given":"Hendrik","family":"Leidinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6002-0458","authenticated-orcid":false,"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,13]]},"reference":[{"key":"5_CR1","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). https:\/\/www.smt-lib.org\/"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-030-67067-2_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Bromberger","year":"2021","unstructured":"Bromberger, M., Fiori, A., Weidenbach, C.: Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) VMCAI 2021. LNCS, vol. 12597, pp. 511\u2013533. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_23"},{"key":"5_CR3","unstructured":"Bromberger, M., Gehl, T., Leutgeb, L., Weidenbach, C.: A two-watched literal scheme for first-order logic. In: Konev, B., Schon, C., Steen, A. (eds.) Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC\/IJCAR 2022), Haifa, Israel, 11\u201312 August 2022. CEUR Workshop Proceedings, vol. 3201. CEUR-WS.org (2022)"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Bromberger, M., Schwarz, S., Weidenbach, C.: Exploring partial models with SCL. In: Piskac, R., Voronkov, A. (eds.) Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol. 94, pp. 48\u201372. EasyChair (2023). https:\/\/doi.org\/10.29007\/8br1","DOI":"10.29007\/8br1"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Bromberger, M., Schwarz, S., Weidenbach, C.: SCL(FOL) revisited (2023). https:\/\/doi.org\/10.48550\/ARXIV.2302.05954. https:\/\/arxiv.org\/abs\/2302.05954","DOI":"10.48550\/ARXIV.2302.05954"},{"issue":"4","key":"5_CR6","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"PJ Downey","year":"1980","unstructured":"Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. J. ACM 27(4), 758\u2013771 (1980)","journal-title":"J. ACM"},{"key":"5_CR7","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. Mathematical Sciences Series. Freeman, New York (1979)"},{"issue":"1","key":"5_CR8","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1093\/jigpal\/9.1.53","volume":"9","author":"J Hurd","year":"2001","unstructured":"Hurd, J.: Congruence classes with logic variables. Log. J. IGPL 9(1), 53\u201369 (2001)","journal-title":"Log. J. IGPL"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, I. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Korovin, K., Voronkov, A.: A decision procedure for the existential theory of term algebras with the Knuth-Bendix ordering. In: Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No. 99CB36332), pp. 291\u2013302. IEEE (2000)","DOI":"10.1109\/LICS.2000.855777"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"979","DOI":"10.1007\/3-540-48224-5_79","volume-title":"Automata, Languages and Programming","author":"K Korovin","year":"2001","unstructured":"Korovin, K., Voronkov, A.: Knuth-Bendix constraint solving is NP-complete. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 979\u2013992. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-48224-5_79"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Korovin, K., Voronkov, A.: Orienting rewrite rules with the Knuth-Bendix order, vol. 183, pp. 165\u2013186. Elsevier (2003)","DOI":"10.1016\/S0890-5401(03)00021-X"},{"key":"5_CR13","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-031-10769-6_14","volume-title":"Automated Reasoning","author":"H Leidinger","year":"2022","unstructured":"Leidinger, H., Weidenbach, C.: SCL(EQ): SCL for first-order logic with equality. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) IJCAR 2022. LNCS, vol. 13385, pp. 228\u2013247. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_14"},{"key":"5_CR14","unstructured":"L\u00f6chner, B.: Advances in Equational Theorem Proving-Architecture, Algorithms, and Redundancy Avoidance. Dissertation, Fachbereich Informatik, TU Kaiserslautern (2005)"},{"issue":"2","key":"5_CR15","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356\u2013364 (1980)","journal-title":"J. ACM"},{"issue":"1","key":"5_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"RE Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding combinations of theories. J. ACM 31(1), 1\u201312 (1984)","journal-title":"J. ACM"},{"issue":"2","key":"5_CR17","first-page":"99","volume":"37","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe, G.: The CADE ATP system competition - CASC. AI Mag. 37(2), 99\u2013101 (2016)","journal-title":"AI Mag."}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-43369-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T02:20:17Z","timestamp":1730082017000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-43369-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031433689","9783031433696"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-43369-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"13 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 September 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 September 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/frocos2023.github.io\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}