{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,5]],"date-time":"2026-01-05T19:47:57Z","timestamp":1767642477261,"version":"3.48.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032156204","type":"print"},{"value":"9783032156211","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-15621-1_3","type":"book-chapter","created":{"date-parts":[[2026,1,5]],"date-time":"2026-01-05T16:38:01Z","timestamp":1767631081000},"page":"26-37","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Small Uniquely Satisfiable Patterns"],"prefix":"10.1007","author":[{"given":"Uro\u0161","family":"\u010cibej","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,1,6]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J.: On the structure of industrial sat instances. In: Proc. 15th Int. Conf. on Principles and Practice of Constraint Programming (CP), pp. 127\u2013141 (2009)","DOI":"10.1007\/978-3-642-04244-7_13"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Biere, A., J\u00e4rvisalo, M., Kiesl, B.: Preprocessing in sat solving. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 391\u2013435. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA200992","DOI":"10.3233\/FAIA200992"},{"key":"3_CR3","unstructured":"Chang, R., Kadin, J.: On the structure of uniquely satisfiable formulas. Technical Report TR 90-1124, Cornell University, Department of Computer Science (1990), available via Stanford University Libraries"},{"issue":"3","key":"3_CR4","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1006\/jcss.1995.1028","volume":"50","author":"R Chang","year":"1995","unstructured":"Chang, R., Kadin, J., Rohatgi, P.: On unique satisfiability and the threshold behavior of randomized reductions. J. Comput. Syst. Sci. 50(3), 359\u2013373 (1995)","journal-title":"J. Comput. Syst. Sci."},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the Third Annual ACM Symposium on Theory of Computing (STOC), pp. 151\u2013158. ACM, New York (1971)","DOI":"10.1145\/800157.805047"},{"issue":"7","key":"3_CR6","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962). https:\/\/doi.org\/10.1145\/368273.368557","journal-title":"Commun. ACM"},{"key":"3_CR7","unstructured":"Ehlers, R.: Approximately propagation complete and conflict propagating constraint encodings. In: Proc. 24th Int. Conf. on Principles and Practice of Constraint Programming (CP), pp. 221\u2013238 (2018)"},{"key":"3_CR8","unstructured":"Elgabou, H.A.M.: Encoding the lexicographic ordering constraint in satisfiability modulo theories. Msc by research thesis, University of York, Department of Computer Science (2015), https:\/\/etheses.whiterose.ac.uk\/id\/eprint\/10387\/1\/Encoding%20The%20Lexicographic%20Ordering%20Constraint%20in%20Satisfiability%20Modulo%20Theories.pdf"},{"key":"3_CR9","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"MR Garey","year":"1979","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman & Co., New York (1979)"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Hagberg, A.A., Schult, D.A., Swart, P.J.: Exploring network structure, dynamics, and function using networkx. In: Varoquaux, G., Vaught, T., Millman, J. (eds.) Proceedings of the 7th Python in Science Conference, pp. 11 \u2013 15. Pasadena (2008)","DOI":"10.25080\/TCWV9851"},{"key":"3_CR11","doi-asserted-by":"publisher","unstructured":"Ignatiev, A., Morgado, A., Marques-Silva, J.: PySAT: a python toolkit for prototyping with SAT oracles. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 428\u2013437. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_26","DOI":"10.1007\/978-3-319-94144-8_26"},{"key":"3_CR12","unstructured":"Jia, H., Moore, C., Strain, D.: Generating hard satisfiable formulas by hiding solutions deceptively. arXiv preprint (2005)"},{"key":"3_CR13","unstructured":"Levin, L.A.: Universal sequential search problems. Problems Inf. Trans. 9(3) (1973)"},{"issue":"5","key":"3_CR14","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: Grasp: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"J\u00e4rvisalo, M., Biere, A.: Reconstructing solutions after blocked clause elimination. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 340\u2013345. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14186-7_30","DOI":"10.1007\/978-3-642-14186-7_30"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer, Berlin Heidelberg, Berlin, Heidelberg (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"1","key":"3_CR17","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s10472-005-0424-6","volume":"43","author":"L Simon","year":"2005","unstructured":"Simon, L., Le Berre, D., Hirsch, E.A.: The sat2002 competition. Ann. Math. Artif. Intell. 43(1), 307\u2013342 (2005)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1","key":"3_CR18","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/0304-3975(86)90135-0","volume":"47","author":"L Valiant","year":"1986","unstructured":"Valiant, L., Vazirani, V.: Np is as easy as detecting unique solutions. Theoretical Comput. Sci. 47(1), 85\u201393 (1986). https:\/\/doi.org\/10.1016\/0304-3975(86)90135-0","journal-title":"Theoretical Comput. Sci."},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Algorithms on Trees and Graphs. TCS, Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81885-2","DOI":"10.1007\/978-3-030-81885-2"}],"container-title":["Lecture Notes in Computer Science","Applied Algorithms"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-15621-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,5]],"date-time":"2026-01-05T16:38:04Z","timestamp":1767631084000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-15621-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032156204","9783032156211"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-15621-1_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"6 January 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICAA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Applied Algorithms","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kolkata","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"India","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 January 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 January 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icaa2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icaa2026.framer.website\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}