{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:48:27Z","timestamp":1773654507845,"version":"3.50.1"},"reference-count":10,"publisher":"Allerton Press","issue":"1","license":[{"start":{"date-parts":[[2010,2,1]],"date-time":"2010-02-01T00:00:00Z","timestamp":1264982400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2010,2,1]],"date-time":"2010-02-01T00:00:00Z","timestamp":1264982400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Aut. Conrol Comp. Sci."],"published-print":{"date-parts":[[2010,2]]},"DOI":"10.3103\/s0146411610010013","type":"journal-article","created":{"date-parts":[[2010,3,22]],"date-time":"2010-03-22T08:23:09Z","timestamp":1269246189000},"page":"1-10","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Formal verification with functional indeterminacy on the basis of satisfiability testing of the conjunctive normal form"],"prefix":"10.3103","volume":"44","author":[{"given":"L. D.","family":"Cheremisinova","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D. Ya.","family":"Novikov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1627","published-online":{"date-parts":[[2010,3,23]]},"reference":[{"key":"6064_CR1","volume-title":"Advanced Formal Verification","year":"2005","unstructured":"Advanced Formal Verification, Drechsler, R., Ed., Netherlands: Kluwer Academic, 2005."},{"key":"6064_CR2","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1007\/978-1-4615-0817-5_13","volume-title":"Logic Synthesis and Verification","author":"A. Kuehlmann","year":"2002","unstructured":"Kuehlmann, A. and van Eijk, C.A.J., Combinational and Sequential Equivalence Checking, Logic Synthesis and Verification, Hassoun, S., Sasao, T., and Brayton, R.K., Eds., Netherlands: Kluwer Academic, 2002, pp. 343\u2013372."},{"key":"6064_CR3","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/978-1-4615-0817-5_12","volume-title":"Logic Synthesis and Verification","author":"W. Kunz","year":"2002","unstructured":"Kunz, W., Marques-Silva, J., and Malik, S., SAT and ATPG: Algorithms for Boolean Decision Problems, Logic Synthesis and Verification, Hassoun, S., Sasao, T., and Brayton, R.K., Eds., Netherlands: Kluwer Academic, 2002, pp. 309\u2013341."},{"key":"6064_CR4","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Zhang, L., Ashar, P., Gupta, A., and Malik, S., Combining Strengths of Circuit-Based and CNF-Based Algorithms for a High-Performance SAT Solver, Proc. ACM\/IEEE Design Automation Conf., 2002, pp. 747\u2013750.","DOI":"10.1109\/DAC.2002.1012722"},{"key":"6064_CR5","doi-asserted-by":"crossref","unstructured":"Goldberg, E. and Novikov, Y., BerkMin: A Fast and Robust SAT-Solver, Proc. European Design and Test Conf., 2002, pp. 142\u2013149.","DOI":"10.1109\/DATE.2002.998262"},{"key":"6064_CR6","doi-asserted-by":"crossref","unstructured":"Een, N. and Sorensson, N., An Extensible SAT-Solver, Theory and Applications of Satisfiability Testing, 2004, pp. 502\u2013518.","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"6064_CR7","unstructured":"The MiniSat Page: http:\/\/minisat.se\/MiniSat.html"},{"key":"6064_CR8","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R., and Een, N., Improvements to Combinational Equivalence Checking, Proc. ICCAD\u201906, pp. San Jose, CA, 2006, pp. 836\u2013843.","DOI":"10.1145\/1233501.1233679"},{"key":"6064_CR9","unstructured":"Novikov, Ya. and Brinkmann, R., Foundations of Hierarchical SAT-Solving, ZIB-Report 05-38, 2005, http:\/\/www.zib.de\/Publications\/Reports\/ZR-05-38.pdf"},{"key":"6064_CR10","unstructured":"Cheremisinova, L. and Novikov, D., SAT-Based Approach to Verification of Logical Descriptions with Functional Indeterminacy, 8th International Workshop on Boolean Problems, Freiberg, 2008, pp. 59\u201366."}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411610010013.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411610010013","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411610010013","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411610010013.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:07:31Z","timestamp":1773612451000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411610010013"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,2]]},"references-count":10,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,2]]}},"alternative-id":["6064"],"URL":"https:\/\/doi.org\/10.3103\/s0146411610010013","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,2]]},"assertion":[{"value":"27 October 2009","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 March 2010","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}