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

• 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–425

• 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–132

• Ackermann W (1954) Solvable cases of the decision problem, 1st edn. North-Holland Publishing, North-Holland

  MATH  Google Scholar 

• 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–353

• Aloul FA (2006) Search techniques for sat-based Boolean optimization, modeling, simulation and applied optimization. J Franklin Inst 343(4–5):436–447

  Article  Google Scholar 

• 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–268

• 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–223

• 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–392

• 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–4

• Argelich J, Manyà F (2006) Exact MAX-SAT solvers for over-constrained problems. J Heuristics 12(4–5):375–392

  Article  Google Scholar 

• 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–134

• 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–317

• 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–404

• 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–205

• Bacchus F, Winter J (2003) Effective preprocessing with hyper-resolution and equality reduction. In: SAT, pp 341–355

• 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, Helsinki

• 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–885

• 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–929

• 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–10

• Bentley B (2005) Validating a modern microprocessor. In: Proceedings of the 17th international conference on computer aided verification. Springer, Berlin, pp 2–4

• Bhm M, Speckenmeyer E (1996) A fast parallel sat-solver-efficient workload balancing’. In: Annals of mathematics and artificial intelligence, p 40

• 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

• Biere A (2015) AIGER format and toolbox. http://fmv.jku.at/aiger/

• Biere A, Cimatti A, Clarke EM, Fujita M, Zhu Y (1999) Symbolic model checking using sat procedures instead of BDDS, pp 317–320

• 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–49

• Bjesse P, Claessen K (2000) Sat-based verification without state space traversal. In: In formal methods in computer-aided design. Springer, pp 372–389

• 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–389

• Blochinger W, Sinz C, Kchlin W (2003) Parallel propositional satisfiability checking with distributed dynamic learning. Parallel Comput 29:969–994

  Article  Google Scholar 

• 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–430

• Boy de la Tour T (1992) An optimality result for clause form translation. J Symb Comput 14(4):283–301

  Article  MathSciNet  Google Scholar 

• 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–321

• Bruttomesso R, Sharygina N (2009) OpenSMT 0.1

• 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–372

• Bryant RE (1992) Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3):293–318

  Article  MathSciNet  Google Scholar 

• Bryant RE, Velev MN (2002) Boolean satisfiability with transitivity constraints. ACM Trans Comput Logic 3(4):604–627

  Article  MathSciNet  Google Scholar 

• Bryant RE, German S, Velev MN (1999) Exploiting positive equality in a logic of equality with uninterpreted functions. Springer, London, pp 470–482

  MATH  Google Scholar 

• 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–80

• Butler R, Lusk E (1992) User’s guide to the p4 parallel programming system

• 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

  Article  MATH  Google Scholar 

• 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–1696

  Article  MathSciNet  Google Scholar 

• 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–66

• Calabro C, Impagliazzo R, Paturi R (2010) On the exact complexity of evaluating quantified-CNF. In: IPEC, pp 50–59

• 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–835

• 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–1595

• 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–51

• Chrabakh W, Wolski R (2003) GrADSAT: a parallel SAT solver for the grid

• Chu G, Harwood A, Stuckey PJ (2009) Cache conscious data structures for Boolean satisfiability solvers. J Satisf Boolean Model Comput 6:99–120

• Davis M, Putnam H (1960) A computing procedure for quantification theory. J ACM 7(3):201–215

  Article  MathSciNet  Google Scholar 

• 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–340

• 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–640

• 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–1333

  Article  Google Scholar 

• Drechsler R, Eggersgl S, Fey G, Tille D (2009) Test pattern generation using Boolean proof engines, 1st edn. Springer, London

  Book  Google Scholar 

• 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–286

• Eggersgluss S, Tille D, Drechsler R (2009) Speeding up sat-based ATPG using dynamic clause activation. In: Asian test symposium. ATS ’09, pp 177–182

• 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–716

• En N, Srensson N (2006) Translating pseudo-Boolean constraints into sat. J Satisf Boolean Model Comput 2:1–26

  Google Scholar 

• 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–518

• 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

• 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–146

• Freeman JW (1995) Improvements to propositional satisfiability search algorithms, Philadelphia, uMI Order No. GAX95-32175

• 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–236

  MATH  Google Scholar 

• Fu YMZ, Malik S (2004) New features of the SAT’04 versions of zChaff

• 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–735

• Gil L, Flores P, Silveira LM (2008) PMSat: a parallel version of MiniSAT. J Satisf Boolean Model Comput 6:71–98

  MathSciNet  MATH  Google Scholar 

• Giunchiglia E, Tacchella A, Giunchiglia F (2002) Sat-based decision procedures for classical modal logics. J Autom Reason 28:143–171

  Article  MathSciNet  Google Scholar 

• 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, Portofino

• 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–224

  Article  Google Scholar 

• Goldberg E, Novikov Y (2007) Berkmin: a fast and robust sat-solver. Discrete Appl Math 155(12):1549–1561

  Article  MathSciNet  Google Scholar 

• 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–335

• Heule MJ, Van Maaren H (2008) Parallel sat solving using bit-level operations. J Satisf Boolean Model Comput 99–116

• 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–206

• 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–666

• 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–660

• 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

  Article  MATH  Google Scholar 

• 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–25

  Article  Google Scholar 

• 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–461

  Article  Google Scholar 

• 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–216

• 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

• 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–198

• Järvisalo M, Le Berre D, Roussel O, Simon L (2012) The international sat solver competitions. AI Mag 33(1):89–92

  Article  Google Scholar 

• 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–689

• 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–823

• 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–101

  Article  MathSciNet  Google Scholar 

• 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–104

• 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–298

• 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–2789

  Article  Google Scholar 

• 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–503

• Larrabee T (1989) Efficient generation of test patterns using boolean difference. In: Test conference, proceedings. Meeting the tests of time, international, pp 795–801

• 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–172

• 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–133

• Lierler Y (2010) Sat-based answer set programming. Ph.D. dissertation, Department of Computer Sciences, The University of Texas at Austin, Austin

• Lindauer M, Hoos HH, Hutter F, Schaub T (2015) Autofolio: an automatically configured algorithm selector. J Artif Int Res 53(1):745–778

  Google Scholar 

• 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

• 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–559

• Luo C, Cai S, Su K, Wu W (2014) Clause states based configuration checking in local search for satisfiability. IEEE Trans Cybern 99:1–1

  Google Scholar 

• 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)

• 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–9

• Manthey N (2011) Solver submission of RISS 1.0 to the sat competition 2011. SAT Competition

• Marić F, Janičić P (2010) Formal correctness proof for dpll procedure. Informatica 21:57–78

  MathSciNet  MATH  Google Scholar 

• Marques R (2013) Parallel sat solver. Universidade Tcnica de Lisboa

• 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–680

• Marques-Silva J, Sakallah K (1999) GRASP: a search algorithm for propositional satisfiability. IEEE Trans Comput 5(48):506–521

  Article  MathSciNet  Google Scholar 

• 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–476

• 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–264

• 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–13

  Chapter  Google Scholar 

• 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–535

• 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–173

• 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–535

• Nadel A (2002) The jerusat sat solver. Master’s thesis, Hebrew University of Jerusalem

• Naumowicz A (2014) SAT-enhanced mizar proof checking. Springer, Berlin, pp 449–452

  MATH  Google Scholar 

• 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–84

• Olivier Bailleux YB, Roussel O (2006) A translation of pseudo Boolean constraints to sat. J Satisf Boolean Model Comput 2:191–200

  MATH  Google Scholar 

• 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–299

• 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–668

• 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–173

  Article  Google Scholar 

• 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–6

• Rodrguez Vega M (2014) Analyzing toys models of arabidopsis and drosphila using z3 SMT-lib, vol 9118, pp 13–15

• Ryan L (2004) Efficient algorithms for clause-learning sat solvers. Simon Fraser University, Burnaby

  Google Scholar 

• 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–343

• 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)

• 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–125

• Sheini HM, Sakallah KA (2006) Pueblo: a hybrid pseudo-Boolean sat solver. J Satisf Boolean Model Comput 2:165–189

  MATH  Google Scholar 

• 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–70

• 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. Andrews

• 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

• 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–291

• 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

• Tseitin GS (1968) On the complexity of derivations in the propositional calculus. Stud Math Math Logic Part II:115–125

  MATH  Google Scholar 

• Tsuchiya T (2012) Model checking that uses satisfiability solving. Comput Softw 29(1):19–29

  Google Scholar 

• Tveretina O, Wesselink W (2009) Eufdpll—a tool to check satisfiability of equality logic formulas. Electron Not Theor Comput Sci 225:405–420

  Article  Google Scholar 

• 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–315

• 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–254

• Vizel Y, Grumberg O (2009) Interpolation-sequence based model checking. In: FMCAD, pp 1–8

• 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–15

• 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–76

• 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–720

• 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–6

• Xu L, Hutter F, Hoos HH, Leyton-Brown K (2008) Satzilla: Portfolio-based algorithm selection for sat. J Artif Int Res 32(1):565–606

  MATH  Google Scholar 

• 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–24

  Article  Google Scholar 

• Zhang H (1997) Sato: an efficient propositional prover. In: Proceedings of the 14th international conference on automated deduction. Springer, London, pp 272–275

• 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–560

  Article  MathSciNet  Google Scholar 

• 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–285

• 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–513

Download references