{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T01:52:14Z","timestamp":1768269134433,"version":"3.49.0"},"reference-count":10,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2017,6,22]],"date-time":"2017-06-22T00:00:00Z","timestamp":1498089600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-13-IS02-0001"],"award-info":[{"award-number":["ANR-13-IS02-0001"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"name":"AW Apart"},{"name":"Austrian Research Promotion Agency (FFG)","award":["845582"],"award-info":[{"award-number":["845582"]}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["ID0EZDAG346"],"award-info":[{"award-number":["ID0EZDAG346"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,12]]},"DOI":"10.1007\/s10703-017-0283-x","type":"journal-article","created":{"date-parts":[[2017,6,22]],"date-time":"2017-06-22T09:55:30Z","timestamp":1498125330000},"page":"533-544","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["NP-completeness of small conflict set generation for congruence closure"],"prefix":"10.1007","volume":"51","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3618-2251","authenticated-orcid":false,"given":"Andreas","family":"Fellner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pascal","family":"Fontaine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bruno Woltzenlogel","family":"Paleo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,6,22]]},"reference":[{"key":"283_CR1","series-title":"Frontiers in artificial intelligence and applications chapter\u00a026","first-page":"825","volume-title":"Handbook of satisfiability","author":"C Barrett","year":"2009","unstructured":"Barrett C, Sebastiani R, Seshia SA, Tinelli C (2009) Satisfiability modulo theories. In: Biere A, Heule MJH, van Maaren H, Walsh T (eds) Handbook of satisfiability, vol 185. Frontiers in artificial intelligence and applications chapter\u00a026. IOS Press, Amsterdam, pp 825\u2013885"},{"key":"283_CR2","doi-asserted-by":"crossref","unstructured":"Boudou J, Fellner A, Paleo BW (2014) Skeptik: A proof compression system. In: Demri S, Kapur D, Weidenbach C (eds) International joint conference on automated reasoning (IJCAR). Lecture notes in computer science, vol 8562. Springer, Berlin, pp 374\u2013380","DOI":"10.1007\/978-3-319-08587-6_29"},{"issue":"4","key":"283_CR3","doi-asserted-by":"crossref","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"PJ Downey","year":"1980","unstructured":"Downey PJ, Sethi R, Tarjan RE (1980) Variations on the common subexpressions problem. J ACM 27(4):758\u2013771","journal-title":"J ACM"},{"key":"283_CR4","unstructured":"Fellner A, Fontaine P, Hofferek G, Paleo BW (2015) NP-completeness of small conflict set generation for congruence closure. In: Ganesh V, Jovanovi\u0107 D (eds) International workshop on satisfiability modulo theories (SMT)"},{"key":"283_CR5","unstructured":"Fontaine P (2004) Techniques for verification of concurrent systems with invariants. PhD thesis, Institut Montefiore, Universit\u00e9 de Liege, Belgium"},{"key":"283_CR6","doi-asserted-by":"crossref","unstructured":"Fontaine P, Gribomont EP (2002) Using BDDs with combinations of theories. In: Baaz M, Voronkov A (eds) Logic for programming, artificial intelligence, and reasoning (LPAR). Lecture notes in computer science, vol 2514. Springer, Berlin, pp 190\u2013201","DOI":"10.1007\/3-540-36078-6_13"},{"issue":"2","key":"283_CR7","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson G, Oppen DC (1980) Fast decision procedures based on congruence closure. J ACM 27(2):356\u2013364","journal-title":"J ACM"},{"key":"283_CR8","unstructured":"Nieuwenhuis R, Oliveras A (2004) Union-find and congruence closure algorithms that produce proofs. In: Tinelli C, Ranise S (eds) Pragmatics of decision procedures in automated reasoning (PDPAR)"},{"key":"283_CR9","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis R, Oliveras A (2005) Proof-producing congruence closure. In: Giesl J (ed) Rewriting techniques and applications (RTA). Lecture notes in computer science, vol 3467. Springer, pp 453\u2013468","DOI":"10.1007\/978-3-540-32033-3_33"},{"issue":"4","key":"283_CR10","doi-asserted-by":"crossref","first-page":"557","DOI":"10.1016\/j.ic.2006.08.009","volume":"205","author":"R Nieuwenhuis","year":"2007","unstructured":"Nieuwenhuis R, Oliveras A (2007) Fast congruence closure and extensions. Inf Comput 205(4):557\u2013580","journal-title":"Inf Comput"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0283-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0283-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0283-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,11,27]],"date-time":"2017-11-27T12:43:11Z","timestamp":1511786591000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0283-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6,22]]},"references-count":10,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,12]]}},"alternative-id":["283"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0283-x","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,6,22]]}}}