{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:18:08Z","timestamp":1781075888027,"version":"3.54.1"},"reference-count":71,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"Hassan Youness"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2020]]},"DOI":"10.1109\/access.2020.2999382","type":"journal-article","created":{"date-parts":[[2020,6,2]],"date-time":"2020-06-02T20:38:46Z","timestamp":1591130326000},"page":"102920-102934","source":"Crossref","is-referenced-by-count":10,"title":["An Effective SAT Solver Utilizing ACO Based on Heterogenous Systems"],"prefix":"10.1109","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2672-132X","authenticated-orcid":false,"given":"Hassan","family":"Youness","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Muhammad","family":"Osama","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aziza","family":"Hussein","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mohammed","family":"Moness","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2643-0792","authenticated-orcid":false,"given":"Ammar Mostafa","family":"Hassan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref71","author":"yuen","year":"2019","journal-title":"Tough SAT project ToughSAT"},{"key":"ref70","year":"2019","journal-title":"NVIDIA's Next Generation CUDA Compute Architecture Kepler GK110"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1016\/j.matcom.2018.08.011"},{"key":"ref38","article-title":"Ant colony optimization","author":"wong","year":"2011"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24258-9_24"},{"key":"ref32","first-page":"18","article-title":"Predicting SAT solver performance on heterogeneous hardware","volume":"59","author":"newsham","year":"2019","journal-title":"Pragmatics of SAT"},{"key":"ref31","first-page":"435","article-title":"Parallel SAT-solving with OpenCL","author":"beckers","year":"2011","journal-title":"Proc of the IADIS Int Conf on Applied Computing"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/3290688.3290706"},{"key":"ref37","first-page":"163","article-title":"ACO algorithms for the traveling salesman problem","volume":"4","author":"st\u00fctzle","year":"1999","journal-title":"Evolutionary Algorithms in Engineering and Computer Science"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-739X(00)00042-X"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2019-1788"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24258-9_11"},{"key":"ref60","year":"2019","journal-title":"STL STD Vector"},{"key":"ref62","year":"2019","journal-title":"Thread Affinity Interface (Linux* and Windows*)"},{"key":"ref61","year":"2019","journal-title":"OpenMP in Visual C++"},{"key":"ref63","year":"0","journal-title":"CUDA C Programming Guide"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/HPCS.2010.5547116"},{"key":"ref64","year":"2019"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190063"},{"key":"ref65","author":"harris","year":"2019","journal-title":"Optimizing Parallel Reduction in CUDA"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1145\/321812.321815"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17462-0_8"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1109\/CCGRID.2018.00008"},{"key":"ref68","year":"2019","journal-title":"Intel"},{"key":"ref69","year":"2019","journal-title":"NVIDIA GeForce Titan Black"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2018.2791465"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2005.852031"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_5"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21581-0_32"},{"key":"ref21","volume":"185","author":"biere","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref24","first-page":"89","article-title":"The complexity of pure literal elimination","author":"johannsen","year":"2005","journal-title":"SAT"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_7"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190070"},{"key":"ref25","author":"moritz","year":"2010","journal-title":"Solving Satisfiability With Ant Colony Optimization and Genetic Algorithms"},{"key":"ref50","author":"maaren","year":"2014","journal-title":"The International SAT Competitions"},{"key":"ref51","first-page":"279","article-title":"Efficient conflict driven learning in a Boolean satisfiability solver","author":"zhang","year":"2001","journal-title":"IEEE\/ACM Int Conf Comput Aided Design (ICCAD) Dig Tech Papers"},{"key":"ref59","year":"2019","journal-title":"CURAND"},{"key":"ref58","year":"2019","journal-title":"CUDA C Programming Guide"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2010.270"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC.2009.65"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2018\/181"},{"key":"ref54","article-title":"DPLL with restarts linearly simulates CDCL","author":"bailleux","year":"2019"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_9"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_11"},{"key":"ref10","first-page":"414","article-title":"Replacing testing with formal verification in Intel Core i7 processor execution engine validation","author":"kaivola","year":"0"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1023\/B:AUSE.0000038938.10589.b9"},{"key":"ref40","author":"kirk","year":"2012","journal-title":"Programming Massively Parallel Processors A Hands-on Approach"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/HST.2018.8383918"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/APCCAS.2018.8605696"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v33i01.33011592"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1049\/cje.2019.01.004"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.vlsi.2018.10.009"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2019.2915317"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_10"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/11527695_22"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/TVLSI.2007.896908"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v33i01.33011452"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1088\/1757-899X\/537\/5\/052029"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180248"},{"key":"ref8","first-page":"104","article-title":"Efficient haplotype inference with Boolean satisfiability","author":"lynce","year":"2006","journal-title":"Proc Nat Conf Artif Intell"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2006.97"},{"key":"ref49","year":"2014","journal-title":"Discrete Mathematics and Theoretical Computer Science"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/HST.2018.8383892"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1109\/PDP.2015.59"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73445-1_26"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_42"},{"key":"ref47","article-title":"Boundary evolution algorithm for SAT-NP","author":"ai","year":"2018","journal-title":"arXiv 1903 01894"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2008.105"},{"key":"ref41","author":"sanders","year":"2010","journal-title":"CUDA by Example An Introduction to General-Purpose GPU Programming"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-739X(00)00043-1"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/99.660313"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6287639\/8948470\/09106795.pdf?arnumber=9106795","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,17]],"date-time":"2021-12-17T19:52:26Z","timestamp":1639770746000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9106795\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"references-count":71,"URL":"https:\/\/doi.org\/10.1109\/access.2020.2999382","relation":{},"ISSN":["2169-3536"],"issn-type":[{"value":"2169-3536","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]}}}