{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T15:21:40Z","timestamp":1759332100913},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2002,12,18]],"date-time":"2002-12-18T00:00:00Z","timestamp":1040169600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2003,11]]},"DOI":"10.1007\/s10009-002-0102-5","type":"journal-article","created":{"date-parts":[[2004,3,20]],"date-time":"2004-03-20T15:40:18Z","timestamp":1079797218000},"page":"4-14","source":"Crossref","is-referenced-by-count":4,"title":["Satisfiability checking using Boolean Expression Diagrams"],"prefix":"10.1007","volume":"5","author":[{"given":"Poul F.","family":"Williams","sequence":"first","affiliation":[]},{"given":"Henrik R.","family":"Andersen","sequence":"additional","affiliation":[]},{"given":"Henrik","family":"Hulgaard","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,12,18]]},"reference":[{"key":"102_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Bjesse, P., E\u00e9n, N.: Symbolic reachability analysis based on SAT solvers. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2000","DOI":"10.1007\/3-540-46419-0_28"},{"key":"102_CR2","doi-asserted-by":"crossref","unstructured":"Andersen, H.R., Hulgaard, H.: Boolean expression diagrams. Information and Computation. (To appear)","DOI":"10.1109\/LICS.1997.614938"},{"key":"102_CR3","doi-asserted-by":"crossref","unstructured":"Andersen, H.R., Hulgaard, H.: Boolean expression diagrams. In: IEEE Symposium on Logic in Computer Science (LICS), July 1997","DOI":"10.1109\/LICS.1997.614938"},{"key":"102_CR4","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proc. ACM\/IEEE Design Automation Conference (DAC), 1999","DOI":"10.1109\/DAC.1999.781333"},{"key":"102_CR5","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 1579. Springer-Verlag, 1999","DOI":"10.1007\/3-540-49059-0_14"},{"key":"102_CR6","doi-asserted-by":"crossref","unstructured":"Biere, A., Clarke, E., Raimi, R., Zhu, Y.: Verifying safety properties of a PowerPC microprocessor using symbolic model checking without BDDs. In Computer Aided Verification (CAV), Lecture Notes in Computer Science, vol. 1633. Springer-Verlag, 1999","DOI":"10.1007\/3-540-48683-6_8"},{"key":"102_CR7","doi-asserted-by":"crossref","unstructured":"Bjesse, P.: SAT-based verification without state space traversal. In: Proc. Formal Methods in Computer-Aided Design, Third International Conference, FMCAD\u201900, Austin, Texas, USA, Lecture Notes in Computer Science, November 2000","DOI":"10.1007\/3-540-40922-X_23"},{"key":"102_CR8","unstructured":"Brglez, F., Fujiware, H.: A neutral netlist of 10 combinational benchmarks circuits and a target translator in Fortran. In: Special Session International Symposium on Circuits and Systems (ISCAS), 1985"},{"key":"102_CR9","first-page":"677","volume":"35","author":"Bryant,","year":"8","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers 35(8): 677\u2013691, August 1986","journal-title":"IEEE Transactions on Computers"},{"key":"102_CR10","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Binary decision diagrams and beyond: Enabling technologies for formal verification. In: Proc. International Conf. Computer-Aided Design (ICCAD), November 1995, pp. 236\u2013243","DOI":"10.1109\/ICCAD.1995.480018"},{"key":"102_CR11","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"Davis,","year":"7","unstructured":"Davis, M., Longemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the ACM 5(7): 394\u2013397, July 1962","journal-title":"Communications of the ACM"},{"key":"102_CR12","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"Davis,","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7: 201\u2013215, 1960","journal-title":"Journal of the ACM"},{"key":"102_CR13","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Sebastiani, R.: Applying the Davis-Putnam procedure to non-clausal formulas. In: Proc. Italian National Conference on Artificial Intelligence, volume 1792 of Lecture Notes in Computer Science, Bologna, Italy. Springer-Verlag, September 1999","DOI":"10.1007\/3-540-46238-4_8"},{"key":"102_CR14","unstructured":"Holger Hoos, H., Thomas St\u00fctzle. SATLIB \u2013 the satisfiability library. http:\/\/www.satlib.org"},{"key":"102_CR15","doi-asserted-by":"crossref","unstructured":"Hulgaard, H., Williams, P.F., Andersen, H.R.: Equivalence checking of combinational circuits using boolean expression diagrams. IEEE Transactions on Computer Aided Design, July 1999","DOI":"10.1109\/43.771175"},{"key":"102_CR16","doi-asserted-by":"crossref","first-page":"1143","DOI":"10.1109\/43.310903","volume":"13","author":"Kunz,","year":"9","unstructured":"Kunz, W., Pradhan, D.K.: Recursive learning: A new implication technique for efficient solutions to CAD problems \u2013 test, verification, optimization. IEEE Transactions on Computer Aided Design 13(9): 1143\u20131158, September 1994","journal-title":"IEEE Transactions on Computer Aided Design"},{"key":"102_CR17","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"Marques-Silva,","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers 48: 506\u2013521, 1999","journal-title":"IEEE Transactions on Computers"},{"key":"102_CR18","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. of the 39th Design Automation Conference, Las Vegas, June 2001","DOI":"10.1145\/378239.379017"},{"key":"102_CR19","doi-asserted-by":"crossref","unstructured":"Mukherjee, R., Jain, J., Takayama, K., Fujita, M., Abraham, J.A., Fussell, D.S.: An Efficient Filter-Based Approach for Combinational Verification. In: Proc. of the Design, Automation and Test in Europe Conference and Exhibition, 1999","DOI":"10.1109\/DATE.1999.761108"},{"key":"102_CR20","doi-asserted-by":"crossref","unstructured":"Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proc. International Conf. Computer-Aided Design (ICCAD), 1993, pp. 42\u201347","DOI":"10.1109\/ICCAD.1993.580029"},{"key":"102_CR21","doi-asserted-by":"crossref","unstructured":"Sebastiani, R.: Applying GSAT to non-clausal formulas. Journal of Artificial Intelligence Research (JAIR), 1: 309\u2013314, January 1994","DOI":"10.1613\/jair.49"},{"key":"102_CR22","unstructured":"Selman, B., Levesque, H.J., Mitchell, D.: A new method for solving hard satisfiability problems. In: Rosenbloom, P., Szolovits, P. (eds.) Proc. Tenth National Conference on Artificial Intelligence, Menlo Park, California. American Association for Artificial Intelligence, AAAI Press, 1992, pp. 440\u2013446"},{"key":"102_CR23","doi-asserted-by":"crossref","unstructured":"Sheeran, M., St\u00e5lmarck, G.: A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic. In: Gopalakrishnan, G., Windley, P.J. (eds.) Proc. Formal Methods in Computer-Aided Design, Second International Conference, FMCAD\u201998, Palo Alto\/CA, USA, Lecture Notes in Computer Science, vol. 1522. November 1998, pp. 82\u201399","DOI":"10.1007\/3-540-49519-3_7"},{"key":"102_CR24","doi-asserted-by":"crossref","unstructured":"van Eijk, C.A.J.: Sequential equivalence checking without state space traversal. In: Proc. International Conf. on Design Automation and Test of Electronic-based Systems (DATE), 1998","DOI":"10.1109\/DATE.1998.655922"},{"key":"102_CR25","unstructured":"Williams, P.F.: Formal Verification Based on Boolean Expression Diagrams. PhD thesis, Dept. of Information Technology, Technical University of Denmark, Lyngby, Denmark, August 2000. ISBN 87-89112-59-8"},{"key":"102_CR26","doi-asserted-by":"crossref","unstructured":"Williams, P.F., Biere, A., Clarke, E.M., Gupta, A.: Combining decision diagrams and SAT procedures for efficient symbolic model checking. In: Computer Aided Verification (CAV), Lecture Notes in Computer Science, vol. 1855. Chicago, U.S.A.. Springer-Verlag, July 2000, pp. 124\u2013138","DOI":"10.1007\/10722167_13"},{"key":"102_CR27","doi-asserted-by":"crossref","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: William McCune, editor, Proceedings of the 14th International Conference on Automated deduction, Lecture Notes in Artificial Intelligence, vol. 1249. Berlin, Springer-Verlag, July 1997, pp. 272\u2013275","DOI":"10.1007\/3-540-63104-6_28"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-002-0102-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-002-0102-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-002-0102-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,31]],"date-time":"2020-03-31T18:11:21Z","timestamp":1585678281000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-002-0102-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,12,18]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,11]]}},"alternative-id":["102"],"URL":"https:\/\/doi.org\/10.1007\/s10009-002-0102-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,12,18]]}}}