{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T01:46:54Z","timestamp":1780537614070,"version":"3.54.1"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2023,5,30]],"date-time":"2023-05-30T00:00:00Z","timestamp":1685404800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,5,30]],"date-time":"2023-05-30T00:00:00Z","timestamp":1685404800000},"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":["J. Comput. Sci. Technol."],"published-print":{"date-parts":[[2023,6]]},"DOI":"10.1007\/s11390-022-1981-4","type":"journal-article","created":{"date-parts":[[2023,8,8]],"date-time":"2023-08-08T10:02:20Z","timestamp":1691488940000},"page":"702-713","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["A Semi-Tensor Product Based All Solutions Boolean Satisfiability Solver"],"prefix":"10.1007","volume":"38","author":[{"given":"Hong-Yang","family":"Pan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhu-Fei","family":"Chu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,5,30]]},"reference":[{"key":"1981_CR1","doi-asserted-by":"publisher","unstructured":"Cook S A. The complexity of theorem-proving procedures. In Proc. the 3rd Annual ACM Symposium on Theory of Computing, May 1971, pp.151\u2013158. https:\/\/doi.org\/10.1145\/800157.805047.","DOI":"10.1145\/800157.805047"},{"key":"1981_CR2","doi-asserted-by":"publisher","unstructured":"E\u00e9n N, S\u00f6rensson N. An extensible SAT-solver. In Proc. the 6th International Conference on Theory and Applications of Satisfiability Testing, May 2004, pp.502\u2013518. https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37.","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"1981_CR3","doi-asserted-by":"publisher","unstructured":"Moskewicz M W, Madigan C F, Zhao Y, Zhang L T, Malik S. Chaff: Engineering an efficient SAT solver. In Proc. the 38th Annual Design Automation Conference, Jun. 2001, pp.530\u2013535. https:\/\/doi.org\/10.1145\/378239.379017.","DOI":"10.1145\/378239.379017"},{"key":"1981_CR4","doi-asserted-by":"publisher","unstructured":"Mishchenko A, Chatterjee S, Brayton R, Een N. Improvements to combinational equivalence checking. In Proc. the 2006 IEEE\/ACM International Conference on Computer Aided Design, Nov. 2006, pp.836\u2013843. https:\/\/doi.org\/10.1109\/ICCAD.2006.320087.","DOI":"10.1109\/ICCAD.2006.320087"},{"key":"1981_CR5","doi-asserted-by":"crossref","unstructured":"Froleyks N, Heule M, Iser M, J\u00e4rvisalo M, Suda M. SAT competition 2020. Artificial Intelligence, 2021, 301: 103572.","DOI":"10.1016\/j.artint.2021.103572"},{"issue":"7","key":"1981_CR6","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis M, Logemann G, Loveland D. A machine program for theorem-proving. Communications of the ACM, 1962, 5(7): 394\u2013397. https:\/\/doi.org\/10.1145\/368273.368557.","journal-title":"Communications of the ACM"},{"key":"1981_CR7","doi-asserted-by":"publisher","unstructured":"Legg A, Narodytska N, Ryzhyk L. A SAT-based counterexample guided method for unbounded synthesis. In Proc. the 28th International Conference on Computer Aided Verification, Jul. 2016, pp.364\u2013382. https:\/\/doi.org\/10.1007\/978-3-319-41540-6_20.","DOI":"10.1007\/978-3-319-41540-6_20"},{"key":"1981_CR8","doi-asserted-by":"publisher","unstructured":"Lowry M, Loh T H. Quantifying bicycle network connectivity. Preventive Medicine, 2017, 95 Supp.: S134\u2013S140. https:\/\/doi.org\/10.1016\/j.ypmed.2016.12.007.","DOI":"10.1016\/j.ypmed.2016.12.007"},{"issue":"1","key":"1981_CR9","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/s10618-006-0059-1","volume":"15","author":"JW Han","year":"2007","unstructured":"Han J W, Cheng H, Xin D, Yan X F. Frequent pattern mining: Current status and future directions. Data Mining and Knowledge Discovery, 2007, 15(1): 55\u201386. https:\/\/doi.org\/10.1007\/s10618-006-0059-1.","journal-title":"Data Mining and Knowledge Discovery"},{"key":"1981_CR10","doi-asserted-by":"publisher","unstructured":"Toda T, Soh T. Implementing efficient all solutions SAT solvers. ACM Journal of Experimental Algorithmics, 2016, 21: Article No. 1.12. https:\/\/doi.org\/10.1145\/2975585.","DOI":"10.1145\/2975585"},{"key":"1981_CR11","doi-asserted-by":"publisher","unstructured":"Ren X Q, Guo W X, Mo Z Q, Tian W H. A divide and conquer approach to all solutions satisfiability problem. In Proc. the 4th IEEE International Conference on Computer and Communications (ICCC), Dec. 2018, pp.2590\u20132595. https:\/\/doi.org\/10.1109\/CompComm.2018.8780746.","DOI":"10.1109\/CompComm.2018.8780746"},{"key":"1981_CR12","doi-asserted-by":"publisher","unstructured":"Zhang Y L, Pu G G, Sun J. Accelerating all-SAT computation with short blocking clauses. In Proc. the 35th IEEE\/ACM International Conference on Automated Software Engineering, Feb. 2020, pp.6\u201317. https:\/\/doi.org\/10.1145\/3324884.3416569.","DOI":"10.1145\/3324884.3416569"},{"key":"1981_CR13","doi-asserted-by":"publisher","unstructured":"Thiffault C, Bacchus F, Walsh T. Solving non-clausal formulas with DPLL search. In Proc. the 10th International Conference on Principles and Practice of Constraint Programming, Oct. 2004, pp.663\u2013678. https:\/\/doi.org\/10.1007\/978-3-540-30201-8_48.","DOI":"10.1007\/978-3-540-30201-8_48"},{"key":"1981_CR14","doi-asserted-by":"publisher","unstructured":"Marques-Silva J, Lynce I, Malik S. Conflict-driven clause learning SAT solvers. In Handbook of Satisfiability, Biere A, Heule M, van Maaren H, Walsh T (eds.), IOS Press, 2009, pp.133\u2013182. https:\/\/doi.org\/10.3233\/978-1-58603-929-5-131.","DOI":"10.3233\/978-1-58603-929-5-131"},{"key":"1981_CR15","doi-asserted-by":"publisher","unstructured":"Ganai M K, Ashar P, Gupta A, Zhang L T, Malik S. Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver. In Proc. the 39th Annual Design Automation Conference, Jun. 2002, pp.747\u2013750. https:\/\/doi.org\/10.1145\/513918.514105.","DOI":"10.1145\/513918.514105"},{"issue":"2","key":"1981_CR16","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/s11424-007-9027-0","volume":"20","author":"DZ Cheng","year":"2007","unstructured":"Cheng D Z, Qi H S, Xue A C. A survey on semi-tensor product of matrices. Journal of Systems Science and Complexity, 2007, 20(2): 304\u2013322. https:\/\/doi.org\/10.1007\/s11424-007-9027-0.","journal-title":"Journal of Systems Science and Complexity"},{"key":"1981_CR17","doi-asserted-by":"publisher","unstructured":"Bai Z W, Li Y, Zhou M L, Li D, Wang D, Po\u0142ap D, Wo\u017aniak M. Bilinear semi-tensor product attention (BST-PA) model for visual question answering. In Proc. the 2020 International Joint Conference on Neural Networks (IJCNN), Jul. 2020. https:\/\/doi.org\/10.1109\/IJCNN48605.2020.9206964.","DOI":"10.1109\/IJCNN48605.2020.9206964"},{"key":"1981_CR18","doi-asserted-by":"publisher","unstructured":"Fu W, Li S T. Semi-tensor compressed sensing for hyperspectral image. In Proc. the 2018 IEEE International Geoscience and Remote Sensing Symposium, Jul. 2018, pp.2737\u20132740. https:\/\/doi.org\/10.1109\/IGARSS.2018.8519360.","DOI":"10.1109\/IGARSS.2018.8519360"},{"key":"1981_CR19","doi-asserted-by":"publisher","unstructured":"Han X G, Chen Z Q, Liu Z X, Zhang Q. Calculating basis siphons of Petri nets based on semi-tensor product of matrices. In Proc. the 35th Chinese Control Conference, Jul. 2016, pp.2331\u20132336. https:\/\/doi.org\/10.1109\/ChiCC.2016.7553712.","DOI":"10.1109\/ChiCC.2016.7553712"},{"key":"1981_CR20","doi-asserted-by":"publisher","unstructured":"Cheng D Z, Qi H S, Zhao Y. An Introduction to Semi-Tensor Product of Matrices and Its Applications. World Scientific, 2012. https:\/\/doi.org\/10.1142\/8323.","DOI":"10.1142\/8323"},{"issue":"1\/2","key":"1981_CR21","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0377-0427(00)00393-9","volume":"123","author":"CF Van Loan","year":"2000","unstructured":"Van Loan C F. The ubiquitous Kronecker product. Journal of Computational and Applied Mathematics, 2000, 123(1\/2): 85\u2013100. https:\/\/doi.org\/10.1016\/S0377-0427(00)00393-9.","journal-title":"Journal of Computational and Applied Mathematics"},{"key":"1981_CR22","doi-asserted-by":"publisher","unstructured":"Cheng D Z. On logic-based intelligent systems. In Proc. the 2005 International Conference on Control and Automation, Jun. 2005, pp.71\u201376. https:\/\/doi.org\/10.1109\/ICCA.2005.1528094.","DOI":"10.1109\/ICCA.2005.1528094"},{"issue":"5","key":"1981_CR23","doi-asserted-by":"publisher","first-page":"751","DOI":"10.1080\/0952813X.2019.1672798","volume":"32","author":"S Siddiqi","year":"2020","unstructured":"Siddiqi S. An extensible circuit-based SAT solver. Journal of Experimental & Theoretical Artificial Intelligence, 2020, 32(5): 751\u2013768. https:\/\/doi.org\/10.1080\/0952813X.2019.1672798.","journal-title":"Journal of Experimental & Theoretical Artificial Intelligence"},{"key":"1981_CR24","unstructured":"Yang S. Logic Synthesis and Optimization Benchmarks User Guide: Version 3.0. Research Triangle Park, NC, USA: Microelectronics Center of North Carolina (MCNC), 1991."}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-022-1981-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11390-022-1981-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-022-1981-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,8]],"date-time":"2023-08-08T10:36:21Z","timestamp":1691490981000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11390-022-1981-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,30]]},"references-count":24,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,6]]}},"alternative-id":["1981"],"URL":"https:\/\/doi.org\/10.1007\/s11390-022-1981-4","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,5,30]]},"assertion":[{"value":"1 November 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 December 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 May 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}