{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T15:21:54Z","timestamp":1784906514315,"version":"3.55.0"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2020,6,29]],"date-time":"2020-06-29T00:00:00Z","timestamp":1593388800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,6,29]],"date-time":"2020-06-29T00:00:00Z","timestamp":1593388800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Ambient Intell Human Comput"],"published-print":{"date-parts":[[2022,7]]},"DOI":"10.1007\/s12652-020-02247-w","type":"journal-article","created":{"date-parts":[[2020,6,29]],"date-time":"2020-06-29T18:03:42Z","timestamp":1593453822000},"page":"3693-3711","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Computation of minimal unsatisfiable subformulas for SAT-based digital circuit error diagnosis"],"prefix":"10.1007","volume":"13","author":[{"given":"Lamya","family":"Gaber","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aziza I.","family":"Hussein","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hanafy","family":"Mahmoud","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"M. Mourad","family":"Mabrook","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mohammed","family":"Moness","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,6,29]]},"reference":[{"key":"2247_CR1","doi-asserted-by":"crossref","unstructured":"Ali LG, Hussein AI, Ali HM (2016) Parallelization of unit propagation algorithm for SAT-based ATPG of digital circuits. In: Microelectronics (ICM) 28th international conference 184\u2013188. Doi: 10.1109\/ICCES.2017.8275337.","DOI":"10.1109\/ICM.2016.7847940"},{"key":"2247_CR2","doi-asserted-by":"crossref","unstructured":"Ali LG, Hussein AI, Ali HM (2017)  An efficient computation of minimal correction subformulas for SAT-based ATPG of digital circuits. In: Computer engineering and systems (ICCES), 12th international conference, pp 383\u2013389. doi: 10.1109\/ICCES.2017.8275337.","DOI":"10.1109\/ICCES.2017.8275337"},{"issue":"6","key":"2247_CR3","doi-asserted-by":"publisher","first-page":"1564","DOI":"10.1109\/TC.2014.2329687","volume":"64","author":"B Alizadeh","year":"2014","unstructured":"Alizadeh B,  Behnam P,  Sadeghi-Kohan S (2014) A scalable formal debugging approach with auto-correction capability based on static slicing and dynamic ranking for RTL datapath designs. IEEE Trans Comput 64(6):1564\u20131578 https:\/\/doi.org\/10.1109\/TC.2014.2329687","journal-title":"IEEE Trans Comput"},{"key":"2247_CR4","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1090\/dimacs\/026\/18","volume":"26","author":"Y Asahiro","year":"1996","unstructured":"Asahiro Y, Iwama K, Miyano E (1996) Random generation of test instances with controlled attributes. DIMACS Ser Discrete Math Theoretical Comput Sci 26:377\u2013394","journal-title":"DIMACS Ser Discrete Math Theoretical Comput Sci"},{"key":"2247_CR5","doi-asserted-by":"publisher","DOI":"10.5075\/epfl-thesis-8850","author":"AJ Becker","year":"2018","unstructured":"Becker AJ (2018) Satisfiability-based methods for digital circuit design, debug, and optimization EPFL https:\/\/doi.org\/10.5075\/epfl-thesis-8850","journal-title":"EPFL"},{"key":"2247_CR6","doi-asserted-by":"crossref","unstructured":"Belov A, Heule M J, Marques-Silva J (2014). MUS extraction using clausal proofs. International Conference on Theory and Applications of Satisfiability Testing, 48-57. https:\/\/doi.org\/10.1007\/978-3-319-09284-3_5","DOI":"10.1007\/978-3-319-09284-3_5"},{"key":"2247_CR7","doi-asserted-by":"crossref","unstructured":"Bend\u00edk J, \u010cern\u00e1 I , Bene\u0161 N. (2018). Recursive online enumeration of all minimal unsatisfiable subsets. In: International symposium on automated technology for verification and analysis, pp 143\u2013159.","DOI":"10.1007\/978-3-030-01090-4_9"},{"key":"2247_CR8","unstructured":"Bend\u00edk J, Cerna I (2018) Evaluation of domain agnostic approaches for enumeration of minimal unsatisfiable subsets. In: LPAR. 131\u2013142."},{"key":"2247_CR9","doi-asserted-by":"crossref","unstructured":"Bend\u00edk J, \u010cern\u00e1 I (2020) MUST: Minimal Unsatisfiable Subsets Enumeration Tool. International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 135-152. https:\/\/doi.org\/10.1007\/978-3-030-45190-5_8","DOI":"10.1007\/978-3-030-45190-5_8"},{"key":"2247_CR10","doi-asserted-by":"publisher","first-page":"59","DOI":"10.3233\/SAT190075","volume":"7","author":"D Le Berre","year":"2010","unstructured":"Berre Le D,  Parrain A (2010) The Sat4j library, release 2.2. J Satisfiability Boolean Modeling Comput 7:59\u201364 https:\/\/doi.org\/10.3233\/SAT190075","journal-title":"J Satisfiability Boolean Modeling Comput"},{"key":"2247_CR11","unstructured":"Bryan D (1985) The ISCAS'85 benchmark circuits and netlist format. North Carolina State University pp 25"},{"key":"2247_CR12","doi-asserted-by":"publisher","first-page":"2519","DOI":"10.1007\/s12652-018-0730-6","volume":"10","author":"S Cai","year":"2019","unstructured":"Cai S,  Gallina B,  Nystr\u00f6m D, Seceleanu C,  Larsson A (2019) Tool-supported design of data aggregation processes in cloud monitoring systems. J Ambient Intell Human Comput 10:2519\u20132535 https:\/\/doi.org\/10.1007\/s12652-018-0730-6","journal-title":"J Ambient Intell Human Comput"},{"issue":"11","key":"2247_CR13","doi-asserted-by":"publisher","first-page":"1804","DOI":"10.1109\/TCAD.2010.2061270","volume":"29","author":"Y Chen","year":"2010","unstructured":"Chen Y,  Safarpour S,  Marques-Silva J,  Veneris A (2010) Automated design debugging with maximum satisfiability. IEEE Trans Comput Aided Des Integr Circuits Syst 29(11):1804\u20131817 https:\/\/doi.org\/10.1109\/TCAD.2010.2061270","journal-title":"IEEE Trans Comput Aided Des Integr Circuits Syst"},{"key":"2247_CR14","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1007\/s12652-013-0183-x","volume":"5","author":"F Corno","year":"2014","unstructured":"Corno F, Razzak F (2014) SAT based enforcement of domotic effects in smart environments. J Ambient Intell Human Comput 5:565\u2013579 https:\/\/doi.org\/10.1007\/s12652-013-0183-x","journal-title":"J Ambient Intell Human Comput"},{"key":"2247_CR15","unstructured":"Dave AH (2018) Application of machine learning in digital logic circuit design verification and testing. Doctoral dissertation, California State University, Fresno."},{"key":"2247_CR16","doi-asserted-by":"crossref","unstructured":"De Moura L, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: International conference on tools and algorithms for the construction and analysis of systems, 337\u2013340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"2247_CR17","doi-asserted-by":"crossref","unstructured":"Foss\u00e9 R, Simon L (2018) On the non-degeneracy of unsatisfiability proof graphs produced by SAT solvers. In: International conference on principles and practice of constraint programming, 128\u2013143.","DOI":"10.1007\/978-3-319-98334-9_9"},{"key":"2247_CR18","doi-asserted-by":"crossref","unstructured":"Gaber L, Hussein AI, Moness M (2019) Improved automatic correction for digital VLSI circuits. In: 2019 31st international conference on microelectronics (ICM) 18\u201322. 10.1109\/ICM48031.2019.9021938","DOI":"10.1109\/ICM48031.2019.9021938"},{"key":"2247_CR19","doi-asserted-by":"crossref","unstructured":"Guthmann O, Strichman O, Trostanetski A (2016) Minimal unsatisfiable core extraction for SMT. In: 2016 Formal methods in computer-aided design (FMCAD), 57\u201364. Doi: 10.5555\/3077629.3077644","DOI":"10.1109\/FMCAD.2016.7886661"},{"key":"2247_CR20","unstructured":"G\u00f3mez LIR (2017) Machine learning support for logic diagnosis. Doctoral dissertation, University of Stuttgart."},{"key":"2247_CR21","doi-asserted-by":"crossref","unstructured":"Hagihara S, Egawa N, Shimakawa M, Yonezaki N (2014). Minimal strongly unsatisfiable subsets of reactive system specifications. Proceedings of the 29th ACM\/IEEE international conference on Automated software engineering 629\u2013634.","DOI":"10.1145\/2642937.2642968"},{"key":"2247_CR22","doi-asserted-by":"crossref","unstructured":"Ignatiev A, Previti A, Liffiton M, Marques-Silva J (2015) Smallest MUS extraction with minimal hitting set dualization. In: Pesant G (ed), Principles and practice of constraint programming: 21st international conference, CP 2015 Cork, Ireland, 9255: 173\u2013182. Springer doi: 10.1007\/978\u20133\u2013319\u201323219\u20135_13","DOI":"10.1007\/978-3-319-23219-5_13"},{"key":"2247_CR23","unstructured":"Koitz-Hristov R, Wotawa F (2018) On the superiority of conflict-driven search in MUs enumeration. In: CEUR workshop proceedings, 2289."},{"key":"2247_CR24","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/j.ic.2016.03.006","volume":"252","author":"I Konnov","year":"2017","unstructured":"Konnov I, Veith H,  Widder J (2017) On the completeness of bounded model checking for threshold-based distributed algorithms: reachability. Inf Comput 252:95\u2013109","journal-title":"Inf Comput"},{"key":"2247_CR25","doi-asserted-by":"crossref","unstructured":"Leo K, Tack G (2017) Debugging unsatisfiable constraint models. In: International conference on AI and OR techniques in constraint programming for combinatorial optimization problems. 77\u201393.","DOI":"10.1007\/978-3-319-59776-8_7"},{"key":"2247_CR26","doi-asserted-by":"crossref","unstructured":"Li J, Zhu S, Zhang Y, Pu G, Vari MY (2017) Safety model checking with complementary approximations. In: Proceedings of the 36th international conference on computer-aided design. 95\u2013100.","DOI":"10.1109\/ICCAD.2017.8203765"},{"key":"2247_CR27","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/s10601-015-9183-0","volume":"21","author":"MH Liffiton","year":"2016","unstructured":"Liffiton MH, Previti A,  Malik A, Silva JM (2016) Fast, flexible MUS enumeration Constraints 21:223\u2013250 https:\/\/doi.org\/10.1007\/s10601-015-9183-0","journal-title":"Constraints"},{"key":"2247_CR28","doi-asserted-by":"crossref","unstructured":"Liffiton MH, Malik A (2013) Enumerating infeasibility: finding multiple MUSes quickly. In: International conference on AI and OR techniques in constriant programming for combinatorial optimization problems, 160\u2013175. Doi: 10.1007\/978\u20133\u2013642\u201338171\u20133_11","DOI":"10.1007\/978-3-642-38171-3_11"},{"issue":"2","key":"2247_CR29","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/s10836-018-5716-y","volume":"34","author":"E Mandouh","year":"2018","unstructured":"Mandouh E,  Wassal AG (2018) Application of machine learning techniques in post-silicon debugging and bug localization J. Electron. Test. 34(2) 163\u2013181 https:\/\/doi.org\/10.1007\/s10836-018-5716-y","journal-title":"J. Electron. Test."},{"issue":"1","key":"2247_CR30","first-page":"163","volume":"19","author":"J Marques-Silva","year":"2012","unstructured":"Marques-Silva J (2012) Computing minimally unsatisfiable subformulas: state of the art and future directions. J Multiple Valued Logic Soft Comput 19(1):163\u2013183","journal-title":"J Multiple Valued Logic Soft Comput"},{"key":"2247_CR31","doi-asserted-by":"crossref","unstructured":"Marques-Silva J, Janota M, Belov A (2013) . Minimal sets over monotone predicates in boolean formulae. International Conference on Computer Aided Verification, 592-607. https:\/\/doi.org\/10.1007\/978-3-642-39799-8_39","DOI":"10.1007\/978-3-642-39799-8_39"},{"key":"2247_CR32","doi-asserted-by":"publisher","first-page":"27","DOI":"10.3233\/SAT190100","volume":"9","author":"A Nadel","year":"2014","unstructured":"Nadel A, Ryvchin V,  Strichman O (2014) Accelerated deletion-based extraction of minimal unsatisfiable cores. J Satisfiability Boolean Modeling Comput 9: 27\u201351","journal-title":"J Satisfiability Boolean Modeling Comput"},{"key":"2247_CR33","doi-asserted-by":"publisher","unstructured":"Narodytska N, Bj\u00f8rner N, Marinescu M-C, Sagiv M (2018). Core-Guided Minimal Correction Set and Core Enumeration. In: IJCAI, 1353\u20131361. https:\/\/doi.org\/10.24963\/ijcai.2018\/188","DOI":"10.24963\/ijcai.2018\/188"},{"key":"2247_CR34","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/s10836-018-5747-4","volume":"34","author":"M Osama","year":"2018","unstructured":"Osama M, Gaber L, Hussein AI, Mahmoud H (2018) An efficient SAT-based test generation algorithm with GPU accelerator J Electron Testing 34:511\u2013527 https:\/\/doi.org\/10.1007\/s10836-018-5747-4","journal-title":"J Electron Testing"},{"key":"2247_CR35","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1080\/0952813X.2014.954274","volume":"27","author":"A Dal Pal\u00f9","year":"2014","unstructured":"Pal\u00f9 Dal A,  Dovier A,  Formisano A,  Pontelli E (2014) Cud@ sat: sat solving on gpus J Exp Theor Artif Intell 27:293\u2013316 https:\/\/doi.org\/10.1080\/0952813X.2014.954274","journal-title":"J Exp Theor Artif Intell"},{"key":"2247_CR36","unstructured":"Ren Z, Al-Asaad H (2016) Overview of assertion-based verification and its applications.\u00a0In: Int'l conf. embedded systems, cyber-physical systems, & applications"},{"key":"2247_CR37","doi-asserted-by":"crossref","unstructured":"Shi J, Fey G, Drechsler R, Glowatz A, Hapke F, Schloffel J, PASSAT (2005) Efficient SAT-based test pattern generation for industrial circuits. In: IEEE computer society annual symposium on VLSI: new frontiers in VLSI Design (ISVLSI'05), 212\u2013217. Doi: 10.1109\/ISVLSI.2005.55","DOI":"10.1109\/ISVLSI.2005.55"},{"key":"2247_CR38","doi-asserted-by":"crossref","unstructured":"Shimakawa M, Hagihara S, Yonezaki N (2018) Efficiency of the strong satisfiability checking procedure for reactive system specifications. In: AIP conference proceedings, 1955(1). Doi: 10.1063\/1.5033715.","DOI":"10.1063\/1.5033715"},{"key":"2247_CR39","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1016\/j.jpdc.2016.12.014","volume":"106","author":"AA Sohanghpurwala","year":"2017","unstructured":"AA Sohanghpurwala MW Hassan P Athanas 2017 Hardware accelerated SAT solvers\u2014a survey J Parallel Distributed Comput 106: 170\u2013184 https:\/\/doi.org\/10.1016\/j.jpdc.2016.12.014","journal-title":"J Parallel Distributed Comput"},{"key":"2247_CR40","doi-asserted-by":"crossref","unstructured":"Zhang J, Li T, S. Li, (2015). Application and analysis of unsatisfiable cores on circuits synthesis, Seventh International Conference on Advanced Computational Intelligence (ICACI): 407\u2013410, doi: 10.1109\/ICACI.2015.7184740.","DOI":"10.1109\/ICACI.2015.7184740"},{"key":"2247_CR41","unstructured":"Zhendong L, Shaowei C (2018) Solving (weighted) partial MaxSAT by dynamic local search for SAT. In: Proceedings of the 27th international joint conference on artificial intelligence (IJCAI\u201918), AAAI Press, 1346\u20131352."},{"key":"2247_CR42","doi-asserted-by":"crossref","unstructured":"Zielke C, Kaufmann M (2015) A new approach to partial MUS enumeration. International Conference on Theory and Applications of Satisfiability Testing, 387-404. https:\/\/doi.org\/10.1007\/978-3-319-24318-4_28","DOI":"10.1007\/978-3-319-24318-4_28"},{"key":"2247_CR43","unstructured":"da Silva PFM (2010) Max-SAT algorithms for real world instances. Master Dissertation."}],"container-title":["Journal of Ambient Intelligence and Humanized Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s12652-020-02247-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s12652-020-02247-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s12652-020-02247-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,9]],"date-time":"2022-06-09T11:55:26Z","timestamp":1654775726000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s12652-020-02247-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,29]]},"references-count":43,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2022,7]]}},"alternative-id":["2247"],"URL":"https:\/\/doi.org\/10.1007\/s12652-020-02247-w","relation":{},"ISSN":["1868-5137","1868-5145"],"issn-type":[{"value":"1868-5137","type":"print"},{"value":"1868-5145","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,6,29]]},"assertion":[{"value":"26 October 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 June 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 June 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}