{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T17:47:06Z","timestamp":1767980826206,"version":"3.49.0"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2018,8,30]],"date-time":"2018-08-30T00:00:00Z","timestamp":1535587200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Electron Test"],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.1007\/s10836-018-5747-4","type":"journal-article","created":{"date-parts":[[2018,8,30]],"date-time":"2018-08-30T07:07:36Z","timestamp":1535612856000},"page":"511-527","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":22,"title":["An Efficient SAT-Based Test Generation Algorithm with GPU Accelerator"],"prefix":"10.1007","volume":"34","author":[{"given":"Muhammad","family":"Osama","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lamya","family":"Gaber","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5023-5348","authenticated-orcid":false,"given":"Aziza I.","family":"Hussein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hanafy","family":"Mahmoud","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,30]]},"reference":[{"key":"5747_CR1","unstructured":"Ali LG, Hussein AI and Ali HM (2016) \"Parallelization of unit propagation algorithm for SAT-based ATPG of digital circuits,\" in Proc. 2016 28th international conference on microelectronics (ICM), pp. 184\u2013188"},{"key":"5747_CR2","doi-asserted-by":"crossref","unstructured":"Arora R and Hsiao MS (2003) \"Enhancing sat-based equivalence checking with static logic implications,\" in Proc Eighth IEEE International High-Level Design Validation and Test Workshop, pp. 63\u201368: IEEE","DOI":"10.1109\/HLDVT.2003.1252476"},{"issue":"2","key":"5747_CR3","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/j.micpro.2012.09.010","volume":"37","author":"J Balcarek","year":"2013","unstructured":"Balcarek J, Fiser P, Schmidt J (2013) Techniques for SAT-based constrained test pattern generation. Microprocess Microsyst 37(2):185\u2013195","journal-title":"Microprocess Microsyst"},{"key":"5747_CR4","unstructured":"Biere A (2015) \"Lingeling SAT Solver,\" SAT Competitions 2014\u20132016, no. January"},{"key":"5747_CR5","doi-asserted-by":"crossref","unstructured":"Bjesse P, Leonard T and Mokkedem A (2001) Finding bugs in an alpha microprocessor using satisfiability solvers, in Computer Aided Verification, pp. 454\u2013464: Springer","DOI":"10.1007\/3-540-44585-4_44"},{"key":"5747_CR6","unstructured":"Brglez F (1985) \"a neutral netlist of 10 combinational benchmark circuits and a target translation in FORTRAN,\" in ISCAS-85"},{"key":"5747_CR7","doi-asserted-by":"crossref","unstructured":"Brglez F, Bryan D, and Ko\u017ami\u0144ski K (1989) \"Combinational profiles of sequential benchmark circuits,\" in Proc IEEE International Symposium on Circuits and Systems, pp. 1929\u20131934: IEEE","DOI":"10.1109\/ISCAS.1989.100747"},{"key":"5747_CR8","unstructured":"Brglez F, Bryan D, and Ko\u017ami\u0144ski K ISCAS 85\u201389 Circuits Benchmark Suite [Online]. Available: http:\/\/www.cbl.ncsu.edu:16080\/benchmarks\/"},{"key":"5747_CR9","doi-asserted-by":"crossref","unstructured":"Cai X, Wohl P, Waicukauski JA, and Notiyath P (2010) \"Highly efficient parallel ATPG based on shared memory,\" in Proc. 2010 IEEE international test conference, pp. 1\u20137","DOI":"10.1109\/TEST.2010.5699236"},{"issue":"7","key":"5747_CR10","doi-asserted-by":"publisher","first-page":"1015","DOI":"10.1109\/43.238038","volume":"12","author":"ST Chakradhar","year":"1993","unstructured":"Chakradhar ST, Agrawal VD, Rothweiler SG (1993) A transitive closure algorithm for test generation. IEEE Trans Comput-Aided Des Integrated Circ Systs 12(7):1015\u20131028","journal-title":"IEEE Trans Comput-Aided Des Integrated Circ Systs"},{"issue":"3","key":"5747_CR11","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1109\/54.867894","volume":"17","author":"F. Corno","year":"2000","unstructured":"Corno F, Reorda MS, Squillero G (2000) RT-level ITC'99 benchmarks and first ATPG results. 17(3):44\u201353","journal-title":"IEEE Design & Test of Computers"},{"key":"5747_CR12","unstructured":"Corno F, Reorda MS, and Squillero G Collection of Digital Design Benchmarks - ITC'99 Test Suite [Online]. Available: http:\/\/ddd.fit.cvut.cz\/prj\/Benchmarks\/"},{"key":"5747_CR13","doi-asserted-by":"crossref","unstructured":"Czutro A, Polian I, Lewis M, Engelke P, Reddy SM, and Becker B (2009) \"Tiguan: Thread-parallel integrated test pattern generator utilizing satisfiability analysis,\" in Proc. 22nd International Conference on VLSI Design, pp. 227\u2013232: IEEE","DOI":"10.1109\/VLSI.Design.2009.20"},{"issue":"3","key":"5747_CR14","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1080\/0952813X.2014.954274","volume":"27","author":"A Dal Pal\u00f9","year":"2015","unstructured":"Dal Pal\u00f9 A, Dovier A, Formisano A, Pontelli E (2015) CUD@SAT: SAT solving on GPUs. J Exp Theor Artif Intelligence 27(3):293\u2013316","journal-title":"J Exp Theor Artif Intelligence"},{"key":"5747_CR15","unstructured":"Dechter R (2003) Constraint processing. Morgan Kaufmann Publishers Inc,, p. 450"},{"issue":"6","key":"5747_CR16","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1016\/j.csi.2004.09.004","volume":"27","author":"R Djemal","year":"2005","unstructured":"Djemal R, Dhouib MA, Dellacherie S, Tourki R (2005) A novel formal verification approach for RTL hardware IP cores. Comput Standards Interfaces 27(6):637\u2013651","journal-title":"Comput Standards Interfaces"},{"key":"5747_CR17","doi-asserted-by":"crossref","unstructured":"E\u00e9n N and Biere A (2005) \"Effective preprocessing in SAT through variable and clause elimination,\" in Proc Theory and Applications of Satisfiability Testing, pp. 61\u201375: Springer","DOI":"10.1007\/11499107_5"},{"key":"5747_CR18","doi-asserted-by":"crossref","unstructured":"E\u00e9n N and S\u00f6rensson N (2003) \"An extensible SAT-solver,\" in Proc. International conference on theory and applications of satisfiability testing, pp. 502\u2013518: Springer","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"5747_CR19","unstructured":"Fujiwara H (1985) \"Fan: a fanout-oriented test pattern generation algorithm,\" in Proc. IEEE international symposium on circuits and systems, pp. 671\u2013674"},{"key":"5747_CR20","unstructured":"Goel P (1995) \"An implicit enumeration algorithm to generate tests for combinational logic circuits,\" in Fault-Tolerant Computing, p. 337"},{"issue":"12","key":"5747_CR21","doi-asserted-by":"publisher","first-page":"1549","DOI":"10.1016\/j.dam.2006.10.007","volume":"155","author":"E Goldberg","year":"2007","unstructured":"Goldberg E, Novikov Y (2007) BerkMin: a fast and robust SAT-solver. Discret Appl Math 155(12):1549\u20131561","journal-title":"Discret Appl Math"},{"key":"5747_CR22","unstructured":"E. Goldberg, M. Prasad, and R. Brayton (2001) Using SAT for combinational equivalence checking, in Proc of the conference on Design, automation and test in Europe, pp. 114\u2013121: IEEE Press"},{"key":"5747_CR23","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/11757283_5","volume-title":"Formal methods for hardware verification: 6th international school on formal methods for the Design of Computer, communication, and software systems, SFM 2006, Bertinoro, Italy, may 22\u201327, 2006","author":"A Gupta","year":"2006","unstructured":"Gupta A, Ganai MK, Wang C (2006) SAT-based verification methods and applications in hardware verification. In: Bernardo M, Cimatti A (eds) Formal methods for hardware verification: 6th international school on formal methods for the Design of Computer, communication, and software systems, SFM 2006, Bertinoro, Italy, may 22\u201327, 2006, Advanced Lectures. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 108\u2013143"},{"issue":"3","key":"5747_CR24","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1016\/j.tcs.2008.03.013","volume":"404","author":"F Ivan\u010di\u0107","year":"2008","unstructured":"Ivan\u010di\u0107 F, Yang Z, Ganai MK, Gupta A, Ashar P (2008) Efficient SAT-based bounded model checking for software verification. Theor Comput Sci 404(3):256\u2013274","journal-title":"Theor Comput Sci"},{"issue":"1","key":"5747_CR25","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.jalgor.2008.02.005","volume":"63","author":"M J\u00e4rvisalo","year":"2008","unstructured":"J\u00e4rvisalo M, Niemel\u00e4 I (2008) The effect of structural branching on the efficiency of clause learning SAT solving: an experimental study. J Algoritm 63(1):90\u2013113","journal-title":"J Algoritm"},{"issue":"7\u20138","key":"5747_CR26","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1016\/j.scico.2011.02.003","volume":"77","author":"S Kemper","year":"2012","unstructured":"Kemper S (2012) SAT-based verification for timed component connectors. Sci Comput Program 77(7\u20138):779\u2013798","journal-title":"Sci Comput Program"},{"issue":"1","key":"5747_CR27","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1109\/43.108614","volume":"11","author":"T Larrabee","year":"1992","unstructured":"Larrabee T (1992) Test pattern generation using Boolean satisfiability. Comput-Aided Des Integrated Circuits Syst, IEEE Trans on 11(1):4\u201315","journal-title":"Comput-Aided Des Integrated Circuits Syst, IEEE Trans on"},{"key":"5747_CR28","doi-asserted-by":"crossref","unstructured":"Lewis M, Schubert T, and Becker B (2007) \"Multithreaded SAT solving,\" in Proc Design Automation Conference. ASP-DAC'07. Asia and South Pacific, pp. 926\u2013931: IEEE","DOI":"10.1109\/ASPDAC.2007.358108"},{"issue":"11","key":"5747_CR29","doi-asserted-by":"publisher","first-page":"1767","DOI":"10.1109\/TCAD.2011.2157693","volume":"30","author":"KY Liao","year":"2011","unstructured":"Liao KY, Chang CY, Li JCM (2011) A parallel test pattern generation algorithm to meet multiple quality objectives. IEEE Trans Comput-Aided Des Integrated Circ Syst 30(11):1767\u20131772","journal-title":"IEEE Trans Comput-Aided Des Integrated Circ Syst"},{"key":"5747_CR30","doi-asserted-by":"crossref","unstructured":"Liao KY, Sheng-Chang H, and Li JCM (2013) \"GPU-based N-detect transition fault ATPG,\" in Proc. 2013 50th ACM\/EDAC\/IEEE design automation conference (DAC), pp. 1\u20138","DOI":"10.1145\/2463209.2488769"},{"issue":"2","key":"5747_CR31","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, Marques-Silva J (2016) Fast, flexible MUS enumeration. Constraints 21(2):223\u2013250","journal-title":"Constraints"},{"issue":"5","key":"5747_CR32","first-page":"518","volume":"15","author":"L Lingappan","year":"2007","unstructured":"Lingappan L, Jha NK (2007) Satisfiability-based automatic test program generation and design for testability for microprocessors, Very Large Scale Integration (VLSI) Systems. IEEE Trans on 15(5):518\u2013530","journal-title":"IEEE Trans on"},{"key":"5747_CR33","doi-asserted-by":"crossref","unstructured":"Marques-Silva J and Glass T (1999) \"Combinational equivalence checking using satisfiability and recursive learning,\" in Proc Design, Automation and Test in Europe Conference and Exhibition, pp. 145\u2013149: IEEE","DOI":"10.1145\/307418.307477"},{"issue":"5","key":"5747_CR34","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva JP, Sakallah KA (1999) GRASP: a search algorithm for propositional satisfiability. IEEE Trans Comput 48(5):506\u2013521","journal-title":"IEEE Trans Comput"},{"key":"5747_CR35","unstructured":"Micikevicius P (2012) \"GPU performance analysis and optimization,\" in GPU\u00a0Technology Conference (GTC'12), NVIDIA, vol. 84. Available:\u00a0 http:\/\/developer.download.nvidia.com\/GTC\/PDF\/GTC2012\/PresentationPDF\/S0514-GTC2012-GPU-Performance-Analysis.pdf"},{"key":"5747_CR36","first-page":"86","volume-title":"Hardware and software: verification and testing: 8th international Haifa verification conference, HVC 2012, Haifa, Israel, November 6\u20138, 2012","author":"A Morgado","year":"2013","unstructured":"Morgado A, Liffiton M, Marques-Silva J (2013) MaxSAT-based MCS enumeration. In: Biere A, Nahir A, Vos T (eds) Hardware and software: verification and testing: 8th international Haifa verification conference, HVC 2012, Haifa, Israel, November 6\u20138, 2012. Revised Selected Papers. Springer Berlin Heidelberg, Berlin, pp 86\u2013101"},{"key":"5747_CR37","doi-asserted-by":"crossref","unstructured":"Moskewicz MW, Madigan CF, Zhao Y, Zhang L, and Malik S (2001) \"Chaff: Engineering an efficient SAT solver,\" in Proc. 38th annual Design Automation Conference, pp. 530\u2013535: ACM","DOI":"10.1145\/378239.379017"},{"issue":"6","key":"5747_CR38","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis R, Oliveras A, Tinelli C (2006) Solving SAT and SAT modulo theories: from an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL (T). J ACM (JACM) 53(6):937\u2013977","journal-title":"J ACM (JACM)"},{"issue":"8","key":"5747_CR39","doi-asserted-by":"publisher","first-page":"741","DOI":"10.1109\/TSE.2016.2520468","volume":"42","author":"MA Noureddine","year":"2016","unstructured":"Noureddine MA, Zaraket FA (2016) Model checking software with first order logic specifications using AIG solvers. IEEE Trans Softw Eng 42(8):741\u2013763","journal-title":"IEEE Trans Softw Eng"},{"key":"5747_CR40","unstructured":"Novikov Y (2003) \"Local search for boolean relations on the basis of unit propagation,\" in Proc. of the conference on Design, Automation and Test in Europe-Volume 1, p. 10810: IEEE Computer Society"},{"key":"5747_CR41","unstructured":"NVIDIA (2015) CUDA C Programming Guide. Available: http:\/\/docs.nvidia.com\/cuda\/cuda-c-programming-guide\/"},{"issue":"5","key":"5747_CR42","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1109\/PGEC.1967.264743","volume":"EC-16","author":"JP Roth","year":"1967","unstructured":"Roth JP, Bouricius WG, Schneider PR (1967) Programmed algorithms to compute tests to detect and distinguish between failures in logic circuits. IEEE Trans Electron Comput EC-16(5):567\u2013580","journal-title":"IEEE Trans Electron Comput"},{"key":"5747_CR43","doi-asserted-by":"crossref","unstructured":"Safarpour S, Mangassarian H, Veneris A, Liffiton MH and Sakallah K (2007) \"Improved design debugging using maximum satisfiability,\" in Proc Formal Methods in Computer Aided Design, FMCAD'07, pp. 13\u201319: IEEE","DOI":"10.1109\/FMCAD.2007.4401977"},{"key":"5747_CR44","unstructured":"Shi J, Fey G, Drechsler R, Glowatz A, Hapke F and Schl\u00f6ffel J (2005) \"PASSAT: efficient SAT-based test pattern generation for industrial circuits,\" in Proc IEEE Computer Society Annual Symposium on VLSI, pp. 212\u2013217: IEEE"},{"issue":"10","key":"5747_CR45","doi-asserted-by":"publisher","first-page":"1606","DOI":"10.1109\/TCAD.2005.852031","volume":"24","author":"A Smith","year":"2005","unstructured":"Smith A, Veneris A, Ali MF, Viglas A (2005) Fault diagnosis and logic debugging using Boolean satisfiability. Comput-Aided Des Integrated Circ Syst, IEEE Trans on 24(10):1606\u20131621","journal-title":"Comput-Aided Des Integrated Circ Syst, IEEE Trans on"},{"key":"5747_CR46","unstructured":"Sohanghpurwala AA, Hassan MW and Athanas P \"Hardware accelerated SAT solvers\u2014a survey,\" Journal of Parallel and Distributed ComputingIEEE Des Test Comput"},{"issue":"8","key":"5747_CR47","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1145\/2517327.2442523","volume":"48","author":"B Wu","year":"2013","unstructured":"Wu B, Zhao Z, Zhang EZ, Jiang Y, Shen X (2013) Complexity analysis and algorithm design for reorganizing data to minimize non-coalesced memory accesses on gpu. ACM SIGPLAN Not 48(8):57\u201368","journal-title":"ACM SIGPLAN Not"},{"key":"5747_CR48","doi-asserted-by":"crossref","unstructured":"Xie H and Luo J (2016) \"An algorithm to compute minimal Unsatisfiable subsets for a decidable fragment of first-order formulas,\" in Proc. 2016 IEEE 28th international conference on tools with artificial intelligence (ICTAI), pp. 444\u2013451","DOI":"10.1109\/ICTAI.2016.0074"},{"key":"5747_CR49","doi-asserted-by":"crossref","unstructured":"Youness H, Ibraheim A, Moness M and Osama M (2015) \"An efficient implementation of ant colony optimization on GPU for the satisfiability problem,\" in Proc 2015 23rd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP), pp. 230\u2013235: IEEE","DOI":"10.1109\/PDP.2015.59"},{"key":"5747_CR50","unstructured":"Zhang H and Stickel ME (1996) \"An efficient algorithm for unit propagation,\" in Proc. of the Fourth International Symposium on Artificial Intelligence and Mathematics (AI-MATH\u201996). Florida, USA: Citeseer"}],"container-title":["Journal of Electronic Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10836-018-5747-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-018-5747-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-018-5747-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T17:56:34Z","timestamp":1751824594000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10836-018-5747-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,8,30]]},"references-count":50,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2018,10]]}},"alternative-id":["5747"],"URL":"https:\/\/doi.org\/10.1007\/s10836-018-5747-4","relation":{},"ISSN":["0923-8174","1573-0727"],"issn-type":[{"value":"0923-8174","type":"print"},{"value":"1573-0727","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,8,30]]},"assertion":[{"value":"26 January 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 August 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 August 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}