Advertisement

A comprehensive study and analysis on SAT-solvers: advances, usages and achievements

  • Sahel Alouneh
  • Sa’ed Abed
  • Mohammad H. Al Shayeji
  • Raed Mesleh
Article
  • 123 Downloads

Abstract

Boolean satisfiability (SAT) has been studied for the last twenty years. Advances have been made allowing SAT solvers to be used in many applications including formal verification of digital designs. However, performance and capacity of SAT solvers are still limited. From the practical side, many of the existing applications based on SAT solvers use them as blackboxes in which the problem is translated into a monolithic conjunctive normal form instance and then throw it to the SAT solver with no interaction between the application and the SAT solver. This paper presents a comprehensive study and analysis of the latest developments in SAT-solver and new approaches that used in branching heuristics, Boolean constraint propagation and conflict analysis techniques during the last two decade. In addition, the paper provides the most effective techniques in using SAT solvers as verification techniques, mainly model checkers, to enhance the SAT solver performance, efficiency and productivity. Moreover, the paper presents the remarkable accomplishments and the main challenges facing SAT-solver techniques and contrasts between different techniques according to their efficiency, algorithms, usage and feasibility.

Keywords

SAT-solvers CNF EUF Verification techniques BMC UMC 

References

  1. Abdulla PA, Bjesse P, Eén 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–425Google Scholar
  2. Abed S, Mohamed OA, Yang Z, Sammane GA (2007) Integrating SAT with multiway decision graphs for efficient model checking. In: Proceedings of IEEE ICM’07. IEEE Press, Egypt, pp 129–132Google Scholar
  3. Ackermann W (1954) Solvable cases of the decision problem, 1st edn. North-Holland Publishing, North-HollandzbMATHGoogle Scholar
  4. 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–353Google Scholar
  5. Aloul FA (2006) Search techniques for sat-based Boolean optimization, modeling, simulation and applied optimization. J Franklin Inst 343(4–5):436–447CrossRefzbMATHGoogle Scholar
  6. 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–268Google Scholar
  7. 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–223Google Scholar
  8. Ansótegui 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–392Google Scholar
  9. 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–4Google Scholar
  10. Argelich J, Manyà F (2006) Exact MAX-SAT solvers for over-constrained problems. J Heuristics 12(4–5):375–392CrossRefzbMATHGoogle Scholar
  11. 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–134Google Scholar
  12. 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–317Google Scholar
  13. 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–404Google Scholar
  14. 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—SAT 2014—17th, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, pp 197–205Google Scholar
  15. Bacchus F, Winter J (2003) Effective preprocessing with hyper-resolution and equality reduction. In: SAT, pp 341–355Google Scholar
  16. Balint A, Belov A, Heule MJ, Järvisalo 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, HelsinkiGoogle Scholar
  17. Barrett C, Sebastiani R, Seshia S, Tinelli C (2009) Satisfiability modulo theories, frontiers in artificial intelligence and applications, vol 185, ch. 26, IOS Press, pp 825–885Google Scholar
  18. 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–929Google Scholar
  19. Becker B, Drechsler R, Eggersglü 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–10Google Scholar
  20. Bentley B (2005) Validating a modern microprocessor. In: Proceedings of the 17th international conference on computer aided verification. Springer, Berlin, pp 2–4Google Scholar
  21. Bhm M, Speckenmeyer E (1996) A fast parallel sat-solver-efficient workload balancing’. In: Annals of mathematics and artificial intelligence, p 40Google Scholar
  22. Biere A (2010) Lingeling, plingeling, picoSAT and precoSAT at SAT race 2010. Technical report 10/1, Institute for formal models and verification, Johannes Kepler UniversityGoogle Scholar
  23. Biere A (2015) AIGER format and toolbox. http://fmv.jku.at/aiger/
  24. Biere A, Cimatti A, Clarke EM, Fujita M, Zhu Y (1999) Symbolic model checking using sat procedures instead of BDDS, pp 317–320Google Scholar
  25. 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–49Google Scholar
  26. Bjesse P, Claessen K (2000) Sat-based verification without state space traversal. In: In formal methods in computer-aided design. Springer, pp 372–389Google Scholar
  27. 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–389Google Scholar
  28. Blochinger W, Sinz C, Kchlin W (2003) Parallel propositional satisfiability checking with distributed dynamic learning. Parallel Comput 29:969–994CrossRefGoogle Scholar
  29. 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–430Google Scholar
  30. Boy de la Tour T (1992) An optimality result for clause form translation. J Symb Comput 14(4):283–301MathSciNetCrossRefzbMATHGoogle Scholar
  31. 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–321Google Scholar
  32. Bruttomesso R, Sharygina N (2009) OpenSMT 0.1Google Scholar
  33. 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–372Google Scholar
  34. Bryant RE (1992) Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3):293–318MathSciNetCrossRefGoogle Scholar
  35. Bryant RE, Velev MN (2002) Boolean satisfiability with transitivity constraints. ACM Trans Comput Logic 3(4):604–627MathSciNetCrossRefzbMATHGoogle Scholar
  36. Bryant RE, German S, Velev MN (1999) Exploiting positive equality in a logic of equality with uninterpreted functions. Springer, London, pp 470–482zbMATHGoogle Scholar
  37. 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–80Google Scholar
  38. Butler R, Lusk E (1992) User’s guide to the p4 parallel programming systemGoogle Scholar
  39. Cai S, Su K (2013) Local search for boolean satisfiability with configuration checking and subscore. Artif Intell 204:75–98.  https://doi.org/10.1016/j.artint.2013.09.001 CrossRefzbMATHGoogle Scholar
  40. Cai S, Su K, Sattar A (2011) Local search with edge weighting and configuration checking heuristics for minimum vertex cover. Artif Intell 175(9–10):1672–1696MathSciNetCrossRefzbMATHGoogle Scholar
  41. 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–66Google Scholar
  42. Calabro C, Impagliazzo R, Paturi R (2010) On the exact complexity of evaluating quantified-CNF. In: IPEC, pp 50–59Google Scholar
  43. 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–835Google Scholar
  44. 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–1595Google Scholar
  45. 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–51Google Scholar
  46. Chrabakh W, Wolski R (2003) GrADSAT: a parallel SAT solver for the gridGoogle Scholar
  47. Chu G, Harwood A, Stuckey PJ (2009) Cache conscious data structures for Boolean satisfiability solvers. J Satisf Boolean Model Comput 6:99–120Google Scholar
  48. Davis M, Putnam H (1960) A computing procedure for quantification theory. J ACM 7(3):201–215MathSciNetCrossRefzbMATHGoogle Scholar
  49. De Moura L, Bjørner 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–340Google Scholar
  50. 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–640Google Scholar
  51. 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–1333CrossRefGoogle Scholar
  52. Drechsler R, Eggersgl S, Fey G, Tille D (2009) Test pattern generation using Boolean proof engines, 1st edn. Springer, LondonCrossRefzbMATHGoogle Scholar
  53. Een N, Mishchenko A, Sörensson 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–286Google Scholar
  54. Eggersgluss S, Tille D, Drechsler R (2009) Speeding up sat-based ATPG using dynamic clause activation. In: Asian test symposium. ATS ’09, pp 177–182Google Scholar
  55. 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–716Google Scholar
  56. En N, Srensson N (2006) Translating pseudo-Boolean constraints into sat. J Satisf Boolean Model Comput 2:1–26Google Scholar
  57. 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–518Google Scholar
  58. 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 testingGoogle Scholar
  59. 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–146Google Scholar
  60. Freeman JW (1995) Improvements to propositional satisfiability search algorithms, Philadelphia, uMI Order No. GAX95-32175Google Scholar
  61. 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–236zbMATHGoogle Scholar
  62. Fu YMZ, Malik S (2004) New features of the SAT’04 versions of zChaffGoogle Scholar
  63. 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–735Google Scholar
  64. Gil L, Flores P, Silveira LM (2008) PMSat: a parallel version of MiniSAT. J Satisf Boolean Model Comput 6:71–98MathSciNetzbMATHGoogle Scholar
  65. Giunchiglia E, Tacchella A, Giunchiglia F (2002) Sat-based decision procedures for classical modal logics. J Autom Reason 28:143–171MathSciNetCrossRefzbMATHGoogle Scholar
  66. Giunchiglia E, Maratea M, Tacchella O (2003) Look-ahead versus look-back techniques in a modern sat solver. In: SAT03—Sixth international conference on theory and applications of satisfiability testing, PortofinoGoogle Scholar
  67. 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–224CrossRefzbMATHGoogle Scholar
  68. Goldberg E, Novikov Y (2007) Berkmin: a fast and robust sat-solver. Discrete Appl Math 155(12):1549–1561MathSciNetCrossRefzbMATHGoogle Scholar
  69. Hamadi Y, Jabbour S, Saïs 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–335Google Scholar
  70. Heule MJ, Van Maaren H (2008) Parallel sat solving using bit-level operations. J Satisf Boolean Model Comput 99–116Google Scholar
  71. 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–206Google Scholar
  72. 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–666Google Scholar
  73. 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–660Google Scholar
  74. Hoos HH, Stützle T (2000) Local search algorithms for sat: an empirical evaluation. J Autom Reason 24(4):421–481.  https://doi.org/10.1023/A:1006350622830 CrossRefzbMATHGoogle Scholar
  75. 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–25CrossRefGoogle Scholar
  76. 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–461CrossRefGoogle Scholar
  77. Ivan T (2013) An efficient hardware implementation of a sat problem solver on FPGA. In: Proceedings—16th Euromicro conference on digital system design, DSD 2013. Universit de Montral, Montral, Department d’informatique et recherche oprationnelle, Montral, pp 209–216Google Scholar
  78. Jackson P, Sheridan D (2004) The optimality of a fast CNF conversion and its use with sat. APES Research Group. Technical report APES-82-2004Google Scholar
  79. 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–198Google Scholar
  80. Järvisalo M, Le Berre D, Roussel O, Simon L (2012) The international sat solver competitions. AI Mag 33(1):89–92CrossRefGoogle Scholar
  81. 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 ’09, pp 686–689Google Scholar
  82. 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–823Google Scholar
  83. 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–101MathSciNetCrossRefzbMATHGoogle Scholar
  84. Kaivola R, O’Leary 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–104Google Scholar
  85. Korovin K (2008) iProver—an 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–298Google Scholar
  86. 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–2789CrossRefGoogle Scholar
  87. 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–503Google Scholar
  88. Larrabee T (1989) Efficient generation of test patterns using boolean difference. In: Test conference, proceedings. Meeting the tests of time, international, pp 795–801Google Scholar
  89. 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’05, pp 158–172Google Scholar
  90. 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–133Google Scholar
  91. Lierler Y (2010) Sat-based answer set programming. Ph.D. dissertation, Department of Computer Sciences, The University of Texas at Austin, AustinGoogle Scholar
  92. Lindauer M, Hoos HH, Hutter F, Schaub T (2015) Autofolio: an automatically configured algorithm selector. J Artif Int Res 53(1):745–778Google Scholar
  93. Lin F, Zhao Y (2004) Assat: computing answer sets of a logic program by sat solvers. In: Artificial intelligence, nonmonotonic reasoning, vol. 157(1–2), pp 115–137. http://www.sciencedirect.com/science/article/pii/S0004370204000578
  94. 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–559Google Scholar
  95. Luo C, Cai S, Su K, Wu W (2014) Clause states based configuration checking in local search for satisfiability. IEEE Trans Cybern 99:1–1Google Scholar
  96. 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–2709 (in press)Google Scholar
  97. 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–9Google Scholar
  98. Manthey N (2011) Solver submission of RISS 1.0 to the sat competition 2011. SAT CompetitionGoogle Scholar
  99. Marić F, Janičić P (2010) Formal correctness proof for dpll procedure. Informatica 21:57–78MathSciNetzbMATHGoogle Scholar
  100. Marques R (2013) Parallel sat solver. Universidade Tcnica de LisboaGoogle Scholar
  101. 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–680Google Scholar
  102. Marques-Silva J, Sakallah K (1999) GRASP: a search algorithm for propositional satisfiability. IEEE Trans Comput 5(48):506–521MathSciNetCrossRefGoogle Scholar
  103. 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–476Google Scholar
  104. 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–264Google Scholar
  105. 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–13CrossRefGoogle Scholar
  106. 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–535Google Scholar
  107. 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–173Google Scholar
  108. 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–535Google Scholar
  109. Nadel A (2002) The jerusat sat solver. Master’s thesis, Hebrew University of JerusalemGoogle Scholar
  110. Naumowicz A (2014) SAT-enhanced mizar proof checking. Springer, Berlin, pp 449–452zbMATHGoogle Scholar
  111. Ogawa M, Khanh T (2013) Sat and SMT: their algorithm designs and applications. In: Software engineering conference (APSEC), 20th Asia-Pacific, vol 2, pp 83–84Google Scholar
  112. Olivier Bailleux YB, Roussel O (2006) A translation of pseudo Boolean constraints to sat. J Satisf Boolean Model Comput 2:191–200zbMATHGoogle Scholar
  113. 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–299Google Scholar
  114. 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–668Google Scholar
  115. 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–173CrossRefGoogle Scholar
  116. 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–6Google Scholar
  117. Rodrguez Vega M (2014) Analyzing toys models of arabidopsis and drosphila using z3 SMT-lib, vol 9118, pp 13–15Google Scholar
  118. Ryan L (2004) Efficient algorithms for clause-learning sat solvers. Simon Fraser University, BurnabyGoogle Scholar
  119. 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–343Google Scholar
  120. 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–446 (in press)Google Scholar
  121. Sheeran M, Singh S, Stålmarck 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–125Google Scholar
  122. Sheini HM, Sakallah KA (2006) Pueblo: a hybrid pseudo-Boolean sat solver. J Satisf Boolean Model Comput 2:165–189zbMATHGoogle Scholar
  123. 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–70Google Scholar
  124. Sorensson N, Een N (2005) Minisat v1.13—a SAT solver with conflict-clause minimization. In: Eighth international conference on theory and applications of satisfiability testing (SAT 2005), vol 3569. Springer, St. AndrewsGoogle Scholar
  125. 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, SwedenGoogle Scholar
  126. 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–291Google Scholar
  127. 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
  128. Tseitin GS (1968) On the complexity of derivations in the propositional calculus. Stud Math Math Logic Part II:115–125Google Scholar
  129. Tsuchiya T (2012) Model checking that uses satisfiability solving. Comput Softw 29(1):19–29Google Scholar
  130. Tveretina O, Wesselink W (2009) Eufdpll—a tool to check satisfiability of equality logic formulas. Electron Not Theor Comput Sci 225:405–420CrossRefzbMATHGoogle Scholar
  131. 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–315Google Scholar
  132. 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 ’04), pp 242–254Google Scholar
  133. Vizel Y, Grumberg O (2009) Interpolation-sequence based model checking. In: FMCAD, pp 1–8Google Scholar
  134. 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–15Google Scholar
  135. Wieringa S, Niemenmaa M, Heljanko K (2009) Tarmo: a framework for parallelized bounded model checking. In: Brim L, van der Pol J (eds) Proceedings of the 8th international workshop on parallel and distributed methods in verification (PDMC’09), electronic proceedings in theoretical computer science (EPTCS), vol 14 pp 62–76Google Scholar
  136. 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–720Google Scholar
  137. 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–6Google Scholar
  138. Xu L, Hutter F, Hoos HH, Leyton-Brown K (2008) Satzilla: Portfolio-based algorithm selection for sat. J Artif Int Res 32(1):565–606zbMATHGoogle Scholar
  139. 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–24CrossRefGoogle Scholar
  140. Zhang H (1997) Sato: an efficient propositional prover. In: Proceedings of the 14th international conference on automated deduction. Springer, London, pp 272–275Google Scholar
  141. 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–560MathSciNetCrossRefzbMATHGoogle Scholar
  142. 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–285Google Scholar
  143. 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 ’09, pp 508–513Google Scholar

Copyright information

© Springer Science+Business Media B.V., part of Springer Nature 2018

Authors and Affiliations

  1. 1.School of Electrical Engineering and Information TechnologyGerman Jordanian UniversityAmmanJordan
  2. 2.Computer Engineering DepartmentKuwait UniversityKuwait CityKuwait

Personalised recommendations