{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:56:47Z","timestamp":1773615407443,"version":"3.50.1"},"reference-count":12,"publisher":"Allerton Press","issue":"4","license":[{"start":{"date-parts":[[2011,8,1]],"date-time":"2011-08-01T00:00:00Z","timestamp":1312156800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2011,8,1]],"date-time":"2011-08-01T00:00:00Z","timestamp":1312156800000},"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":[[2011,8]]},"DOI":"10.3103\/s0146411611040055","type":"journal-article","created":{"date-parts":[[2011,9,6]],"date-time":"2011-09-06T14:34:30Z","timestamp":1315319670000},"page":"206-217","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Analysis of the implementability of descriptions with functional indeterminacy based on the verification of conjunctive normal form satisfiability"],"prefix":"10.3103","volume":"45","author":[{"given":"D. Ya.","family":"Novikov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"L. D.","family":"Cheremisinova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1627","published-online":{"date-parts":[[2011,9,6]]},"reference":[{"key":"6145_CR1","doi-asserted-by":"crossref","unstructured":"Drechsler, R., et al., Advanced Formal Verification, Kluwer, 2005.","DOI":"10.1007\/b105236"},{"key":"6145_CR2","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A. and van Eijk Cornelis, A.J., Combinational and Sequential Equivalence Checking, in Logic Synthesis and Verification, Hassoun, S., Sasao, T., and Brayton, R.K., Eds., Kluwer, 2002, pp. 343\u2013372.","DOI":"10.1007\/978-1-4615-0817-5_13"},{"key":"6145_CR3","doi-asserted-by":"crossref","unstructured":"Kunz, W., Marques-Silva, J., and Malik, S., SAT and ATPG: Algorithms for Boolean Decision Problems, in Logic Synthesis and Verification, Hassoun, S., Sasao, T., and Brayton, R.K., Eds., Kluwer, 2002, pp. 309\u2013341.","DOI":"10.1007\/978-1-4615-0817-5_12"},{"key":"6145_CR4","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R., and Een, N., Improvements to Combinational Equivalence Checking, Proc. ICCAD\u201906, San Jose, CA, 2006, pp. 836\u2013843.","DOI":"10.1145\/1233501.1233679"},{"key":"6145_CR5","volume-title":"Hardware Design Verification: Simulation and Formal Method-Based Approaches","author":"W.K. Lam","year":"2005","unstructured":"Lam, W.K., Hardware Design Verification: Simulation and Formal Method-Based Approaches, New York: Prentice Hall, 2005."},{"issue":"2","key":"6145_CR6","first-page":"22","volume":"4","author":"L. Li","year":"2006","unstructured":"Li, L., Thornton, M.A., and Szygenda, S.A., Integrated Design Validation: Combining Simulation and Formal Verification for Digital Integrated Circuits, J. Systemics, Cybernetics and Informatics, 2006, vol. 4, no. 2, pp. 22\u201330.","journal-title":"J. Systemics, Cybernetics and Informatics"},{"key":"6145_CR7","unstructured":"Cheremisinova, L. and Novikov, D.Ya., SAT-Based Approach to Verification of Logical Descriptions with Functional Indeterminacy, Proc. 8th Int. Workshop on Boolean Problems, Freiberg, 2008, pp. 59\u201366."},{"issue":"1","key":"6145_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3103\/S0146411610010013","volume":"44","author":"L.D. Cheremisinova","year":"2010","unstructured":"Cheremisinova, L.D. and Novikov, D.Ya., SAT-Based Formal Verification of Logical Descriptions with Functional Indeterminacy, Autom. Control Compt. Sci., 2010, vol. 44, no. 1, pp. 1\u201310.","journal-title":"Autom. Control Compt. Sci."},{"key":"6145_CR9","unstructured":"Novikov, D.Ya. and Cheremisinova, L.D., Verification of Functional Descriptions with Indeterminacy on the Base of Paraphase Presentation of Boolean Functions, Informatika, 2010, no. 3, pp. 54\u201362."},{"key":"6145_CR10","unstructured":"Sorensson, N. and Een, N., MiniSat v1.13\u2014A SAT Solver with Conflict-Clause Minimization, Proc. Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 2005). http:\/\/www.lri.fr\/~simon\/contest\/results\/descriptions\/solvers\/minisat-static.pdf"},{"key":"6145_CR11","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":"6145_CR12","doi-asserted-by":"crossref","unstructured":"Goldberg, E. and Novikov, D.Ya., BerkMin: A Fast and Robust SAT-Solver, Proc. European Design and Test Conf., 2002, pp. 142\u2013149.","DOI":"10.1109\/DATE.2002.998262"}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411611040055.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411611040055","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411611040055","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411611040055.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T21:59:28Z","timestamp":1773611968000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411611040055"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,8]]},"references-count":12,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2011,8]]}},"alternative-id":["6145"],"URL":"https:\/\/doi.org\/10.3103\/s0146411611040055","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,8]]},"assertion":[{"value":"28 March 2011","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 September 2011","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}