{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,27]],"date-time":"2024-03-27T23:46:14Z","timestamp":1711583174002},"reference-count":143,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2018,3,28]],"date-time":"2018-03-28T00:00:00Z","timestamp":1522195200000},"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":["Artif Intell Rev"],"published-print":{"date-parts":[[2019,12]]},"DOI":"10.1007\/s10462-018-9628-0","type":"journal-article","created":{"date-parts":[[2018,3,28]],"date-time":"2018-03-28T05:16:44Z","timestamp":1522214204000},"page":"2575-2601","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["A comprehensive study and analysis on SAT-solvers: advances, usages and achievements"],"prefix":"10.1007","volume":"52","author":[{"ORCID":"http:\/\/orcid.org\/0000-0001-9321-4005","authenticated-orcid":false,"given":"Sahel","family":"Alouneh","sequence":"first","affiliation":[]},{"given":"Sa\u2019ed","family":"Abed","sequence":"additional","affiliation":[]},{"given":"Mohammad H.","family":"Al Shayeji","sequence":"additional","affiliation":[]},{"given":"Raed","family":"Mesleh","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,3,28]]},"reference":[{"key":"9628_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla PA, Bjesse P, E\u00e9n N (2000) Symbolic reachability analysis based on sat-solvers. In: Proceedings of the 6th international conference on tools and algorithms for construction and analysis of systems: held as part of the European joint conferences on the theory and practice of software, ETAPS 2000. Springer, London, pp 411\u2013425","DOI":"10.1007\/3-540-46419-0_28"},{"key":"9628_CR2","doi-asserted-by":"crossref","unstructured":"Abed S, Mohamed OA, Yang Z, Sammane GA (2007) Integrating SAT with multiway decision graphs for efficient model checking. In: Proceedings of IEEE ICM\u201907. IEEE Press, Egypt, pp 129\u2013132","DOI":"10.1109\/ICM.2007.4497677"},{"key":"9628_CR3","volume-title":"Solvable cases of the decision problem","author":"W Ackermann","year":"1954","unstructured":"Ackermann W (1954) Solvable cases of the decision problem, 1st edn. North-Holland Publishing, North-Holland","edition":"1"},{"key":"9628_CR4","unstructured":"Aloul FA, Ramani A, Markov IL, Sakallah KA (2002) Pbs: a backtrack search pseudo Boolean solver. In: Symposium on the theory and applications of satisfiability testing (SAT), pp 346\u2013353"},{"issue":"4\u20135","key":"9628_CR5","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1016\/j.jfranklin.2006.01.003","volume":"343","author":"FA Aloul","year":"2006","unstructured":"Aloul FA (2006) Search techniques for sat-based Boolean optimization, modeling, simulation and applied optimization. J Franklin Inst 343(4\u20135):436\u2013447","journal-title":"J Franklin Inst"},{"key":"9628_CR6","doi-asserted-by":"crossref","unstructured":"Amla N, Du X, Kuehlmann A, Kurshan RP, Mcmillan KL (2005) An analysis of sat-based model checking techniques in an industrial environment. In: CHARME, pp 254\u2013268","DOI":"10.1007\/11560548_20"},{"key":"9628_CR7","unstructured":"Andraus ZS, Sakallah KA (2004) Automatic abstraction and verification of verilog models. In: Proceedings of the 41st annual design automation conference. ACM, New York, pp 218\u2013223"},{"key":"9628_CR8","unstructured":"Ans\u00f3tegui C, Bonet ML, Levy J (2009) Towards industrial-like random sat instances. In: Proceedings of the 21st international joint conference on artifical intelligence. Morgan Kaufmann Publishers Inc., San Francisco, pp 387\u2013392"},{"key":"9628_CR9","unstructured":"Arbelaez A, Codognet P (2013) A survey of parallel local search for sat. In: Theory, implementation, and applications of SAT technology. Workshop at JSAI 2013, pp 1\u20134"},{"issue":"4\u20135","key":"9628_CR10","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/s10732-006-7234-9","volume":"12","author":"J Argelich","year":"2006","unstructured":"Argelich J, Many\u00e0 F (2006) Exact MAX-SAT solvers for over-constrained problems. J Heuristics 12(4\u20135):375\u2013392","journal-title":"J Heuristics"},{"key":"9628_CR11","unstructured":"Arora R, Hsiao MS (2004) CNF formula simplification using implication reasoning. In: Proceedings of the high-level design validation and test workshop, ninth IEEE international. IEEE Computer Society, Washington, pp 129\u2013134"},{"key":"9628_CR12","doi-asserted-by":"crossref","unstructured":"Audemard G, Lagniez J-M, Simon L (2013) Improving glucose for incremental sat solving with assumptions: application to MUS extraction. In: International conference on theory and applications of satisfiability testing. Springer, pp 309\u2013317","DOI":"10.1007\/978-3-642-39071-5_23"},{"key":"9628_CR13","unstructured":"Audemard G, Simon L (2009) Predicting learnt clauses quality in modern sat solvers. In: Proceedings of the 21st international jont conference on artifical intelligence. Morgan Kaufmann Publishers Inc, San Francisco, pp 399\u2013404"},{"key":"9628_CR14","doi-asserted-by":"crossref","unstructured":"Audemard G, Simon L (2014) Lazy clause exchange policy for parallel SAT solvers. In: Proceedings of international conference on theory and applications of satisfiability testing\u2014SAT 2014\u201417th, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, pp 197\u2013205","DOI":"10.1007\/978-3-319-09284-3_15"},{"key":"9628_CR15","unstructured":"Bacchus F, Winter J (2003) Effective preprocessing with hyper-resolution and equality reduction. In: SAT, pp 341\u2013355"},{"key":"9628_CR16","unstructured":"Balint A, Belov A, Heule MJ, J\u00e4rvisalo M (2013) Solver and benchmark descriptions. In: Proceedings of SAT competition 2013, vol B-2013-1. Department of Computer Science Series of Publications, University of Helsinki, Helsinki"},{"key":"9628_CR17","unstructured":"Barrett C, Sebastiani R, Seshia S, Tinelli C (2009) Satisfiability modulo theories, frontiers in artificial intelligence and applications, vol 185, ch.\u00a026, IOS Press, pp 825\u2013885"},{"key":"9628_CR18","doi-asserted-by":"crossref","unstructured":"Bauer A, Pister M, Tautschnig M (2007) Tool-support for the analysis of hybrid systems and models. In: Proceedings of the conference on design, automation and test in Europe. EDA Consortium, San Jose, pp 924\u2013929","DOI":"10.1109\/DATE.2007.364411"},{"key":"9628_CR19","doi-asserted-by":"crossref","unstructured":"Becker B, Drechsler R, Eggersgl\u00fc S, Sauer M (2014) Recent advances in sat-based ATPG: non-standard fault models, multi constraints and optimization. In: Proceedings of the 9th international conference on design & technology of integrated systems in nanoscale era, DTIS 2014, Santorini, Greece, pp 1\u201310","DOI":"10.1109\/DTIS.2014.6850674"},{"key":"9628_CR20","doi-asserted-by":"crossref","unstructured":"Bentley B (2005) Validating a modern microprocessor. In: Proceedings of the 17th international conference on computer aided verification. Springer, Berlin, pp 2\u20134","DOI":"10.1007\/11513988_2"},{"key":"9628_CR21","doi-asserted-by":"crossref","unstructured":"Bhm M, Speckenmeyer E (1996) A fast parallel sat-solver-efficient workload balancing\u2019. In: Annals of mathematics and artificial intelligence, p 40","DOI":"10.1007\/BF02127976"},{"key":"9628_CR22","unstructured":"Biere A (2010) Lingeling, plingeling, picoSAT and precoSAT at SAT race 2010. Technical report 10\/1, Institute for formal models and verification, Johannes Kepler University"},{"key":"9628_CR23","unstructured":"Biere A (2015) AIGER format and toolbox. http:\/\/fmv.jku.at\/aiger\/"},{"key":"9628_CR24","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke EM, Fujita M, Zhu Y (1999) Symbolic model checking using sat procedures instead of BDDS, pp 317\u2013320","DOI":"10.21236\/ADA360973"},{"key":"9628_CR25","doi-asserted-by":"crossref","unstructured":"Bjesse P, Boralv A (2004) Dag-aware circuit compression for formal verification. In: Proceedings of the 2004 IEEE\/ACM international conference on computer-aided design. IEEE Computer Society, Washington, pp 42\u201349","DOI":"10.1109\/ICCAD.2004.1382541"},{"key":"9628_CR26","doi-asserted-by":"crossref","unstructured":"Bjesse P, Claessen K (2000) Sat-based verification without state space traversal. In: In formal methods in computer-aided design. Springer, pp 372\u2013389","DOI":"10.1007\/3-540-40922-X_23"},{"key":"9628_CR27","doi-asserted-by":"crossref","unstructured":"Bjesse P, Claessen K (2000) Sat-based verification without state space traversal. In: Proceedings of the third international conference on formal methods in computer-aided design. Springer, London, pp 372\u2013389","DOI":"10.1007\/3-540-40922-X_23"},{"key":"9628_CR28","doi-asserted-by":"publisher","first-page":"969","DOI":"10.1016\/S0167-8191(03)00068-1","volume":"29","author":"W Blochinger","year":"2003","unstructured":"Blochinger W, Sinz C, Kchlin W (2003) Parallel propositional satisfiability checking with distributed dynamic learning. Parallel Comput 29:969\u2013994","journal-title":"Parallel Comput"},{"key":"9628_CR29","doi-asserted-by":"crossref","unstructured":"Boppana V, Rajan SP, Takayama K, Fujita M (1999) Model checking based on sequential ATPG. In: Proceedings of the 11th international conference on computer aided verification. Springer, London, pp 418\u2013430","DOI":"10.1007\/3-540-48683-6_36"},{"issue":"4","key":"9628_CR30","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1016\/0747-7171(92)90009-S","volume":"14","author":"T Boy de la Tour","year":"1992","unstructured":"Boy de la Tour T (1992) An optimality result for clause form translation. J Symb Comput 14(4):283\u2013301","journal-title":"J Symb Comput"},{"key":"9628_CR31","doi-asserted-by":"crossref","unstructured":"Bozzano M, Bruttomesso R, Cimatti R, Junttila T, Rossum PV, Schulz S, Sebastiani R (2005) The mathsat 3 system. In: Automated deduction: proceedings of the 20th international conference, volume 3632 of Lecture notes in computer science. Springer, pp 315\u2013321","DOI":"10.1007\/11532231_23"},{"key":"9628_CR32","unstructured":"Bruttomesso R, Sharygina N (2009) OpenSMT 0.1"},{"key":"9628_CR33","doi-asserted-by":"crossref","unstructured":"Bryant RE, Kroening D, Ouaknine J, Seshia SA, Strichman O, Brady B (2007) Deciding bit-vector arithmetic with abstraction. In : Proceedings of the 13th international conference on tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 358\u2013372","DOI":"10.1007\/978-3-540-71209-1_28"},{"issue":"3","key":"9628_CR34","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant RE (1992) Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3):293\u2013318","journal-title":"ACM Comput Surv"},{"issue":"4","key":"9628_CR35","doi-asserted-by":"publisher","first-page":"604","DOI":"10.1145\/566385.566390","volume":"3","author":"RE Bryant","year":"2002","unstructured":"Bryant RE, Velev MN (2002) Boolean satisfiability with transitivity constraints. ACM Trans Comput Logic 3(4):604\u2013627","journal-title":"ACM Trans Comput Logic"},{"key":"9628_CR36","first-page":"470","volume-title":"Exploiting positive equality in a logic of equality with uninterpreted functions","author":"RE Bryant","year":"1999","unstructured":"Bryant RE, German S, Velev MN (1999) Exploiting positive equality in a logic of equality with uninterpreted functions. Springer, London, pp 470\u2013482"},{"key":"9628_CR37","unstructured":"Burch JR, Dill DL (1994) Automatic verification of pipelined microprocessor control. In: Proceedings of the 6th international conference on computer aided verification. Springer, London, pp 68\u201380"},{"key":"9628_CR38","unstructured":"Butler R, Lusk E (1992) User\u2019s guide to the p4 parallel programming system"},{"key":"9628_CR39","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/j.artint.2013.09.001","volume":"204","author":"S Cai","year":"2013","unstructured":"Cai S, Su K (2013) Local search for boolean satisfiability with configuration checking and subscore. Artif Intell 204:75\u201398. https:\/\/doi.org\/10.1016\/j.artint.2013.09.001","journal-title":"Artif Intell"},{"issue":"9\u201310","key":"9628_CR40","doi-asserted-by":"publisher","first-page":"1672","DOI":"10.1016\/j.artint.2011.03.003","volume":"175","author":"S Cai","year":"2011","unstructured":"Cai S, Su K, Sattar A (2011) Local search with edge weighting and configuration checking heuristics for minimum vertex cover. Artif Intell 175(9\u201310):1672\u20131696","journal-title":"Artif Intell"},{"key":"9628_CR41","doi-asserted-by":"crossref","unstructured":"Cai S, Su K (2011) Local search with configuration checking for sat. In: 23rd IEEE international conference on tools with artificial intelligence (ICTAI), pp 59\u201366","DOI":"10.1109\/ICTAI.2011.18"},{"key":"9628_CR42","doi-asserted-by":"crossref","unstructured":"Calabro C, Impagliazzo R, Paturi R (2010) On the exact complexity of evaluating quantified-CNF. In: IPEC, pp 50\u201359","DOI":"10.1007\/978-3-642-17493-3_7"},{"key":"9628_CR43","doi-asserted-by":"crossref","unstructured":"Chai D, Kuehlmann A (2003) A fast pseudo-boolean constraint solver. In: Proceedings of the 40th annual design automation conference. ACM, New York, pp 830\u2013835","DOI":"10.1145\/775832.776041"},{"key":"9628_CR44","doi-asserted-by":"crossref","unstructured":"Chambers B, Manolios P, Vroon D (2009) Faster sat solving with better CNF generation. In: Proceedings of the conference on design, automation and test in Europe, 3001 Leuven, Belgium. European Design and Automation Association, Belgium, pp 1590\u20131595","DOI":"10.1109\/DATE.2009.5090918"},{"key":"9628_CR45","doi-asserted-by":"crossref","unstructured":"Chauhan P, Clarke EM, Kukula JH, Sapra S, Veith H, Wang D (2002) Automated abstraction refinement for model checking large state spaces using sat based conflict analysis. In: Proceedings of the 4th international conference on formal methods in computer-aided design. Springer, London, pp 33\u201351","DOI":"10.1007\/3-540-36126-X_3"},{"key":"9628_CR46","doi-asserted-by":"crossref","unstructured":"Chrabakh W, Wolski R (2003) GrADSAT: a parallel SAT solver for the grid","DOI":"10.1145\/1048935.1050188"},{"key":"9628_CR47","doi-asserted-by":"crossref","unstructured":"Chu G, Harwood A, Stuckey PJ (2009) Cache conscious data structures for Boolean satisfiability solvers. J Satisf Boolean Model Comput 6:99\u2013120","DOI":"10.3233\/SAT190064"},{"issue":"3","key":"9628_CR48","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis M, Putnam H (1960) A computing procedure for quantification theory. J ACM 7(3):201\u2013215","journal-title":"J ACM"},{"key":"9628_CR49","doi-asserted-by":"crossref","unstructured":"De Moura L, Bj\u00f8rner N (2008) Z3: an efficient smt solver. In: Proceedings of the theory and practice of software, 14th international conference on tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9628_CR50","unstructured":"Dixon HE, Ginsberg ML (2002) Inference methods for a pseudo-Boolean satisfiability solver. In: Eighteenth national conference on artificial intelligence. American Association for Artificial Intelligence, Menlo Park, pp 635\u2013640"},{"issue":"7","key":"9628_CR51","doi-asserted-by":"publisher","first-page":"1329","DOI":"10.1109\/TCAD.2008.923107","volume":"27","author":"R Drechsler","year":"2008","unstructured":"Drechsler R, Eggersgluss S, Fey G, Glowatz A, Hapke F, Schloeffel J, Tille D (2008) On acceleration of sat-based ATPG for industrial designs. Trans Comput Aided Des Integ Circuit Syst 27(7):1329\u20131333","journal-title":"Trans Comput Aided Des Integ Circuit Syst"},{"key":"9628_CR52","doi-asserted-by":"publisher","DOI":"10.1007\/978-90-481-2360-5","volume-title":"Test pattern generation using Boolean proof engines","author":"R Drechsler","year":"2009","unstructured":"Drechsler R, Eggersgl S, Fey G, Tille D (2009) Test pattern generation using Boolean proof engines, 1st edn. Springer, London","edition":"1"},{"key":"9628_CR53","doi-asserted-by":"crossref","unstructured":"Een N, Mishchenko A, S\u00f6rensson N (2007) Applying logic synthesis for speeding up sat. In: Proceedings of the 10th international conference on Theory and applications of satisfiability testing. Springer, Berlin, pp 272\u2013286","DOI":"10.1007\/978-3-540-72788-0_26"},{"key":"9628_CR54","doi-asserted-by":"crossref","unstructured":"Eggersgluss S, Tille D, Drechsler R (2009) Speeding up sat-based ATPG using dynamic clause activation. In: Asian test symposium. ATS \u201909, pp 177\u2013182","DOI":"10.1109\/ATS.2009.26"},{"key":"9628_CR55","doi-asserted-by":"crossref","unstructured":"Ehlers T, Nowotka D, Sieweck P (2014) Communication in massively-parallel sat solving. In: 2014 IEEE 26th international conference on tools with artificial intelligence, pp 709\u2013716","DOI":"10.1109\/ICTAI.2014.111"},{"key":"9628_CR56","first-page":"1","volume":"2","author":"N En","year":"2006","unstructured":"En N, Srensson N (2006) Translating pseudo-Boolean constraints into sat. J Satisf Boolean Model Comput 2:1\u201326","journal-title":"J Satisf Boolean Model Comput"},{"key":"9628_CR57","unstructured":"En N, Srensson N (2004) An extensible sat-solver. In: Giunchiglia E, Tacchella A (eds) Theory and applications of satisfiability testing. Lecture Notes in Computer Science, vol 2919. Springer, Berlin, pp 502\u2013518"},{"key":"9628_CR58","unstructured":"Forman SL, Segre A (2002) Nagsat: a randomized, complete, parallel solver for 3-sat. In: Fifth international symposium on the theory and applications of satisfiability testing"},{"key":"9628_CR59","unstructured":"Formisano A, Vella F (2014) On multiple learning schemata in conflict driven solvers. In: Proceedings of the 15th Italian conference on theoretical computer science, Perugia, Italy, pp 133\u2013146"},{"key":"9628_CR60","unstructured":"Freeman JW (1995) Improvements to propositional satisfiability search algorithms, Philadelphia, uMI Order No. GAX95-32175"},{"key":"9628_CR61","first-page":"209","volume":"1","author":"M Frnzle","year":"2007","unstructured":"Frnzle M, Herde C, Teige T, Ratschan S, Schubert T (2007) Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. J Satisf Boolean Model Comput 1:209\u2013236","journal-title":"J Satisf Boolean Model Comput"},{"key":"9628_CR62","unstructured":"Fu YMZ, Malik S (2004) New features of the SAT\u201904 versions of zChaff"},{"key":"9628_CR63","unstructured":"Ganai MK, Aziz A (2002) Improved sat-based bounded reachability analysis. In: Proceedings of the 2002 Asia and South Pacific design automation conference. IEEE Computer Society, Washington, pp 729\u2013735"},{"key":"9628_CR64","first-page":"71","volume":"6","author":"L Gil","year":"2008","unstructured":"Gil L, Flores P, Silveira LM (2008) PMSat: a parallel version of MiniSAT. J Satisf Boolean Model Comput 6:71\u201398","journal-title":"J Satisf Boolean Model Comput"},{"key":"9628_CR65","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1023\/A:1015071400913","volume":"28","author":"E Giunchiglia","year":"2002","unstructured":"Giunchiglia E, Tacchella A, Giunchiglia F (2002) Sat-based decision procedures for classical modal logics. J Autom Reason 28:143\u2013171","journal-title":"J Autom Reason"},{"key":"9628_CR66","doi-asserted-by":"crossref","unstructured":"Giunchiglia E, Maratea M, Tacchella O (2003) Look-ahead versus look-back techniques in a modern sat solver. In: SAT03\u2014Sixth international conference on theory and applications of satisfiability testing, Portofino","DOI":"10.1007\/978-3-540-45193-8_64"},{"issue":"3","key":"9628_CR67","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1023\/A:1022988809947","volume":"22","author":"A Goel","year":"2003","unstructured":"Goel A, Sajid K, Zhou H, Aziz A, Singhal V (2003) Bdd based procedures for a theory of equality with uninterpreted functions. Form Methods Syst Des 22(3):205\u2013224","journal-title":"Form Methods Syst Des"},{"issue":"12","key":"9628_CR68","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. Discrete Appl Math 155(12):1549\u20131561","journal-title":"Discrete Appl Math"},{"key":"9628_CR69","doi-asserted-by":"crossref","unstructured":"Hamadi Y, Jabbour S, Sa\u00efs L (2009) Learning for dynamic subsumption. In: Proceedings of the 2009 21st IEEE international conference on tools with artificial intelligence. IEEE Computer Society, Washington, pp 328\u2013335","DOI":"10.1109\/ICTAI.2009.22"},{"key":"9628_CR70","unstructured":"Heule MJ, Van Maaren H (2008) Parallel sat solving using bit-level operations. J Satisf Boolean Model Comput 99\u2013116"},{"key":"9628_CR71","unstructured":"Holldobler S, Manthey N, Nguyen VH, Stecklina J, Steinke P (2011) A short overview on modern parallel sat-solvers. In: International conference on advanced computer science and information system (ICACSIS), pp 201\u2013206"},{"key":"9628_CR72","unstructured":"Hoos H (1999) On the run-time behaviour of stochastic local search algorithms for sat. In: Sixteenth national conference on artificial intelligence and the eleventh innovative applications of artificial intelligence conference innovative applications of artificial intelligence. American Association for Artificial Intelligence, Menlo Park, pp 661\u2013666"},{"key":"9628_CR73","unstructured":"Hoos HH (2002) An adaptive noise mechanism for walksat. In: Eighteenth national conference on artificial intelligence. American Association for Artificial Intelligence, Menlo Park, pp 655\u2013660"},{"issue":"4","key":"9628_CR74","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1023\/A:1006350622830","volume":"24","author":"HH Hoos","year":"2000","unstructured":"Hoos HH, St\u00fctzle T (2000) Local search algorithms for sat: an empirical evaluation. J Autom Reason 24(4):421\u2013481. https:\/\/doi.org\/10.1023\/A:1006350622830","journal-title":"J Autom Reason"},{"issue":"1\/2","key":"9628_CR75","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1504\/IJCCBS.2012.045074","volume":"3","author":"KA Hoque","year":"2012","unstructured":"Hoque KA, Mohamed OA, Abed S, Boukadoum M (2012) Mdg-sat: an automated methodology for efficient safety checking. Int J Crit Comput Based Syst 3(1\/2):4\u201325","journal-title":"Int J Crit Comput Based Syst"},{"issue":"5","key":"9628_CR76","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/s10009-011-0193-y","volume":"13","author":"D Ishii","year":"2011","unstructured":"Ishii D, Ueda K, Hosobe H (2011) An interval-based sat modulo ode solver for model checking nonlinear hybrid systems. Int J Softw Tools Technol Transf 13(5):449\u2013461","journal-title":"Int J Softw Tools Technol Transf"},{"key":"9628_CR77","doi-asserted-by":"crossref","unstructured":"Ivan T (2013) An efficient hardware implementation of a sat problem solver on FPGA. In: Proceedings\u201416th Euromicro conference on digital system design, DSD 2013. Universit de Montral, Montral, Department d\u2019informatique et recherche oprationnelle, Montral, pp 209\u2013216","DOI":"10.1109\/DSD.2013.31"},{"key":"9628_CR78","unstructured":"Jackson P, Sheridan D (2004) The optimality of a fast CNF conversion and its use with sat. APES Research Group. Technical report APES-82-2004"},{"key":"9628_CR79","doi-asserted-by":"crossref","unstructured":"Jackson P, Sheridan D (2005) Clause form conversions for Boolean circuits. In: Proceedings of the 7th international conference on theory and applications of satisfiability testing. Springer, Berlin, pp 183\u2013198","DOI":"10.1007\/11527695_15"},{"issue":"1","key":"9628_CR80","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1609\/aimag.v33i1.2395","volume":"33","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo M, Le Berre D, Roussel O, Simon L (2012) The international sat solver competitions. AI Mag 33(1):89\u201392","journal-title":"AI Mag"},{"key":"9628_CR81","doi-asserted-by":"crossref","unstructured":"Jing M, Yin W, Chen G, Zhou D (2009) Enhance sat conflict analysis for model checking. In: IEEE 8th international conference on ASIC, 2009, ASICON \u201909, pp 686\u2013689","DOI":"10.1109\/ASICON.2009.5351339"},{"key":"9628_CR82","unstructured":"Jin H, Somenzi F (2006) Strong conflict analysis for propositional satisfiability. In Proceedings of the conference on design, automation and test in Europe, 3001 Leuven, Belgium. European Design and Automation Association, Belgium, pp 818\u2013823"},{"issue":"1","key":"9628_CR83","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s10817-005-1970-7","volume":"34","author":"B Jurkowiak","year":"2005","unstructured":"Jurkowiak B, Li CM, Utard G (2005) A parallelization scheme based on work stealing for a class of sat solvers. J Autom Reason 34(1):73\u2013101","journal-title":"J Autom Reason"},{"key":"9628_CR84","unstructured":"Kaivola R, O\u2019Leary J, Melham T (2013) Relational STE and theorem proving for formal verification of industrial circuit designs. In: Proceedings of the 2013 international conference on formal methods in computer-aided design, formal methods in computer-aided design (FMCAD). Springer, London, pp 97\u2013104"},{"key":"9628_CR85","doi-asserted-by":"crossref","unstructured":"Korovin K (2008) iProver\u2014an instantiation-based theorem prover for first-order logic (system description). In: Proceedings of the 4th international joint conference on automated reasoning. Springer, Berlin, pp 292\u2013298","DOI":"10.1007\/978-3-540-71070-7_24"},{"issue":"12","key":"9628_CR86","doi-asserted-by":"publisher","first-page":"2778","DOI":"10.1093\/ietfec\/e90-a.12.2778","volume":"90","author":"H Kozawa","year":"2007","unstructured":"Kozawa H, Hamaguchi K, Kashiwabara T (2007) Satisfiability checking for logic with equality and uninterpreted functions under equivalence constraints. IEICE Trans Fundam Electron Commun Comput Sci 90(12):2778\u20132789","journal-title":"IEICE Trans Fundam Electron Commun Comput Sci"},{"key":"9628_CR87","doi-asserted-by":"crossref","unstructured":"Kroening D, Leroux J, Rmmer P (2010) Interpolating quantifier-free presburger arithmetic. In: Fermller C, Voronkov A (eds) Logic for programming, artificial intelligence, and reasoning. Lecture Notes in Computer Science, vol 6397. Springer, Berlin, pp 489\u2013503","DOI":"10.1007\/978-3-642-16242-8_35"},{"key":"9628_CR88","doi-asserted-by":"crossref","unstructured":"Larrabee T (1989) Efficient generation of test patterns using boolean difference. In: Test conference, proceedings. Meeting the tests of time, international, pp 795\u2013801","DOI":"10.1109\/TEST.1989.82368"},{"key":"9628_CR89","unstructured":"Li CM, Huang WQ (2005) Diversification and determinism in local search for satisfiability. In: Proceedings of the 8th international conference on theory and applications of satisfiability testing, SAT\u201905, pp 158\u2013172"},{"key":"9628_CR90","unstructured":"Li CM, Wei W, Zhang H (2007) Combining adaptive noise and look-ahead in local search for sat. In: Proceedings of the 10th international conference on theory and applications of satisfiability testing. Springer, Berlin, pp 121\u2013133"},{"key":"9628_CR91","unstructured":"Lierler Y (2010) Sat-based answer set programming. Ph.D. dissertation, Department of Computer Sciences, The University of Texas at Austin, Austin"},{"issue":"1","key":"9628_CR92","first-page":"745","volume":"53","author":"M Lindauer","year":"2015","unstructured":"Lindauer M, Hoos HH, Hutter F, Schaub T (2015) Autofolio: an automatically configured algorithm selector. J Artif Int Res 53(1):745\u2013778","journal-title":"J Artif Int Res"},{"key":"9628_CR93","doi-asserted-by":"crossref","unstructured":"Lin F, Zhao Y (2004) Assat: computing answer sets of a logic program by sat solvers. In: Artificial intelligence, nonmonotonic reasoning, vol. 157(1\u20132), pp 115\u2013137. http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0004370204000578","DOI":"10.1016\/j.artint.2004.04.004"},{"key":"9628_CR94","doi-asserted-by":"crossref","unstructured":"Liu L, Kong W, Ando T, Yatsu H, Fukuda A (2013) A survey of acceleration techniques for SMT-based bounded model checking In: International conference on computer sciences and applications (CSA), pp 554\u2013559","DOI":"10.1109\/CSA.2013.135"},{"key":"9628_CR95","first-page":"1","volume":"99","author":"C Luo","year":"2014","unstructured":"Luo C, Cai S, Su K, Wu W (2014) Clause states based configuration checking in local search for satisfiability. IEEE Trans Cybern 99:1\u20131","journal-title":"IEEE Trans Cybern"},{"key":"9628_CR96","doi-asserted-by":"crossref","unstructured":"Luo C, Cai S, Wu W, Su K (2014) Double configuration checking in stochastic local search for satisfiability. In: Proceedings of the twenty-eighth AAAI conference on artificial intelligence, pp 2703\u20132709 (in press)","DOI":"10.1609\/aaai.v28i1.9110"},{"key":"9628_CR97","doi-asserted-by":"crossref","unstructured":"Manolios P, Vroon D (2007) Efficient circuit to cnf conversion. In: Proceedings of the 10th international conference on Theory and applications of satisfiability testing. Springer, Berlin, pp 4\u20139","DOI":"10.1007\/978-3-540-72788-0_3"},{"key":"9628_CR98","unstructured":"Manthey N (2011) Solver submission of RISS 1.0 to the sat competition 2011. SAT Competition"},{"key":"9628_CR99","doi-asserted-by":"crossref","first-page":"57","DOI":"10.15388\/Informatica.2010.273","volume":"21","author":"F Mari\u0107","year":"2010","unstructured":"Mari\u0107 F, Jani\u010di\u0107 P (2010) Formal correctness proof for dpll procedure. Informatica 21:57\u201378","journal-title":"Informatica"},{"key":"9628_CR100","unstructured":"Marques R (2013) Parallel sat solver. Universidade Tcnica de Lisboa"},{"key":"9628_CR101","doi-asserted-by":"crossref","unstructured":"Marques-Silva JP, Sakallah KA (2000) Boolean satisfiability in electronic design automation. In: Proceedings of the 37th annual design automation conference. ACM, New York, pp 675\u2013680","DOI":"10.1145\/337292.337611"},{"issue":"48","key":"9628_CR102","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"5","author":"J Marques-Silva","year":"1999","unstructured":"Marques-Silva J, Sakallah K (1999) GRASP: a search algorithm for propositional satisfiability. IEEE Trans Comput 5(48):506\u2013521","journal-title":"IEEE Trans Comput"},{"key":"9628_CR103","doi-asserted-by":"crossref","unstructured":"Mcmillan KL, Kuehlmann A, Sagiv M (2009) Generalizing dpll to richer logics. In: Proceedings of the 21st international conference on computer aided verification. Springer, Berlin, pp 462\u2013476","DOI":"10.1007\/978-3-642-02658-4_35"},{"key":"9628_CR104","doi-asserted-by":"crossref","unstructured":"McMillan KL (2002) Applying sat methods in unbounded symbolic model checking. In: Proceedings of the 14th international conference on computer aided verification. Springer, London, pp 250\u2013264","DOI":"10.1007\/3-540-45657-0_19"},{"key":"9628_CR105","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer aided verification. Lecture Notes in Computer Science","author":"KL Mcmillan","year":"2003","unstructured":"Mcmillan KL (2003) Interpolation and sat-based model checking. In: Hunt J, Warren A, Somenzi F (eds) Computer aided verification. Lecture Notes in Computer Science, vol 2725. Springer, Berlin, pp 1\u201313"},{"key":"9628_CR106","doi-asserted-by":"crossref","unstructured":"Mishchenko A, Chatterjee S, Brayton R (2006) Dag-aware aig rewriting a fresh look at combinational logic synthesis. In: Proceedings of the 43rd annual design automation conference. ACM, New York, pp 532\u2013535","DOI":"10.1145\/1146909.1147048"},{"key":"9628_CR107","doi-asserted-by":"crossref","unstructured":"Mony H, Baumgartner J, Paruthi V, Kanzelman R, Kuehlmann A (2004) Scalable automated verification via expert-system guided transformations. In: Hu A, Martin A (eds) FMCAD, Lecture Notes in Computer Science, vol 3312. Springer, Berlin, pp 159\u2013173","DOI":"10.1007\/978-3-540-30494-4_12"},{"key":"9628_CR108","doi-asserted-by":"crossref","unstructured":"Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient sat solver. In: Annual ACM IEEE design automation conference. ACM, pp 530\u2013535","DOI":"10.1145\/378239.379017"},{"key":"9628_CR109","unstructured":"Nadel A (2002) The jerusat sat solver. Master\u2019s thesis, Hebrew University of Jerusalem"},{"key":"9628_CR110","first-page":"449","volume-title":"SAT-enhanced mizar proof checking","author":"A Naumowicz","year":"2014","unstructured":"Naumowicz A (2014) SAT-enhanced mizar proof checking. Springer, Berlin, pp 449\u2013452"},{"key":"9628_CR111","doi-asserted-by":"crossref","unstructured":"Ogawa M, Khanh T (2013) Sat and SMT: their algorithm designs and applications. In: Software engineering conference (APSEC), 20th Asia-Pacific, vol\u00a02, pp 83\u201384","DOI":"10.1109\/APSEC.2013.118"},{"key":"9628_CR112","first-page":"191","volume":"2","author":"YB Olivier Bailleux","year":"2006","unstructured":"Olivier Bailleux YB, Roussel O (2006) A translation of pseudo Boolean constraints to sat. J Satisf Boolean Model Comput 2:191\u2013200","journal-title":"J Satisf Boolean Model Comput"},{"key":"9628_CR113","doi-asserted-by":"crossref","unstructured":"Pipatsrisawat K, Darwiche A (2007) A lightweight component caching scheme for satisfiability solvers. In: Proceedings of 10th international conference on theory and applications of satisfiability testing (SAT), pp 294\u2013299","DOI":"10.1007\/978-3-540-72788-0_28"},{"key":"9628_CR114","doi-asserted-by":"crossref","unstructured":"Pipatsrisawat K, Darwiche A (2009) On the power of clause-learning sat solvers with restarts. In: Proceedings of the 15th international conference on principles and practice of constraint programming. Springer, Berlin, pp 654\u2013668","DOI":"10.1007\/978-3-642-04244-7_51"},{"issue":"2","key":"9628_CR115","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"MR Prasad","year":"2005","unstructured":"Prasad MR, Biere A, Gupta A (2005) A survey of recent advances in sat-based formal verification. Int J Softw Tools Technol Transf 7(2):156\u2013173","journal-title":"Int J Softw Tools Technol Transf"},{"key":"9628_CR116","unstructured":"Reimer S, Sauer M, Schubert T, Becker B (2014) Using MAXBMC for pareto-optimal circuit initialization. In: Design, automation and test in Europe conference and exhibition (DATE), pp 1\u20136"},{"key":"9628_CR117","doi-asserted-by":"crossref","unstructured":"Rodrguez Vega M (2014) Analyzing toys models of arabidopsis and drosphila using z3 SMT-lib, vol 9118, pp 13\u201315","DOI":"10.1117\/12.2050071"},{"key":"9628_CR118","volume-title":"Efficient algorithms for clause-learning sat solvers","author":"L Ryan","year":"2004","unstructured":"Ryan L (2004) Efficient algorithms for clause-learning sat solvers. Simon Fraser University, Burnaby"},{"key":"9628_CR119","unstructured":"Selman B, Kautz HA, Cohen B (1994) Noise strategies for improving local search. In: Proceedings of the eleventh national conference on artificial intelligence (AAAI-94), pp 337\u2013343"},{"key":"9628_CR120","unstructured":"Selman B, Levesque H, Mitchell D (1992) A new method for solving hard satisfiability problems. In: Proceedings of the tenth national conference on artificial intelligence, pp 440\u2013446 (in press)"},{"key":"9628_CR121","doi-asserted-by":"crossref","unstructured":"Sheeran M, Singh S, St\u00e5lmarck G (2000) Checking safety properties using induction and a sat-solver. In: Proceedings of the third international conference on formal methods in computer-aided design. Springer, London, pp 108\u2013125","DOI":"10.1007\/3-540-40922-X_8"},{"key":"9628_CR122","first-page":"165","volume":"2","author":"HM Sheini","year":"2006","unstructured":"Sheini HM, Sakallah KA (2006) Pueblo: a hybrid pseudo-Boolean sat solver. J Satisf Boolean Model Comput 2:165\u2013189","journal-title":"J Satisf Boolean Model Comput"},{"key":"9628_CR123","doi-asserted-by":"crossref","unstructured":"Shtrichman O (2001) Pruning techniques for the sat-based bounded model checking problem. In: Proceedings of the 11th IFIP WG 10.5 advanced research working conference on correct hardware design and verification methods. Springer, London, pp 58\u201370","DOI":"10.1007\/3-540-44798-9_4"},{"key":"9628_CR124","unstructured":"Sorensson N, Een N (2005) Minisat v1.13\u2014a SAT solver with conflict-clause minimization. In: Eighth international conference on theory and applications of satisfiability testing (SAT 2005), vol 3569. Springer, St. Andrews"},{"key":"9628_CR125","unstructured":"Srensson N (2008) Effective sat solving. Ph.D. dissertation, Department of Computer Science and Engineering Chalmers University of Technology and University of Gothenburg SE-412 96, Gteborg, Sweden"},{"key":"9628_CR126","unstructured":"Subbarayan S, Pradhan DK (2004) Niver: non increasing variable elimination resolution for preprocessing sat instances. In: Proceedings of the 7th international conference on theory and applications of satisfiability testing (SAT). Springer, pp 276\u2013291"},{"key":"9628_CR127","unstructured":"The International SAT Competitions: SAT competition 2014, experiments: parallel, random SAT track: solver configurations: pprobSAT details. http:\/\/satcompetition.org\/edacc\/sc14\/experiment\/29\/solver-configurations\/1561"},{"key":"9628_CR128","first-page":"115","volume":"Part II","author":"GS Tseitin","year":"1968","unstructured":"Tseitin GS (1968) On the complexity of derivations in the propositional calculus. Stud Math Math Logic Part II:115\u2013125","journal-title":"Stud Math Math Logic"},{"issue":"1","key":"9628_CR129","first-page":"19","volume":"29","author":"T Tsuchiya","year":"2012","unstructured":"Tsuchiya T (2012) Model checking that uses satisfiability solving. Comput Softw 29(1):19\u201329","journal-title":"Comput Softw"},{"key":"9628_CR130","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1016\/j.entcs.2008.12.089","volume":"225","author":"O Tveretina","year":"2009","unstructured":"Tveretina O, Wesselink W (2009) Eufdpll\u2014a tool to check satisfiability of equality logic formulas. Electron Not Theor Comput Sci 225:405\u2013420","journal-title":"Electron Not Theor Comput Sci"},{"key":"9628_CR131","doi-asserted-by":"crossref","unstructured":"Velev MN (2004) Efficient translation of Boolean formulas to CNF in formal verification of microprocessors. In: Proceedings of the 2004 Asia and South Pacific design automation conference. IEEE Press, Piscataway, pp 310\u2013315","DOI":"10.1109\/ASPDAC.2004.1337587"},{"key":"9628_CR132","unstructured":"Velev MN (2004) Using automatic case splits and efficient CNF translation to guide a sat solver when formally verifying out-of-order processors. In: Artificial intelligence and mathematics (AIMATH \u201904), pp 242\u2013254"},{"key":"9628_CR133","doi-asserted-by":"crossref","unstructured":"Vizel Y, Grumberg O (2009) Interpolation-sequence based model checking. In: FMCAD, pp 1\u20138","DOI":"10.1109\/FMCAD.2009.5351148"},{"key":"9628_CR134","doi-asserted-by":"crossref","unstructured":"Vizel Y, Weissenbacher G, Malik S (2015) Boolean satisfiability solvers and their applications in model checking. In: Proceedings of the IEEE, vol 99, pp 1\u201315","DOI":"10.1109\/JPROC.2015.2455034"},{"key":"9628_CR135","doi-asserted-by":"crossref","unstructured":"Wieringa S, Niemenmaa M, Heljanko K (2009) Tarmo: a framework for parallelized bounded model checking. In: Brim L, van\u00a0der Pol J (eds) Proceedings of the 8th international workshop on parallel and distributed methods in verification (PDMC\u201909), electronic proceedings in theoretical computer science (EPTCS), vol\u00a014 pp 62\u201376","DOI":"10.4204\/EPTCS.14.5"},{"key":"9628_CR136","doi-asserted-by":"crossref","unstructured":"Wintersteiger CM, Hamadi Y, Moura L (2009) A concurrent Portfolio approach to SMT solving. In: Proceedings of the 21st international conference on computer aided verification. Springer, Berlin, pp 715\u2013720","DOI":"10.1007\/978-3-642-02658-4_60"},{"key":"9628_CR137","unstructured":"Wu CY, Wu CA, Lai CY, Huang CY (2013) A counterexample-guided interpolant generation algorithm for sat-based model checking. In: Design automation conference (DAC), 2013 50th ACM\/EDAC\/IEEE, pp 1\u20136"},{"issue":"1","key":"9628_CR138","first-page":"565","volume":"32","author":"L Xu","year":"2008","unstructured":"Xu L, Hutter F, Hoos HH, Leyton-Brown K (2008) Satzilla: Portfolio-based algorithm selection for sat. J Artif Int Res 32(1):565\u2013606","journal-title":"J Artif Int Res"},{"issue":"1\/2","key":"9628_CR139","doi-asserted-by":"publisher","first-page":"19","DOI":"10.14257\/astl.2014.48.04","volume":"48","author":"T Yoo","year":"2014","unstructured":"Yoo T, Kim S, Yeom Y, Kang J (2014) A study of the parallelization of hybrid sat solver using cuda. Adv Sci Technol Lett 48(1\/2):19\u201324","journal-title":"Adv Sci Technol Lett"},{"key":"9628_CR140","doi-asserted-by":"crossref","unstructured":"Zhang H (1997) Sato: an efficient propositional prover. In: Proceedings of the 14th international conference on automated deduction. Springer, London, pp 272\u2013275","DOI":"10.1007\/3-540-63104-6_28"},{"key":"9628_CR141","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1006\/jsco.1996.0030","volume":"21","author":"H Zhang","year":"1996","unstructured":"Zhang H, Bonacina MP, Paola M, Bonacina HJ (1996) Psato: a distributed propositional prover and its application to quasigroup problems. J Symb Comput 21:543\u2013560","journal-title":"J Symb Comput"},{"key":"9628_CR142","unstructured":"Zhang L, Madigan CF, Moskewicz MH, Malik S (2001) Efficient conflict driven learning in a Boolean satisfiability solver. In: Proceedings of the 2001 IEEE\/ACM international conference on computer-aided design. IEEE Press, Piscataway, pp 279\u2013285"},{"key":"9628_CR143","doi-asserted-by":"crossref","unstructured":"Zhao W, Wu W (2009) Asig: an all-solution sat solver for CNF formulas. In: 11th IEEE international conference on computer-aided design and computer graphics, CAD\/Graphics \u201909, pp 508\u2013513","DOI":"10.1109\/CADCG.2009.5246850"}],"container-title":["Artificial Intelligence Review"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10462-018-9628-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10462-018-9628-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10462-018-9628-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,17]],"date-time":"2022-08-17T04:34:00Z","timestamp":1660710840000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10462-018-9628-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,3,28]]},"references-count":143,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,12]]}},"alternative-id":["9628"],"URL":"https:\/\/doi.org\/10.1007\/s10462-018-9628-0","relation":{},"ISSN":["0269-2821","1573-7462"],"issn-type":[{"value":"0269-2821","type":"print"},{"value":"1573-7462","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,3,28]]},"assertion":[{"value":"28 March 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}