{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:12:25Z","timestamp":1748664745535,"version":"3.41.0"},"reference-count":7,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2015,10,14]],"date-time":"2015-10-14T00:00:00Z","timestamp":1444780800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["K\u00fcnstl Intell"],"published-print":{"date-parts":[[2016,10]]},"DOI":"10.1007\/s13218-015-0406-8","type":"journal-article","created":{"date-parts":[[2015,10,14]],"date-time":"2015-10-14T14:31:40Z","timestamp":1444833100000},"page":"339-342","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Towards Next Generation Sequential and Parallel SAT Solvers"],"prefix":"10.1007","volume":"30","author":[{"given":"Norbert","family":"Manthey","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,10,14]]},"reference":[{"key":"406_CR1","unstructured":"Biere A, Heule MJH, van Maaren H, Walsh T (eds) Handbook of satisfiability, Frontiers in artificial intelligence and applications, vol 185. IOS Press (2009)"},{"key":"406_CR2","doi-asserted-by":"crossref","unstructured":"H\u00f6lldobler S, Manthey N, Philipp T, Steinke P (2014) Generic CDCL\u2014A formalization of modern propositional satisfiability solvers. In: Berre DL (ed) POS-14, EPiC Series, vol 27, pp 89\u2013102. EasyChair","DOI":"10.29007\/7n71"},{"key":"406_CR3","doi-asserted-by":"publisher","unstructured":"Manthey N (2012) Coprocessor 2.0\u2014A flexible CNF simplifier. In: Cimatti A, Sebastiani R (eds) Theory and Applications of Satisfiability Testing\u2014SAT 2012, Lecture Notes in Computer Science, vol 7317, pp 436\u2013441. Springer Berlin Heidelberg (2012). doi: 10.1007\/978-3-642-31612-8_34","DOI":"10.1007\/978-3-642-31612-8_34"},{"key":"406_CR4","unstructured":"Manthey N (2014) Towards next generation sequential and parallel SAT solvers. Ph.D. thesis, Technische Universit\u00e4t Dresden. http:\/\/nbn-resolving.de\/urn:nbn:de:bsz:14-qucosa-158672"},{"key":"406_CR5","doi-asserted-by":"publisher","unstructured":"Manthey N, Heule MJH, Biere A (2013) Automated reencoding of Boolean formulas. In: Biere A, Nahir A, Vos T (eds) Hardware and software: verification and testing, Lecture Notes in Computer Science, vol 7857, pp 102\u2013117. Springer Berlin Heidelberg (2013). doi: 10.1007\/978-3-642-39611-3_14","DOI":"10.1007\/978-3-642-39611-3_14"},{"key":"406_CR6","doi-asserted-by":"publisher","unstructured":"Manthey N, Philipp T, Wernhard C (2013) Soundness of inprocessing in clause sharing SAT solvers. In: J\u00e4rvisalo M, Van Gelder A (eds) Theory and applications of satisfiability testing\u2014SAT 2013, Lecture Notes in Computer Science, vol 7962, pp 22\u201339. Springer Berlin Heidelberg. doi: 10.1007\/978-3-642-39071-5_4","DOI":"10.1007\/978-3-642-39071-5_4"},{"key":"406_CR7","doi-asserted-by":"publisher","unstructured":"Wernhard C (2013) Computing with logic as operator elimination: The ToyElim system. In: Tompits H, Abreu S, Oetsch J, P\u00fchrer J, Seipel D, Umeda M, Wolf A (eds) Applications of declarative programming and knowledge management, Lecture Notes in Computer Science, vol 7773, pp 289\u2013296. Springer Berlin Heidelberg (2013). doi: 10.1007\/978-3-642-41524-1_17","DOI":"10.1007\/978-3-642-41524-1_17"}],"container-title":["KI - K\u00fcnstliche Intelligenz"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s13218-015-0406-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s13218-015-0406-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s13218-015-0406-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s13218-015-0406-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T01:15:26Z","timestamp":1748654126000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s13218-015-0406-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,10,14]]},"references-count":7,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2016,10]]}},"alternative-id":["406"],"URL":"https:\/\/doi.org\/10.1007\/s13218-015-0406-8","relation":{},"ISSN":["0933-1875","1610-1987"],"issn-type":[{"type":"print","value":"0933-1875"},{"type":"electronic","value":"1610-1987"}],"subject":[],"published":{"date-parts":[[2015,10,14]]}}}