A survey of recent advances in SAT-based formal verification

Untitled work

(1979) · Cited by 43,841

Graph-Based Algorithms for Boolean Function Manipulation

Bryant (1986) · IEEE Transactions on Computers · doi:10.1109/tc.1986.1676819 · Cited by 8,941

Model checking

Clarke, E. M., Grümberg, O., & Long, D. (1996) · Cited by 6,877

Model Checking

Clarke, E. M., & Schlingloff, B. (1999) · Cited by 4,237

Temporal and Modal Logic

Emerson, E. (1991) · Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics · doi:10.1016/b978-0-444-88074-1.50021-4 · Cited by 3,268

A machine program for theorem-proving

Davis, M. D., Logemann, G. W., & Loveland, D. W. (1962) · Communications of the ACM · doi:10.1145/368273.368557 · Cited by 3,240

Chaff

Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., & Malik, S. (2001) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1145/378239.379017 · Cited by 2,954

Symbolic model checking

Clarke, E., McMillan, K. L., Campos, S., & Hartonas-Garmhausen, V. (1996) · Lecture notes in computer science · doi:10.1007/3-540-61474-5_93 · Cited by 2,846

A Computing Procedure for Quantification Theory

Davis, M. D., & Putnam, H. (1960) · Journal of the ACM · doi:10.1145/321033.321034 · Cited by 2,657

Design and synthesis of synchronization skeletons using branching time temporal logic

Clarke, E. M., & Emerson, E. A. (2005) · Springer eBooks · doi:10.1007/bfb0025774 · Cited by 2,223

Quantum algorithms: an overview

Montanaro, A. (2016) · npj Quantum Information · doi:10.1038/npjqi.2015.23 · Cited by 1,071

Predicting learnt clauses quality in modern SAT solvers

Audemard, G., & Simon, L. (2009) · Cited by 498

Algorithm runtime prediction: Methods & evaluation

Hutter, F., Xu, L., Hoos, H. H., & Leyton‐Brown, K. (2013) · Artificial Intelligence · doi:10.1016/j.artint.2013.10.003 · Cited by 424

Combinatorial Optimization and Reasoning with Graph Neural Networks

Cappart, Q., Chételat, D., Khalil, E. B., Lodi, A., Morris, C., & Veličković, P. (2021) · International Joint Conference on Artificial Intelligence · doi:10.24963/ijcai.2021/595 · Cited by 315

Linear Encodings of Bounded LTL Model Checking

Biere, A., Heljanko, K., Junttila, T. A., Latvala, T., & Schuppan, V. (2006) · Logical Methods in Computer Science · doi:10.2168/lmcs-2(5:5)2006 · Cited by 224

ASlib: A benchmark library for algorithm selection

Bischl, B., Kerschke, P., Kotthoff, L., Lindauer, M., Malitsky, Y., Fréchette, A., Hoos, H. H., Hutter, F., Leyton‐Brown, K., Tierney, K., et al. (2016) · Artificial Intelligence · doi:10.1016/j.artint.2016.04.003 · Cited by 215

Automated Algorithm Configuration and Parameter Tuning

Hoos, H. H. (2011) · Springer eBooks · doi:10.1007/978-3-642-21434-9_3 · Cited by 215

Challenges and opportunities in quantum optimization

Abbas, A., Ambainis, A., Augustino, B., Bärtschi, A., Buhrman, H., Coffrin, C., Cortiana, G., Dunjko, V., Egger, D. J., Elmegreen, B. G., et al. (2024) · Nature Reviews Physics · doi:10.1038/s42254-024-00770-9 · Cited by 201

Exact Multiple-Control Toffoli Network Synthesis With SAT Techniques

Grosse, D. J., Wille, R., Dueck, G. W., & Drechsler, R. (2009) · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · doi:10.1109/tcad.2009.2017215 · Cited by 178

Boolean Satisfiability Solvers and Their Applications in Model Checking

Vizel, Y., Weißenbacher, G., & Malik, S. (2015) · Proceedings of the IEEE · doi:10.1109/jproc.2015.2455034 · Cited by 120

Formal verification approaches and standards in the cloud computing: A comprehensive and systematic review

Souri, A., Navimipour, N. J., & Rahmani, A. M. (2017) · Computer Standards & Interfaces · doi:10.1016/j.csi.2017.11.007 · Cited by 110

Propositional Satisfiability and Constraint Programming

Bordeaux, L., Hamadi, Y., & Zhang, L. (2006) · ACM Computing Surveys · doi:10.1145/1177352.1177354 · Cited by 107

An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment

Amla, N., Du, X., Kuehlmann, A., Kurshan, R. P., & McMillan, K. L. (2005) · Lecture notes in computer science · doi:10.1007/11560548_20 · Cited by 104

Efficient SAT-based bounded model checking for software verification

Ivančić, F., Yang, Z., Ganai, M., Gupta, A., & Ashar, P. N. (2008) · Theoretical Computer Science · doi:10.1016/j.tcs.2008.03.013 · Cited by 98

Boosting Verification by Automatic Tuning of Decision Procedures

Hutter, F., Babić, D., Hoos, H. H., & Hu, A. J. (2007) · doi:10.1109/fmcad.2007.13 · Cited by 95

Fixed-Parameter Algorithms For Artificial Intelligence, Constraint Satisfaction and Database Problems

Gottlob, G., & Szeider, S. (2007) · The Computer Journal · doi:10.1093/comjnl/bxm056 · Cited by 93

Logical Formalizations of Commonsense Reasoning: A Survey

Davis, E. (2017) · Journal of Artificial Intelligence Research · doi:10.1613/jair.5339 · Cited by 97

Model checking C programs using F-Soft

Ivančić, F., Shlyakhter, I. A., Gupta, A., Ganai, M., Kahlon, V., Wang, C., & Yang, Z. (2006) · IEEE International Conference on Computer Design: VLSI in Computers and Processors (ICCD) · doi:10.1109/iccd.2005.77 · Cited by 90

Boosting Verification by Automatic Tuning of Decision Procedures

Hutter, F., Babić, D., Hoos, H. H., & Hu, A. J. (2007) · Formal Methods in Computer-Aided Design · doi:10.1109/famcad.2007.9 · Cited by 79

Backdoors to Satisfaction

Gaspers, S., & Szeider, S. (2012) · Lecture notes in computer science · doi:10.1007/978-3-642-30891-8_15 · Cited by 76

Applying quantum algorithms to constraint satisfaction problems

Campbell, E. T., Khurana, A., & Montanaro, A. (2019) · Quantum · doi:10.22331/q-2019-07-18-167 · Cited by 89

The Configurable SAT Solver Challenge (CSSC)

Hutter, F., Lindauer, M., Balint, A., Bayless, S., Hoos, H. H., & Leyton‐Brown, K. (2016) · Artificial Intelligence · doi:10.1016/j.artint.2016.09.006 · Cited by 69

Accelerating high-level bounded model checking

Ganai, M., & Gupta, A. (2006) · Digest of technical papers/Digest of technical papers - IEEE/ACM International Conference on Computer-Aided Design · doi:10.1145/1233501.1233664 · Cited by 65

Quantum Optimization: Potential, Challenges, and the Path Forward

Abbas, A., (NNSA), U. N. N. S. A., Ambainis, A., Augustino, B., Bärtschi, A., Buhrman, H., Coffrin, C., Cortiana, G., Dunjko, V., Egger, D., et al. (2023) · OSTI OAI (U.S. Department of Energy Office of Scientific and Technical Information) · doi:10.2172/2229681 · Cited by 65

Bit-Exact ECC Recovery (BEER): Determining DRAM On-Die ECC Functions by Exploiting DRAM Data Retention Characteristics

Patel, M., Kim, J. S., Shahroodi, T., Hassan, H., & Mutlu, O. (2020) · IEEE/ACM International Symposium on Microarchitecture (MICRO) · doi:10.1109/micro50266.2020.00034 · Cited by 58

A Survey on Network Verification and Testing With Formal Methods: Approaches and Challenges

Li, Y., Yin, X., Wang, Z., Yao, J., Shi, X., Wu, J., Zhang, H., & Wang, Q. (2018) · IEEE Communications Surveys & Tutorials · doi:10.1109/comst.2018.2868050 · Cited by 54

A Restriction of Extended Resolution for Clause Learning SAT Solvers

Audemard, G., Katsirelos, G., & Simon, L. (2010) · Proceedings of the AAAI Conference on Artificial Intelligence · doi:10.1609/aaai.v24i1.7553 · Cited by 53

Functional Test Generation Using Efficient Property Clustering and Learning Techniques

Chen, M., & Mishra, P. (2010) · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · doi:10.1109/tcad.2010.2041846 · Cited by 53

1 Applying Formal Methods to Networking: Theory, Techniques and ApplicationsPreprint

Qadir, J., & Hasan, O. (2016) · Cited by 51

Understanding the empirical hardness of NP-complete problems

Leyton-Brown, K., Hoos, H., Hutter, F., & Xu, L. (2014) · CACM · doi:10.1145/2594413.2594424 · Cited by 54

Applying Formal Methods to Networking: Theory, Techniques, and Applications

Qadir, J., & Hasan, O. (2014) · IEEE Communications Surveys & Tutorials · doi:10.1109/comst.2014.2345792 · Cited by 48

Temporal Representation and Reasoning.

Fisher, M. (2008) · Cited by 45

Relational Hidden Variables and Non-Locality

Abramsky, S. (2013) · Studia Logica · doi:10.1007/s11225-013-9477-4 · Cited by 43

Using Boolean satisfiability for computing soft error rates in early design stages

Shazli, S. Z., & Tahoori, M. B. (2009) · Microelectronics Reliability · doi:10.1016/j.microrel.2009.08.006 · Cited by 42

The AI Methods, Capabilities and Criticality Grid

Schmid, T., Hildesheim, W., Holoyad, T., & Schumacher, K. (2021) · Künstliche Intell. · doi:10.1007/s13218-021-00736-4 · Cited by 46

Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation

Grümberg, O., Heyman, T., Ifergan, N., & Schuster, A. (2005) · Lecture notes in computer science · doi:10.1007/11560548_12 · Cited by 41

SAT-Based Verification Methods and Applications in Hardware Verification

Gupta, A., Ganai, M., & Wang, C. (2006) · Lecture notes in computer science · doi:10.1007/11757283_5 · Cited by 40

Protecting analog circuits with parameter biasing obfuscation

Rao, V. V., & Savidis, I. (2017) · IEEE Latin American Test Symposium (LATS) · doi:10.1109/latw.2017.7906739 · Cited by 40

Finding Efficient Circuits Using SAT-Solvers

Kojevnikov, A., Kulikov, A. S., & Yaroslavtsev, G. (2009) · Lecture notes in computer science · doi:10.1007/978-3-642-02777-2_5 · Cited by 39

SAT-Based Model Checking

Biere, A., & Kroening, D. (2018) · Springer eBooks · doi:10.1007/978-3-319-10575-8_10 · Cited by 39

Building a Knowledge Base System for an Integration of Logic Programming and Classical Logic

Denecker, M., & Vennekens, J. (2008) · Lecture notes in computer science · doi:10.1007/978-3-540-89982-2_12 · Cited by 38

A Formula-based Approach for Automatic Fault Localization of Multi-fault Programs

Lamraoui, S.-M., & Nakajima, S. (2016) · Journal of Information Processing · doi:10.2197/ipsjjip.24.88 · Cited by 38

Continuous Search in Constraint Programming

Arbeláez, A., Hamadi, Y., & Sébag, M. (2010) · IEEE International Conference on Tools with Artificial Intelligence (ICTAI) · doi:10.1109/ictai.2010.17 · Cited by 37

Functional test generation using design and property decomposition techniques

Koo, H.-M., & Mishra, P. (2009) · ACM Transactions on Embedded Computing Systems · doi:10.1145/1550987.1550995 · Cited by 35

SAT-solving in practice

Claessen, K., Eén, N., Sheeran, M., & Sörensson, N. (2008) · International Workshop on Discrete Event Systems · doi:10.1109/wodes.2008.4605923 · Cited by 33

Test generation using SAT-based bounded model checking for validation of pipelined processors

Koo, H.-M., & Mishra, P. (2006) · ACM Great Lakes Symposium on VLSI (GLSVLSI) · doi:10.1145/1127908.1127991 · Cited by 33

Towards a notion of unsatisfiable and unrealizable cores for LTL

Schuppan, V. (2010) · Science of Computer Programming · doi:10.1016/j.scico.2010.11.004 · Cited by 33

Complexity of Fixed-Size Bit-Vector Logics

Kovásznai, G., Fröhlich, A., & Biere, A. (2015) · Theory of Computing Systems · doi:10.1007/s00224-015-9653-1 · Cited by 33

Soundness of Q-resolution with dependency schemes

Slivovsky, F., & Szeider, S. (2015) · Theoretical Computer Science · doi:10.1016/j.tcs.2015.10.020 · Cited by 32

On Approaches to Explaining Infeasibility of Sets of Boolean Clauses

Grégoire, É., Mazure, B., & Piette, C. (2008) · IEEE International Conference on Tools with Artificial Intelligence (ICTAI) · doi:10.1109/ictai.2008.39 · Cited by 31

SAT-Solving in Practice, with a Tutorial Example from Supervisory Control

Claessen, K., Eén, N., Sheeran, M., Sörensson, N., Voronov, A., & Åkesson, K. (2009) · Discrete Event Dynamic Systems · doi:10.1007/s10626-009-0081-8 · Cited by 30

Deep Learning for Autonomous Vehicle Control: Algorithms, State-of-the-Art, and Future Prospects

Kuutti, S., Fallah, S., Bowden, R., & Barber, P. (2019) · Synthesis lectures on advances in automotive technology · doi:10.2200/s00932ed1v01y201906aat008 · Cited by 29

A Clause-Based Heuristic for SAT Solvers

Dershowitz, N., Hanna, Z., & Nadel, A. (2005) · Lecture notes in computer science · doi:10.1007/11499107_4 · Cited by 29

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

Alouneh, S., Abed, S., Alshayeji, M. H., & Mesleh, R. (2018) · Artificial Intelligence Review · doi:10.1007/s10462-018-9628-0 · Cited by 28

First steps towards SAT-based formal analog verification

Tiwary, S. K., Gupta, A., Phillips, J. R., Pinello, C., & Zlatanovici, R. (2009) · doi:10.1145/1687399.1687401 · Cited by 28

Efficient test case generation for validation of UML activity diagrams

Chen, M., Mishra, P., & Kalita, D. (2010) · Design Automation for Embedded Systems · doi:10.1007/s10617-010-9052-4 · Cited by 26

Survey on automated symbolic verification and its application for synthesising cyber‐physical systems

Cordeiro, L. C., Filho, E. B. L., & de Bessa, I. V. (2019) · IET Cyber-Physical Systems Theory & Applications · doi:10.1049/iet-cps.2018.5006 · Cited by 26

Model Checking: Software and Beyond

Clarke, E. M., & Lerda, F. (2020) · doi:10.3217/jucs-013-05-0639 · Cited by 26

Mesh Based Obfuscation of Analog Circuit Properties

Rao, V. V., & Savidis, I. (2019) · IEEE International Symposium on Circuits and Systems proceedings · doi:10.1109/iscas.2019.8702671 · Cited by 26

Accelerating High-level Bounded Model Checking

Ganai, M., & Gupta, A. (2006) · Digest of technical papers/Digest of technical papers - IEEE/ACM International Conference on Computer-Aided Design · doi:10.1109/iccad.2006.320122 · Cited by 26

Automatic decomposition for sequential equivalence checking of system level and RTL descriptions

Vasudevan, S., Abraham, J. A., Viswanath, V., & Tu, J. (2006) · ACM/IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE) · doi:10.1109/memcod.2006.1695903 · Cited by 25

Improving platform-based system synthesis by satisfiability modulo theories solving

Reimann, F., Glaß, M., Haubelt, C. D., Eberl, M., & Teich, J. (2010) · International Conference on Hardware/Software Codesign and System Synthesis · doi:10.1145/1878961.1878986 · Cited by 25

SAT-Based Compositional Verification Using Lazy Learning

Sinha, N., & Clarke, E. M. (2007) · Springer eBooks · doi:10.1007/978-3-540-73368-3_8 · Cited by 25

Automatic Generation of Model Checking Scripts Based on Environment Modeling

Yatake, K., & Aoki, T. (2010) · Lecture notes in computer science · doi:10.1007/978-3-642-16164-3_5 · Cited by 23

A systematic literature review on counterexample explanation

Kaleeswaran, A. P., Nordmann, A., Vogel, T., & Grunske, L. (2021) · Information and Software Technology · doi:10.1016/j.infsof.2021.106800 · Cited by 23

Computing high-degree polynomial gradients in memory

Bhattacharya, T., Hutchinson, G. H., Pedretti, G., Sheng, X., Ignowski, J., Vaerenbergh, T. V., Beausoleil, R. G., Strachan, J. P., & Strukov, D. B. (2024) · Nature Communications · doi:10.1038/s41467-024-52488-y · Cited by 27

Symbolic quick error detection using symbolic initial state for pre-silicon verification

Fadiheh, M. R., Urdahl, J., Nuthakki, S. S., Mitra, S., Barrett, C., Stoffel, D., & Kunz, W. (2018) · Design, Automation, and Test in Europe · doi:10.23919/date.2018.8341979 · Cited by 23

Efficient Techniques for Directed Test Generation Using Incremental Satisfiability

Mishra, P., & Chen, M. (2009) · International Conference on VLSI Design · doi:10.1109/vlsi.design.2009.72 · Cited by 22

Towards a Notion of Unsatisfiable Cores for LTL

Schuppan, V. (2010) · Lecture notes in computer science · doi:10.1007/978-3-642-11623-0_7 · Cited by 22

Model-Based Testing for Verification Back-Ends

Artho, C. V., Biere, A., & Seidl, M. (2013) · Lecture notes in computer science · doi:10.1007/978-3-642-38916-0_3 · Cited by 22

A Formula-Based Approach for Automatic Fault Localization of Imperative Programs

Lamraoui, S.-M., & Nakajima, S. (2014) · Lecture notes in computer science · doi:10.1007/978-3-319-11737-9_17 · Cited by 22

Encodings of Bounded LTL Model Checking in Effectively Propositional Logic

Navarro-Pérez, J. A., & Воронков, А. (2007) · Lecture notes in computer science · doi:10.1007/978-3-540-73595-3_24 · Cited by 22

Answer Set versus Integer Linear Programming for Automatic Synthesis of Multiprocessor Systems from Real‐Time Parallel Programs

Ishebabi, H., Mahr, P., Bobda, C., Gebser, M., & Schaub, T. H. (2009) · International Journal of Reconfigurable Computing · doi:10.1155/2009/863630 · Cited by 21

FPGA acceleration of enhanced boolean constraint propagation for SAT solvers

Thong, J., & Nicolici, N. (2013) · International Conference on Computer Aided Design · doi:10.1109/iccad.2013.6691124 · Cited by 21

Better Decision Heuristics in CDCL through Local Search and Target Phases

Cai, S., Zhang, X., Fleury, M., & Biere, A. (2022) · Journal of Artificial Intelligence Research · doi:10.1613/jair.1.13666 · Cited by 20

Simultaneous SAT-Based Model Checking of Safety Properties

Khasidashvili, Z. O., Nadel, A., Palti, A., & Hanna, Z. (2006) · Lecture notes in computer science · doi:10.1007/11678779_5 · Cited by 20

Merging nodes under sequential observability

Case, M. L., Kravets, V. N., Mishchenko, A., & Brayton, R. K. (2008) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1145/1391469.1391605 · Cited by 20

Guided Merging of Sequence Diagrams

Widl, M., Biere, A., Brosch, P., Egly, U., Heule, M. J. H., Kappel, G., Seidl, M., & Tompits, H. (2013) · Lecture notes in computer science · doi:10.1007/978-3-642-36089-3_10 · Cited by 19

A SAT-based approach to decipher Gene Regulatory Networks

Corblin, F., Hamadi, Y., Fanchon, É., & Trilling, L. (2007) · Cited by 19

Verification Techniques for System-Level Design

Fujita, M., Ghosh, I., & Prasad, M. R. (2008) · Elsevier eBooks · doi:10.1016/b978-0-12-370616-4.x5001-0 · Cited by 18

How to Implement a Theory of Correctness in the Area of Business Processes and Services

Lohmann, N., & Wolf, K. (2010) · Lecture notes in computer science · doi:10.1007/978-3-642-15618-2_7 · Cited by 18

Parallel Combinational Equivalence Checking

Possani, V. N., Mishchenko, A., Ribas, R. P., & Reis, A. I. (2019) · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · doi:10.1109/tcad.2019.2946254 · Cited by 17

Backdoors to q-Horn

Gaspers, S., Ordyniak, S., Ramanujan, M. S., Saurabh, S., & Szeider, S. (2014) · Algorithmica · doi:10.1007/s00453-014-9958-5 · Cited by 17

Translation of Algorithmic Descriptions of Discrete Functions to SAT with Applications to Cryptanalysis Problems

Semenov, A., Otpuschennikov, I. V., Gribanova, I., Заикин, О. С., & Kochemazov, S. (2020) · Logical Methods in Computer Science · doi:10.23638/lmcs-16(1:29)2020 · Cited by 17

Bosphorus: Bridging ANF and CNF Solvers

Choo, D., Soos, M., Chai, K. M. A., & Meel, K. S. (2019) · Design, Automation, and Test in Europe · doi:10.23919/date.2019.8715061 · Cited by 17

Advancements in Applications of Quantum Entanglement

Yu, Y. (2021) · Journal of Physics Conference Series · doi:10.1088/1742-6596/2012/1/012113 · Cited by 18

Learning finite cover automata from queries

Ipate, F. (2011) · Journal of Computer and System Sciences · doi:10.1016/j.jcss.2011.04.002 · Cited by 16

What is answer set programming to propositional satisfiability

Lierler, Y. (2016) · Constraints · doi:10.1007/s10601-016-9257-7 · Cited by 16

A SAT-based autonomous strategy for security vulnerability management

Barrère, M., Badonnel, R., & Festor, O. (2014) · IEEE/IFIP Network Operations and Management Symposium (NOMS) · doi:10.1109/noms.2014.6838309 · Cited by 16

Bounded Semantics of CTL and SAT-Based Verification

Zhang, W. (2009) · Lecture notes in computer science · doi:10.1007/978-3-642-10373-5_15 · Cited by 15

An Autonomous Engine for Services Configuration and Deployment

Cuadrado, F., Dueñas, J. C., & García-Carmona, R. (2011) · IEEE Transactions on Software Engineering · doi:10.1109/tse.2011.24 · Cited by 15

Bounded sequence testing from deterministic finite state machines

Ipate, F. (2010) · Theoretical Computer Science · doi:10.1016/j.tcs.2010.01.030 · Cited by 15

Online over time processing of combinatorial problems

Duque, R., Arbeláez, A., & Díaz, J. F. (2018) · Constraints · doi:10.1007/s10601-018-9287-4 · Cited by 14

Automatic Constraint Based Test Generation for Behavioral HDL Models

Hari, S. K. S., Konda, V. V. R., Kamakoti, V., Vedula, V. M., & Maneperambil, K. S. (2008) · IEEE Transactions on Very Large Scale Integration (VLSI) Systems · doi:10.1109/tvlsi.2008.917424 · Cited by 14

Scalable constraint-based virtual data center allocation

Bayless, S., Kodirov, N., Iqbal, S. M., Beschastnikh, I., Hoos, H. H., & Hu, A. J. (2019) · Artificial Intelligence · doi:10.1016/j.artint.2019.103196 · Cited by 14

Verification and refutation of C programs based on k-induction and invariant inference

Alhawi, O. M. K., Rocha, H. O., Gadelha, M. R., Cordeiro, L. C., & Batista, E. (2020) · International Journal on Software Tools for Technology Transfer · doi:10.1007/s10009-020-00564-1 · Cited by 14

Chapter 12 Temporal Representation and Reasoning

(2008) · Foundations of artificial intelligence · doi:10.1016/s1574-6526(07)03012-x · Cited by 14

Ant Colony Optimization with Adaptive Fitness Function for Satisfiability Testing

Villagra, M., & Barán, B. (2007) · Lecture notes in computer science · doi:10.1007/978-3-540-73445-1_26 · Cited by 14

QuteSAT: A Robust Circuit-based SAT Solver for Complex Circuit Structure

Wu, C.-A. R., Lin, T.-H., Lee, C.-C., & Huang, C.-Y. R. (2007) · Design, Automation, and Test in Europe · doi:10.1109/date.2007.364479 · Cited by 14

qbf2epr: A Tool for Generating EPR Formulas from QBF

Seidl, M., Lonsing, F., & Biere, A. (2018) · EPiC series in computing · doi:10.29007/2b5d · Cited by 13

SAT-based Verification -- From Core Algorithms to Novel Application Domains

Herbstritt, M. (2008) · FreiDok plus (Universitätsbibliothek Freiburg)

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

Alouneh, S., Abed, S., Alshayeji, M. H., & Mesleh, R. (2018) · Artificial Intelligence Review · doi:10.1007/s10462-018-9628-0 · Cited by 28

Tuning SAT for Formal Verification and Testing.

Velev, M. N. (2004) · Zenodo (CERN European Organization for Nuclear Research) · doi:10.3217/jucs-010-12 · Cited by 1

SAT-Based Verification Methods and Applications in Hardware Verification

Gupta, A., Ganai, M., & Wang, C. (2006) · Lecture notes in computer science · doi:10.1007/11757283_5 · Cited by 40

Editor’s Introduction to the Special Volume on Application of Constraints to Formal Verification

Velev, M. N. (2008) · Journal on Satisfiability Boolean Modeling and Computation · doi:10.3233/sat190049