{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:17:02Z","timestamp":1760203022865,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030802226"},{"type":"electronic","value":"9783030802233"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-80223-3_30","type":"book-chapter","created":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T14:13:49Z","timestamp":1625148829000},"page":"436-452","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Fast Algorithm for SAT in Terms of Formula Length"],"prefix":"10.1007","author":[{"given":"Junqiang","family":"Peng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1012-2373","authenticated-orcid":false,"given":"Mingyu","family":"Xiao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,2]]},"reference":[{"key":"30_CR1","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)"},{"key":"30_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-642-03367-4_13","volume-title":"Algorithms and Data Structures","author":"J Chen","year":"2009","unstructured":"Chen, J., Liu, Y.: An improved SAT algorithm in terms of formula length. In: Dehne, F., Gavrilova, M., Sack, J.-R., T\u00f3th, C.D. (eds.) WADS 2009. LNCS, vol. 5664, pp. 144\u2013155. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03367-4_13"},{"key":"30_CR3","unstructured":"Chu, H., Xiao, M., Zhang, Z.: An improved upper bound for SAT. Proc. AAAI Conf. Artif. Intell. 35(5), 3707\u20133714 (2021). https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/view\/16487"},{"key":"30_CR4","doi-asserted-by":"publisher","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Harrison, M.A., Banerji, R.B., Ullman, J.D. (eds.) Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, Shaker Heights, Ohio, USA, 3\u20135 May 1971, pp. 151\u2013158. ACM (1971). https:\/\/doi.org\/10.1145\/800157.805047","DOI":"10.1145\/800157.805047"},{"key":"30_CR5","doi-asserted-by":"publisher","unstructured":"Cook, S.A., Mitchell, D.G.: Finding hard instances of the satisfiability problem: a survey. In: Du, D., Gu, J., Pardalos, P.M. (eds.) Satisfiability Problem: Theory and Applications, Proceedings of a DIMACS Workshop, Piscataway, New Jersey, USA, 11\u201313 March 1996. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 35, pp. 1\u201317. DIMACS\/AMS (1996). https:\/\/doi.org\/10.1090\/dimacs\/035\/01","DOI":"10.1090\/dimacs\/035\/01"},{"issue":"3","key":"30_CR6","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960). https:\/\/doi.org\/10.1145\/321033.321034","journal-title":"J. ACM"},{"key":"30_CR7","doi-asserted-by":"publisher","unstructured":"Fomin, F.V., Grandoni, F., Kratsch, D.: A measure & conquer approach for the analysis of exact algorithms. J. ACM 56(5), 25:1\u201325:32 (2009). https:\/\/doi.org\/10.1145\/1552285.1552286","DOI":"10.1145\/1552285.1552286"},{"key":"30_CR8","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16533-7","volume-title":"Exact Exponential Algorithms","author":"FV Fomin","year":"2010","unstructured":"Fomin, F.V., Kratsch, D.: Exact Exponential Algorithms. TTCSAES. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16533-7"},{"key":"30_CR9","unstructured":"Hirsch, E.A.: Two new upper bounds for SAT. In: Karloff, H.J. (ed.) Proceedings of the Ninth Annual ACM-SIAM Symposium on Discrete Algorithms, San Francisco, California, USA, 25\u201327 January 1998, pp. 521\u2013530. ACM\/SIAM (1998). http:\/\/dl.acm.org\/citation.cfm?id=314613.314838"},{"issue":"4","key":"30_CR10","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1023\/A:1006340920104","volume":"24","author":"EA Hirsch","year":"2000","unstructured":"Hirsch, E.A.: New worst-case upper bounds for SAT. J. Autom. Reason. 24(4), 397\u2013420 (2000). https:\/\/doi.org\/10.1023\/A:1006340920104","journal-title":"J. Autom. Reason."},{"issue":"2","key":"30_CR11","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1006\/jcss.2000.1727","volume":"62","author":"R Impagliazzo","year":"2001","unstructured":"Impagliazzo, R., Paturi, R.: On the complexity of k-sat. J. Comput. Syst. Sci. 62(2), 367\u2013375 (2001). https:\/\/doi.org\/10.1006\/jcss.2000.1727","journal-title":"J. Comput. Syst. Sci."},{"key":"30_CR12","unstructured":"Kullmann, O., Luckhardt, H.: Deciding propositional tautologies: Algorithms and their complexity. preprint 82 (1997)"},{"key":"30_CR13","doi-asserted-by":"publisher","unstructured":"Liu, S.: Chain, generalization of covering code, and deterministic algorithm for k-sat. In: Chatzigiannakis, I., Kaklamanis, C., Marx, D., Sannella, D. (eds.) 45th International Colloquium on Automata, Languages, and Programming, ICALP 2018, Prague, Czech Republic, 9\u201313 July 2018. LIPIcs, vol. 107, pp. 88:1\u201388:13. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2018). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2018.88","DOI":"10.4230\/LIPIcs.ICALP.2018.88"},{"key":"30_CR14","first-page":"419","volume":"43","author":"B Monien","year":"1981","unstructured":"Monien, B., Speckenmeyer, E., Vornberger, O.: Upper bounds for covering problems. Methods Oper. Res. 43, 419\u2013431 (1981)","journal-title":"Methods Oper. Res."},{"key":"30_CR15","unstructured":"Peng, J., Xiao, M.: A fast algorithm for SAT in terms of formula length (2021). https:\/\/arxiv.org\/abs\/2105.06131"},{"issue":"1","key":"30_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(88)90014-4","volume":"79","author":"A Van Gelder","year":"1988","unstructured":"Van Gelder, A.: A satisfiability tester for non-clausal propositional calculus. Inf. Comput. 79(1), 1\u201321 (1988). https:\/\/doi.org\/10.1016\/0890-5401(88)90014-4","journal-title":"Inf. Comput."},{"key":"30_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/11561071_12","volume-title":"Algorithms \u2013 ESA 2005","author":"M Wahlstr\u00f6m","year":"2005","unstructured":"Wahlstr\u00f6m, M.: An algorithm for the SAT problem for formulae of linear length. In: Brodal, G.S., Leonardi, S. (eds.) ESA 2005. LNCS, vol. 3669, pp. 107\u2013118. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11561071_12"},{"key":"30_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/11499107_23","volume-title":"Theory and Applications of Satisfiability Testing","author":"M Wahlstr\u00f6m","year":"2005","unstructured":"Wahlstr\u00f6m, M.: Faster exact solving of SAT formulae with a low number of occurrences per variable. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 309\u2013323. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11499107_23"},{"key":"30_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1007\/11602613_65","volume-title":"Algorithms and Computation","author":"M Yamamoto","year":"2005","unstructured":"Yamamoto, M.: An improved $$\\tilde{\\cal{O}}(1.234^{m})$$-time deterministic algorithm for SAT. In: Deng, X., Du, D.-Z. (eds.) ISAAC 2005. LNCS, vol. 3827, pp. 644\u2013653. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11602613_65"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2021"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-80223-3_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T23:36:48Z","timestamp":1625182608000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-80223-3_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030802226","9783030802233"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-80223-3_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"2 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Satisfiability Testing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Barcelona","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.iiia.csic.es\/sat2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}