research-article

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

Authors:

Mohammad H. Al Shayeji,

Raed MeslehAuthors Info & Claims

Volume 52, Issue 4

Pages 2575 - 2601

https://doi.org/10.1007/s10462-018-9628-0

Published: 01 December 2019 Publication History

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.

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

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

[3]

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

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

[5]

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

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

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

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

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

[10]

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

Digital Library

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

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

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

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

[15]

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

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

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

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

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

[20]

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

[21]

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

[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 University

[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–320

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

[26]

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

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

[28]

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

Digital Library

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

[30]

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

Digital Library

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

[32]

Bruttomesso R, Sharygina N (2009) OpenSMT 0.1

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

[34]

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

Digital Library

[35]

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

Digital Library

[36]

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

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

[38]

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

[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

Digital Library

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

Digital Library

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

[42]

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

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

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

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

[46]

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

[47]

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

[48]

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

Digital Library

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

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

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

Digital Library

[52]

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

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

[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–182

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

[56]

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

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

[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 testing

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

[60]

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

Digital Library

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

[62]

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

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

[64]

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

[65]

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

Digital Library

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

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

Digital Library

[68]

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

Digital Library

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

[70]

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

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

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

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

[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

Digital Library

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

Digital Library

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

Digital Library

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

[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-2004

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

[80]

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

Digital Library

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

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

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

Digital Library

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

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

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

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

[88]

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

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

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

[91]

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

[92]

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

Digital Library

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

[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–1

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

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

[98]

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

[99]

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

Digital Library

[100]

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

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

[102]

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

Digital Library

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

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

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

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

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

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

[109]

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

[110]

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

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

[112]

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

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

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

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

Digital Library

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

[117]

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

[118]

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

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

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

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

[122]

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

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

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

[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, Sweden

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

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

[129]

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

[130]

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

Digital Library

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

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

[133]

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

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

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

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

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

[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–606

Digital Library

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

[140]

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

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

Digital Library

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

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

Cited By

Liu PXu YLiu JChen SCao FWu G(2023)Fully reusing clause deduction algorithm based on standard contradiction separation ruleInformation Sciences: an International Journal10.1016/j.ins.2022.11.128622:C(337-356)Online publication date: 9-Mar-2023
https://dl.acm.org/doi/10.1016/j.ins.2022.11.128
Kuiter EKrieter SSundermann CThüm TSaake G(2022)Tseitin or not Tseitin? The Impact of CNF Transformations on Feature-Model AnalysesProceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering10.1145/3551349.3556938(1-13)Online publication date: 10-Oct-2022
https://dl.acm.org/doi/10.1145/3551349.3556938
Nooraei Abadeh MAjoudanian S(2021)Reconfigurable edge as a service: enhancing edges using quality-based solutionsThe Journal of Supercomputing10.1007/s11227-020-03579-277:7(6754-6787)Online publication date: 1-Jul-2021
https://dl.acm.org/doi/10.1007/s11227-020-03579-2

Index Terms

A comprehensive study and analysis on SAT-solvers: advances, usages and achievements
1. Hardware
  1. Hardware validation
    1. Functional verification

Index terms have been assigned to the content through auto-classification.

Recommendations

Making deduction more effective in SAT solvers

Satisfiability (SAT) solvers often benefit from transformations of the formula to be decided that allow them to do more through deduction and decrease their reliance on enumeration. For formulae in conjunctive normal form, subsumed clauses may be ...
Global Optimization for Satisfiability (SAT) Problem

The satisfiability (SAT) problem is a fundamental problem in mathematical logic, inference, automated reasoning, VLSI engineering, and computing theory. Following CNF and DNF local search methods, we introduce the Universal SAT problem model, UniSAT, ...
CDCL(Crypto) SAT solvers for cryptanalysis
CASCON '19: Proceedings of the 29th Annual International Conference on Computer Science and Software Engineering

Over the last two decades we have seen a dramatic improvement in the efficiency of conflict-driven clause-learning Boolean satisfiability (CDCL SAT) solvers on industrial problems from a variety of domains. The availability of such a powerful general-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Artificial Intelligence Review

Artificial Intelligence Review Volume 52, Issue 4

Dec 2019

566 pages

ISSN:0269-2821

Issue’s Table of Contents

Copyright © 2019 Springer Nature B.V.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 December 2019

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Liu PXu YLiu JChen SCao FWu G(2023)Fully reusing clause deduction algorithm based on standard contradiction separation ruleInformation Sciences: an International Journal10.1016/j.ins.2022.11.128622:C(337-356)Online publication date: 9-Mar-2023
https://dl.acm.org/doi/10.1016/j.ins.2022.11.128
Kuiter EKrieter SSundermann CThüm TSaake G(2022)Tseitin or not Tseitin? The Impact of CNF Transformations on Feature-Model AnalysesProceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering10.1145/3551349.3556938(1-13)Online publication date: 10-Oct-2022
https://dl.acm.org/doi/10.1145/3551349.3556938
Nooraei Abadeh MAjoudanian S(2021)Reconfigurable edge as a service: enhancing edges using quality-based solutionsThe Journal of Supercomputing10.1007/s11227-020-03579-277:7(6754-6787)Online publication date: 1-Jul-2021
https://dl.acm.org/doi/10.1007/s11227-020-03579-2

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents