{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:27:39Z","timestamp":1750307259010,"version":"3.41.0"},"reference-count":2,"publisher":"Association for Computing Machinery (ACM)","issue":"1\/2","license":[{"start":{"date-parts":[[2011,7,25]],"date-time":"2011-07-25T00:00:00Z","timestamp":1311552000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Commun. Comput. Algebra"],"published-print":{"date-parts":[[2011,7,25]]},"abstract":"<jats:p>We want to incorporate the reasoning power of Boolean Gr\u00f6bner bases into modern SAT solvers. There are many starting points where to plug in the Gr\u00f6bner bases engine in the SAT solving process. As a first step we chose the learning part where new consequences (lemmas) of the original formula are deduced. This paper shows first promising results, also published at the CASC 2010 in Armenia [1].<\/jats:p>","DOI":"10.1145\/2016567.2016596","type":"journal-article","created":{"date-parts":[[2011,8,10]],"date-time":"2011-08-10T16:16:22Z","timestamp":1312992982000},"page":"141-142","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Boolean Gr\u00f6bner bases in SAT solving"],"prefix":"10.1145","volume":"45","author":[{"given":"Christoph","family":"Zengler","sequence":"first","affiliation":[{"name":"University of T\u00fcbingen, T\u00fcbingen, Germany"}]},{"given":"Wolfgang","family":"K\u00fcchlin","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, T\u00fcbingen, Germany"}]}],"member":"320","published-online":{"date-parts":[[2011,7,25]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1893832.1893858"},{"key":"e_1_2_1_2_1","series-title":"Frontiers in Artificial Intelligence and Applications","volume-title":"Handbook of Satisfiability","author":"Biere A.","year":"2009","unstructured":"Biere , A. , Heule , M. , van Maaren , H. , Walsh , T. , eds.: Handbook of Satisfiability . Volume 185 of Frontiers in Artificial Intelligence and Applications . IOS Press ( 2009 ). Biere, A., Heule, M., van Maaren, H., Walsh, T., eds.: Handbook of Satisfiability. Volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press (2009)."}],"container-title":["ACM Communications in Computer Algebra"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2016567.2016596","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2016567.2016596","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:52:32Z","timestamp":1750243952000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2016567.2016596"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7,25]]},"references-count":2,"journal-issue":{"issue":"1\/2","published-print":{"date-parts":[[2011,7,25]]}},"alternative-id":["10.1145\/2016567.2016596"],"URL":"https:\/\/doi.org\/10.1145\/2016567.2016596","relation":{},"ISSN":["1932-2240"],"issn-type":[{"type":"print","value":"1932-2240"}],"subject":[],"published":{"date-parts":[[2011,7,25]]},"assertion":[{"value":"2011-07-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}