{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T02:01:58Z","timestamp":1760061718819},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642152733"},{"type":"electronic","value":"9783642152740"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15274-0_26","type":"book-chapter","created":{"date-parts":[[2010,9,4]],"date-time":"2010-09-04T14:17:34Z","timestamp":1283609854000},"page":"293-302","source":"Crossref","is-referenced-by-count":3,"title":["Extending Clause Learning of SAT Solvers with Boolean Gr\u00f6bner Bases"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Zengler","sequence":"first","affiliation":[]},{"given":"Wolfgang","family":"K\u00fcchlin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/11814948_16","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"I. Lynce","year":"2006","unstructured":"Lynce, I., Marques da Silva, J.P.: SAT in bioinformatics: Making the case with haplotype inference. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 136\u2013141. Springer, Heidelberg (2006)"},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-02777-2_3","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"M.L. Bonet","year":"2009","unstructured":"Bonet, M.L., John, K.S.: Efficiently calculating evolutionary tree measures using SAT. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 4\u201317. Springer, Heidelberg (2009)"},{"issue":"1","key":"26_CR3","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design\u00a019(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"key":"26_CR4","series-title":"Advances in Computers","volume-title":"Highly Dependable Software","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. In: Zelkowitz, M. (ed.) Highly Dependable Software. Advances in Computers, vol.\u00a058. Academic Press, San Diego (2003)"},{"issue":"7","key":"26_CR5","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. Communications of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"26_CR6","unstructured":"Buchberger, B.: Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. PhD thesis, Universit\u00e4t Innsbruck (1965)"},{"issue":"4","key":"26_CR7","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/1012497.1012521","volume":"10","author":"D. Kapur","year":"1985","unstructured":"Kapur, D., Narendran, P.: An equational approach to theorem proving in first-order predicate calculus. ACM SIGSOFT Notes\u00a010(4), 63\u201366 (1985)","journal-title":"ACM SIGSOFT Notes"},{"key":"26_CR8","series-title":"Frontiers in Artificial Intelligence and Applications","volume-title":"Handbook of Satisfiability","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press, Amsterdam (2009)"},{"key":"26_CR9","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/S1571-0653(04)00317-8","volume":"9","author":"A. Gelder Van","year":"2001","unstructured":"Van Gelder, A.: Combining preorder and postorder resolution in a satisfiability solver. Electronic Notes in Discrete Mathematics\u00a09, 115\u2013128 (2001)","journal-title":"Electronic Notes in Discrete Mathematics"},{"key":"26_CR10","first-page":"613","volume-title":"18th National Conference on Artificial Intelligence","author":"F. Bacchus","year":"2002","unstructured":"Bacchus, F.: Enhancing davis putnam with extended binary clause reasoning. In: 18th National Conference on Artificial Intelligence, pp. 613\u2013619. AAAI Press, Menlo Park (2002)"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"618","DOI":"10.1007\/978-3-540-71209-1_48","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Condrat","year":"2007","unstructured":"Condrat, C., Kalla, P.: A gr\u00f6bner basis approach to CNF-formulae preprocessing. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 618\u2013631. Springer, Heidelberg (2007)"},{"key":"26_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/11916277_33","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"N. Dershowitz","year":"2006","unstructured":"Dershowitz, N., Hsiang, J., Huang, G.S., Kaiss, D.: Boolean rings for intersection-based satisfiability. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 482\u2013496. Springer, Heidelberg (2006)"},{"key":"26_CR13","unstructured":"Seidl, A.M., Sturm, T.: Boolean quantification in a first-order context. In: Proceedings of the CASC 2003. Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Garching, pp. 329\u2013345 (2003)"},{"issue":"1","key":"26_CR14","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P. Beame","year":"2004","unstructured":"Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. JAIR\u00a022(1), 319\u2013351 (2004)","journal-title":"JAIR"},{"key":"26_CR15","first-page":"37","volume":"40","author":"M.H. Stone","year":"1936","unstructured":"Stone, M.H.: The theory of representations for boolean algebras. Transactions of the American Mathematical Society\u00a040, 37\u2013111 (1936)","journal-title":"Transactions of the American Mathematical Society"},{"key":"26_CR16","doi-asserted-by":"publisher","first-page":"1612","DOI":"10.1016\/j.jpaa.2008.11.043","volume":"213","author":"M. Brickenstein","year":"2009","unstructured":"Brickenstein, M., Dreyer, A., Greuel, G.M., Wedler, M.: New developments in the theory of gr\u00f6bner bases and applications to formal verification. Journal of Pure and Applied Algebra\u00a0213, 1612\u20131635 (2009)","journal-title":"Journal of Pure and Applied Algebra"},{"key":"26_CR17","unstructured":"K\u00fcchlin, W.: Canonical hardware representation using Gr\u00f6bner bases. In: Proceedings of the A3L 2005, Passau, Germany, pp. 147\u2013154 (2005)"},{"key":"26_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0913-3","volume-title":"Gr\u00f6bner Bases: A Computational Approach to Commutative Algebra","author":"T. Becker","year":"1993","unstructured":"Becker, T., Weispfenning, V.: Gr\u00f6bner Bases: A Computational Approach to Commutative Algebra. Springer, New York (1993)"},{"key":"26_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35651-8","volume-title":"Ideals, Varieties, and Algorithms","author":"D. Cox","year":"2007","unstructured":"Cox, D., Little, J., O\u2019Shea, D.: Ideals, Varieties, and Algorithms, 3rd edn. Springer, New York (2007)","edition":"3"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"issue":"2","key":"26_CR21","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/261320.261324","volume":"31","author":"A. Dolzmann","year":"1997","unstructured":"Dolzmann, A., Sturm, T.: Redlog: Computer algebra meets computer logic. ACM SIGSAM Bulletin\u00a031(2), 2\u20139 (1997)","journal-title":"ACM SIGSAM Bulletin"},{"key":"26_CR22","volume-title":"Proceedings of the ISSAC 2010","author":"T. Sturm","year":"2010","unstructured":"Sturm, T., Zengler, C.: Parametric quantified SAT solving. In: Proceedings of the ISSAC 2010. ACM, New York (2010)"}],"container-title":["Lecture Notes in Computer Science","Computer Algebra in Scientific Computing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15274-0_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,19]],"date-time":"2019-03-19T22:55:01Z","timestamp":1553036101000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15274-0_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642152733","9783642152740"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15274-0_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}