{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:18:10Z","timestamp":1759033090889},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540372066"},{"type":"electronic","value":"9783540372073"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814948_10","type":"book-chapter","created":{"date-parts":[[2006,7,18]],"date-time":"2006-07-18T10:12:38Z","timestamp":1153217558000},"page":"75-89","source":"Crossref","is-referenced-by-count":9,"title":["Satisfiability Checking of Non-clausal Formulas Using General Matings"],"prefix":"10.1007","author":[{"given":"Himanshu","family":"Jain","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Constantinos","family":"Bartzis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"Edimacs format, www.satcompetition.org\/2005\/edimacs.pdf"},{"key":"10_CR2","unstructured":"Minisat sat solver, http:\/\/www.cs.chalmers.se\/cs\/research\/formalmethods\/minisat\/"},{"key":"10_CR3","unstructured":"SatMate website, http:\/\/www.cs.cmu.edu\/~modelcheck\/satmate"},{"key":"10_CR4","unstructured":"Siege (version 4) sat solver, http:\/\/www.cs.sfu.ca\/~loryan\/personal\/"},{"key":"10_CR5","unstructured":"TPS and ETPS, http:\/\/gtps.math.cmu.edu\/tps-papers.html"},{"issue":"2","key":"10_CR6","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P.B. Andrews","year":"1981","unstructured":"Andrews, P.B.: Theorem Proving via General Matings. J. ACM\u00a028(2), 193\u2013214 (1981)","journal-title":"J. ACM"},{"key":"10_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-015-9934-4","volume-title":"An Introduction to Mathematical Logic and Type Theory: to Truth through Proof","author":"P.B. Andrews","year":"2002","unstructured":"Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: to Truth through Proof, 2nd edn. Kluwer Academic Publishers, Dordrecht (2002)","edition":"2"},{"issue":"4","key":"10_CR8","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W. Bibel","year":"1981","unstructured":"Bibel, W.: On Matrices with Connections. J. ACM\u00a028(4), 633\u2013645 (1981)","journal-title":"J. ACM"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Ashar, P., Gupta, A., Zhang, L., Malik, S.: Combining Strengths of Circuit-based and CNF-based Algorithms for a High-performance SAT solver. In: DAC (2002)","DOI":"10.1145\/513918.514105"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: A Fast and Robust Sat-Solver. In: DATE (2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP - A New Search Algorithm for Satisfiability. In: ICCAD, pp. 220\u2013227 (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"10_CR12","unstructured":"McAllester, D., Selman, B., Kautz, H.: Evidence for invariants in local search. In: AAAI, Providence, Rhode Island, pp. 321\u2013326 (1997)"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11499107_39","volume-title":"Theory and Applications of Satisfiability Testing","author":"A. Meier","year":"2005","unstructured":"Meier, A., Sorge, V.: A new set of algebraic benchmark problems for sat solvers. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 459\u2013466. Springer, Heidelberg (2005)"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: DAC, June 2001, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput.\u00a02(3) (1986)","DOI":"10.1016\/S0747-7171(86)80028-1"},{"key":"10_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First Order Logic","author":"R.M. Smullyan","year":"1968","unstructured":"Smullyan, R.M.: First Order Logic. Springer, Heidelberg (1968)"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Thiffault, C., Bacchus, F., Walsh, T.: Solving Non-clausal Formulas with DPLL Search. In: SAT (2004)","DOI":"10.1007\/978-3-540-30201-8_48"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Zhang, H.: Sato: An efficient propositional prover. In: CADE-14, pp. 272\u2013275 (1997)","DOI":"10.1007\/3-540-63104-6_28"},{"key":"10_CR19","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in boolean satisfiability solver. In: ICCAD, pp. 279\u2013285 (2001)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2006"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814948_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:27:52Z","timestamp":1619508472000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814948_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540372066","9783540372073"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/11814948_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}