{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,23]],"date-time":"2026-10-23T11:59:11Z","timestamp":1792756751682,"version":"4.5.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642314230","type":"print"},{"value":"9783642314247","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31424-7_31","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T14:26:49Z","timestamp":1340288809000},"page":"410-426","source":"Crossref","is-referenced-by-count":17,"title":["When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way"],"prefix":"10.1007","author":[{"given":"Cheng-Shen","family":"Han","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jie-Hong Roland","family":"Jiang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"31_CR1","unstructured":"Altera Advanced Synthesis Cookbook, http:\/\/www.altera.com\/literature\/manual\/stx_cookbook.pdf"},{"key":"31_CR2","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press (2009)"},{"key":"31_CR3","unstructured":"Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification, http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/"},{"key":"31_CR4","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Massacci, F.: The taming of the (X)OR. In: Proc. Int\u2019l Conf. on Computational Logic, pp. 508\u2013522 (2000)","DOI":"10.1007\/3-540-44957-4_34"},{"issue":"1","key":"31_CR5","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/1838552.1838559","volume":"12","author":"A. Cimatti","year":"2010","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans. on Computational Logic\u00a012(1), 7 (2010)","journal-title":"ACM Trans. on Computational Logic"},{"key":"31_CR6","unstructured":"Chen, J.-C.: XORSAT: An efficient algorithm for the DIMACS 32-bit parity problem, CoRR abs\/cs\/0703006 (2007)"},{"key":"31_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-642-02777-2_29","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"J.-C. Chen","year":"2009","unstructured":"Chen, J.-C.: Building a Hybrid SAT Solver via Conflict-Driven, Look-Ahead and XOR Reasoning Techniques. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 298\u2013311. Springer, Heidelberg (2009)"},{"issue":"3","key":"31_CR8","doi-asserted-by":"publisher","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Linear reasoning: A new form of the Herbrand-Gentzen theorem. J. Symbolic Logic\u00a022(3), 250\u2013268 (1957)","journal-title":"J. Symbolic Logic"},{"key":"31_CR9","unstructured":"Dantzig, G.: Maximization of linear function of variables subject to linear inequalities. Activity Analysis of Production and Allocation, 339\u2013347 (1951)"},{"key":"31_CR10","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)"},{"key":"31_CR11","unstructured":"Gomes, C., Sabharwal, A., Selman, B.: Model counting: A new strategy for obtaining good bounds. In: Proc. National Conf. on Artificial Intelligence (AAAI), pp. 54\u201361 (2006)"},{"issue":"1-4","key":"31_CR12","doi-asserted-by":"crossref","first-page":"27","DOI":"10.3233\/SAT190015","volume":"2","author":"H. Haanpaa","year":"2006","unstructured":"Haanpaa, H., Jarvisalo, M., Kaski, P., Niemela, I.: Hard satisfiable clause sets for benchmarking equivalence reasoning techniques. Journal on Satisfiability, Boolean Modeling and Computation\u00a02(1-4), 27\u201346 (2006)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"issue":"4","key":"31_CR13","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1109\/TC.2010.12","volume":"59","author":"J.-H.R. Jiang","year":"2010","unstructured":"Jiang, J.-H.R., Lee, C.-C., Mishchenko, A., Huang, C.-Y.: To SAT or not to SAT: Scalable exploration of functional dependency. IEEE Trans. on Computers\u00a059(4), 457\u2013467 (2010)","journal-title":"IEEE Trans. on Computers"},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"Liu, H.-Y., Chou, Y.-C., Lin, C.-H., Jiang, J.-H.R.: Towards Completely Automatic Decoder Synthesis. In: Proc. Int\u2019l Conf. on Computer Aided Design (ICCAD), pp. 389\u2013395 (2011)","DOI":"10.1109\/ICCAD.2011.6105359"},{"key":"31_CR15","unstructured":"Li, C.M.: Integrating equivalency reasoning into Davis-Putnam procedure. In: Proc. National Conf. on Artificial Intelligence (AAAI), pp. 291\u2013296 (2000)"},{"key":"31_CR16","doi-asserted-by":"crossref","unstructured":"Laitinen, T., Junttila, T., Niemela, I.: Extending clause learning DPLL with parity reasoning. In: Proc. European Conference on Artificial Intelligence (ECAI), pp. 21\u201326 (2010)","DOI":"10.3233\/978-1-60750-606-5-21"},{"key":"31_CR17","doi-asserted-by":"crossref","unstructured":"Laitinen, T., Junttila, T., Niemela, I.: Equivalence class based parity reasoning with DPLL(XOR). In: Proc. Int\u2019l Conf. on Tools with Artificial Intelligence (ICTAI), pp. 649\u2013658 (2011)","DOI":"10.1109\/ICTAI.2011.103"},{"key":"31_CR18","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R., Een, N.: Improvements to combinational equivalence checking. In: Proc. Int\u2019l Conf. on Computer-Aided Design (ICCAD), pp. 836\u2013843 (2006)","DOI":"10.1109\/ICCAD.2006.320087"},{"key":"31_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-Based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"issue":"1","key":"31_CR20","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"K.L. McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theoretical Computer Science\u00a0345(1), 101\u2013121 (2005)","journal-title":"Theoretical Computer Science"},{"issue":"1-2","key":"31_CR21","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1023\/A:1006326723002","volume":"24","author":"F. Massacci","year":"2000","unstructured":"Massacci, F., Marraro, L.: Logical cryptanalysis as a SAT-problem: Encoding and analysis. Journal of Automated Reasoning\u00a024(1-2), 165\u2013203 (2000)","journal-title":"Journal of Automated Reasoning"},{"key":"31_CR22","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proc. Design Automation Conf. (DAC), pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"issue":"5","key":"31_CR23","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J., Sakallah, K.: GRASP: A search algorithm for propositional satisfiability. IEEE Trans. on Computeres\u00a048(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. on Computeres"},{"issue":"6","key":"31_CR24","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM\u00a053(6), 937\u2013977 (2006)","journal-title":"Journal of the ACM"},{"key":"31_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-02777-2_24","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"M. Soos","year":"2009","unstructured":"Soos, M., Nohl, K., Castelluccia, C.: Extending SAT Solvers to Cryptographic Problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 244\u2013257. Springer, Heidelberg (2009)"},{"key":"31_CR26","unstructured":"Soos, M.: Enhanced Gaussian elimination in DPLL-based SAT solvers. In: Proc. Pragmatics of SAT (2010)"},{"issue":"3-5","key":"31_CR27","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/S0167-6377(98)00052-2","volume":"23","author":"J. Warners","year":"1998","unstructured":"Warners, J., van Maaren, H.: A two-phase algorithm for solving a class of hard satisfiability problems. Operations Research Letters\u00a023(3-5), 81\u201388 (1998)","journal-title":"Operations Research Letters"},{"key":"31_CR28","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/11532231_26","volume-title":"Automated Deduction \u2013 CADE-20","author":"G. Yorsh","year":"2005","unstructured":"Yorsh, G., Musuvathi, M.: A Combination Method for Generating Interpolants. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 353\u2013368. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31424-7_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T09:31:41Z","timestamp":1743586301000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31424-7_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314230","9783642314247"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31424-7_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}