{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T05:51:14Z","timestamp":1775454674491,"version":"3.50.1"},"reference-count":63,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2009,9,10]],"date-time":"2009-09-10T00:00:00Z","timestamp":1252540800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2009,12]]},"DOI":"10.1007\/s10626-009-0081-8","type":"journal-article","created":{"date-parts":[[2009,9,9]],"date-time":"2009-09-09T09:47:10Z","timestamp":1252489630000},"page":"495-524","source":"Crossref","is-referenced-by-count":23,"title":["SAT-Solving in Practice, with a Tutorial Example from Supervisory Control"],"prefix":"10.1007","volume":"19","author":[{"given":"Koen","family":"Claessen","sequence":"first","affiliation":[]},{"given":"Niklas","family":"Een","sequence":"additional","affiliation":[]},{"given":"Mary","family":"Sheeran","sequence":"additional","affiliation":[]},{"given":"Niklas","family":"S\u00f6rensson","sequence":"additional","affiliation":[]},{"given":"Alexey","family":"Voronov","sequence":"additional","affiliation":[]},{"given":"Knut","family":"\u00c5kesson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,9,10]]},"reference":[{"key":"81_CR1","series-title":"LNCS","volume-title":"Proceedings of the 6th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u20192000)","author":"PA Abdulla","year":"2000","unstructured":"Abdulla PA, Bjesse P, Een N (2000) Symbolic reachability analysis based on SAT-solvers. In: Proceedings of the 6th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u20192000). LNCS, vol 1785. Springer, Berlin"},{"key":"81_CR2","series-title":"LNCS","volume-title":"Conference on correct hardware design and verification methods (CHARME\u201905)","author":"N Amla","year":"2005","unstructured":"Amla N, Du X, Kuehlmann A, Kurshan RP, McMillan KL (2005) An analysis of SAT-based model checking techniques in an industrial environment. In: Conference on correct hardware design and verification methods (CHARME\u201905)). LNCS, vol 3725. Springer, Berlin"},{"key":"81_CR3","volume-title":"Int. conf. on formal methods in computer-aided design (FMCAD\u201907)","year":"2007","unstructured":"Baumgartner J, Sheeran M (eds) (2007) Int. conf. on formal methods in computer-aided design (FMCAD\u201907). IEEE, New York"},{"key":"81_CR4","unstructured":"Bentley B (2005) Validating a modern microprocessor, invited talk. In: 17th international conference on computer aided verification (CAV\u201905). LNS, vol 3576. Springer, Berlin. Slides available at http:\/\/www.cav2005.inf.ed.ac.uk\/Fbentley_CAV_07_08_2005.ppt"},{"key":"81_CR5","unstructured":"Biere A (2007a) PicoSAT ver 535, system description for the SAT competition. Available at http:\/\/www.satcompetition.org\/2007\/picosat.pdf"},{"key":"81_CR6","unstructured":"Biere A (2007b) Short history on SAT solver technology and what is next? Invited talk. In: Int. conf. on theory and applications of satisfiability testing (SAT\u201907). Slides available at http:\/\/fmv.jku.at\/biere\/talks\/Biere-SAT07-talk.pdf"},{"key":"81_CR7","series-title":"LNCS","volume-title":"5th international conference on tools and algorithms for construction and analysis of systems (TACAS\u201999)","author":"A Biere","year":"1999","unstructured":"Biere A, Cimatti A, Clarke EM, Zhu Y (1999a) Symbolic model checking without BDDs. In: 5th international conference on tools and algorithms for construction and analysis of systems (TACAS\u201999). LNCS, vol 1579. Springer, Berlin"},{"key":"81_CR8","series-title":"LNCS","volume-title":"Int. conf. on computer aided verification (CAV\u201999)","author":"A Biere","year":"1999","unstructured":"Biere A, Clarke E, Raimi R, Zhu Y (1999b) Verifying safety properties of a powerPC microprocessor using symbolic model checking without BDDs. In: Int. conf. on computer aided verification (CAV\u201999). LNCS, vol 1633. Springer, Berlin"},{"key":"81_CR9","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke E, Strichman O, Zhu Y (2003) Bounded model checking. In: Advances in computers","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"81_CR10","series-title":"LNCS","first-page":"372","volume-title":"Formal methods in computer-aided design (FMCAD\u201900)","author":"P Bjesse","year":"2000","unstructured":"Bjesse P, Claessen K (2000) SAT-based verification without state space traversal. In: Formal methods in computer-aided design (FMCAD\u201900). LNCS, vol 1954. Springer, New York, pp 372\u2013389"},{"key":"81_CR11","series-title":"LNCS","volume-title":"Int. conf. on computer aided verification (CAV\u201901)","author":"P Bjesse","year":"2001","unstructured":"Bjesse P, Leonard T, Mokkedem A (2001) Finding bugs in an alpha microprocessor using satisfiability solvers. In: Int. conf. on computer aided verification (CAV\u201901). LNCS, vol 2102. Springer, New York"},{"key":"81_CR12","volume-title":"Industrial-strength formal methods","author":"A Bor\u00e4lv","year":"1998","unstructured":"Bor\u00e4lv A, St\u00e5lmarck G (1998) Prover technology in railways. In: Industrial-strength formal methods. Academic, London"},{"key":"81_CR13","volume-title":"Int. conf. on formal methods in computer-aided design (FMCAD\u201907)","author":"A Bradley","year":"2007","unstructured":"Bradley A, Manna Z (2007) Checking safety by inductive generalization of counterexamples to induction. In: Int. conf. on formal methods in computer-aided design (FMCAD\u201907). IEEE, New York"},{"key":"81_CR14","doi-asserted-by":"crossref","unstructured":"Bryant R (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans. Comp. c-35:8","DOI":"10.1109\/TC.1986.1676819"},{"key":"81_CR15","volume-title":"Best of ICCAD: 20 years of excellence in computer-aided design","author":"RE Bryant","year":"2002","unstructured":"Bryant RE, Kukula JH (2002) Formal methods for functional verification. In: Best of ICCAD: 20 years of excellence in computer-aided design. ACM, New York"},{"key":"81_CR16","volume-title":"Int. conf. on formal methods in computer-aided design (FMCAD\u201907)","author":"M Case","year":"2007","unstructured":"Case M, Mishchenko A, Brayton R (2007) Automated extraction of inductive invariants to aid model checking. In: Int. conf. on formal methods in computer-aided design (FMCAD\u201907). IEEE, New York"},{"key":"81_CR17","volume-title":"Introduction to discrete event systems","author":"CG Cassandras","year":"2007","unstructured":"Cassandras CG, Lafortune S (2007) Introduction to discrete event systems. Springer, Berlin"},{"key":"81_CR18","volume-title":"Design automation conference (DAC\u201904)","author":"P Chauhan","year":"2004","unstructured":"Chauhan P, Kroening D, Clarke E (2004) A SAT-based algorithm for reparameterization in symbolic simulation. In: Design automation conference (DAC\u201904). ACM, New York"},{"key":"81_CR19","doi-asserted-by":"crossref","unstructured":"Cimatti A (2008) Beyond boolean SAT: satisfiability modulo theories. In: Proceedings of the 9th international workshop on discrete event systems. WODES08, pp 68\u201373","DOI":"10.1109\/WODES.2008.4605924"},{"key":"81_CR20","doi-asserted-by":"crossref","unstructured":"Claessen K, Een N, Sheeran M, S\u00f6rensson N (2008) SAT-solving in practice. In: Invited paper in session on SAT in WODES08","DOI":"10.1109\/WODES.2008.4605923"},{"key":"81_CR21","volume-title":"Model checking","author":"EM Clarke","year":"2000","unstructured":"Clarke EM, Grumberg O, Peled DA (2000) Model checking. MIT, Cambridge"},{"key":"81_CR22","volume-title":"Proc. 3rd ACM symp. on the theory of computing","author":"S Cook","year":"1971","unstructured":"Cook S (1971) The complexity of theorem-proving procedures. In: Proc. 3rd ACM symp. on the theory of computing. ACM, New York"},{"key":"81_CR23","series-title":"LNCS","volume-title":"Int. conf. on computer aided verification (CAV\u201901)","author":"F Copty","year":"2001","unstructured":"Copty F, Fix L, Fraer R, Giunchiglia E, Kamhi G, Tacchella A, Vardi MY (2001) Benefits of bounded model checking at an industrial setting. In: Int. conf. on computer aided verification (CAV\u201901). LNCS, vol 2102. Springer, Berlin"},{"key":"81_CR24","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis M, Putnam H (1960) A computing procedure for quantification theory. J ACM 7:201\u2013215 (reprinted in\u00a0Siekman and Wrightson 1983)","journal-title":"J ACM"},{"key":"81_CR25","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis M, Logemann G, Loveland D (1962) A machine program for theorem proving. Commun ACM 5:394\u2013397 (reprinted in Siekman and Wrightson 1983)","journal-title":"Commun ACM"},{"key":"81_CR26","unstructured":"Een N (1999) Symbolic reachability analysis based on SAT-solvers. Master\u2019s thesis, Department of Computer Systems, Uppsala University, Sweden"},{"key":"81_CR27","unstructured":"Een N (2007) Practical SAT, invited tutorial at int. conf. on formal methods in computer aided design. Slides available at http:\/\/minisat.se\/Papers.html"},{"key":"81_CR28","series-title":"LNCS","volume-title":"8th int. conf. theory and applications of satisfiability testing (SAT\u201905)","author":"N Een","year":"2005","unstructured":"Een N, Biere A (2005) Effective preprocessing in SAT through variable and clause elimination. In: 8th int. conf. theory and applications of satisfiability testing (SAT\u201905). LNCS, vol 3569. Springer, New York"},{"key":"81_CR29","series-title":"LNCS","volume-title":"Proc.\u00a0of theory and applications of satisfiability testing (SAT\u201903)","author":"N Een","year":"2003","unstructured":"Een N, S\u00f6rensson N (2003a) An extensible SAT solver. In: Proc.\u00a0of theory and applications of satisfiability testing (SAT\u201903). LNCS, vol 2919. Springer, New York"},{"key":"81_CR30","doi-asserted-by":"crossref","unstructured":"Een N, S\u00f6rensson N (2003b) Temporal induction by incremental SAT solving. In: First int. workshop on bounded model checking. ENTCS, vol 89, no 4","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"81_CR31","unstructured":"Een N, S\u00f6rensson N (2005) MiniSat v1.13 - a SAT solver with conflict-clause minimization, system description for the SAT competition. Available at http:\/\/minisat.se\/Papers.html"},{"key":"81_CR32","series-title":"LNCS","volume-title":"Int. conf. on theory and applications of satisfiability testing (SAT\u201907)","author":"N Een","year":"2007","unstructured":"Een N, Mishchenko A, S\u00f6rensson N (2007) Applying logic synthesis for speeding up SAT. In: Int. conf. on theory and applications of satisfiability testing (SAT\u201907). LNCS, vol 4501. Springer, New York"},{"key":"81_CR33","volume-title":"Design and test in Europe (DATE\u201902)","author":"E Goldberg","year":"2002","unstructured":"Goldberg E, Novikov Y (2002) BerkMin: a fast and robust SAT solver. In: Design and test in Europe (DATE\u201902). IEEE Computer Society, Los Alamitos"},{"key":"81_CR34","unstructured":"Huang J (2007) The effect of restarts on the efficiency of clause learning. In: IJCAI, pp 2318\u20132323"},{"key":"81_CR35","first-page":"57","volume-title":"Proc. 10th annual conference on computer assurance (COMPASS\u201995)","author":"JF Groote","year":"1995","unstructured":"Groote JF, van Vlijmen SFM, Koorn JWC (1995) The safety guaranteeing system at station hoorn-kersenboogerd (extended abstract). In: Proc. 10th annual conference on computer assurance (COMPASS\u201995). IEEE, New York, pp 57\u201368"},{"key":"81_CR36","volume-title":"IEEE international conference on electronics, circuits and systems (ICECS)","author":"L Guerra\u00a0e Silva","year":"1998","unstructured":"Guerra\u00a0e Silva L, Marques-Silva JP, Silveira LM, Sakallah KA (1998) Timing analysis using propositional satisfiability. In: IEEE international conference on electronics, circuits and systems (ICECS). IEEE, New York"},{"key":"81_CR37","volume-title":"Proceedings ECAI-92","author":"H Kautz","year":"1992","unstructured":"Kautz H, Selman B (1992) Planning as Satisfiability. In: Proceedings ECAI-92. Wiley, New York"},{"key":"81_CR38","unstructured":"Kunz W (2007) Formal verification of systems-on-chip\u2014industrial experiences and scientific perspectives. Invited talk at int. conf. on formal methods in computer aided design. Slides available at http:\/\/www.fmcad.org\/2007 (under Advance Program)"},{"issue":"9","key":"81_CR39","doi-asserted-by":"crossref","first-page":"1149","DOI":"10.1109\/43.310903","volume":"13","author":"W Kunz","year":"1994","unstructured":"Kunz W, Pradhan D (1994) Recursive learning: a new implication technique for efficient solutions to CAD-problems: test, verification and optimization. IEEE Trans Comput-Aided Des 13(9): 1149\u20131158","journal-title":"IEEE Trans Comput-Aided Des"},{"issue":"1","key":"81_CR40","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1109\/43.108614","volume":"11","author":"T Larrabee","year":"1992","unstructured":"Larrabee T (1992) Test pattern generation using boolean satisfiability. IEEE Trans Comput-Aided Des 11(1):6\u201322","journal-title":"IEEE Trans Comput-Aided Des"},{"key":"81_CR41","doi-asserted-by":"crossref","unstructured":"Luby M, Sinclair A, Zuckerman D (1993) Optimal speedup of Las Vegas algorithms. In: Israel symposium on theory of computing systems, pp 128\u2013133. citeseer.ist.psu.edu\/article\/luby93optimal.html","DOI":"10.1109\/ISTCS.1993.253477"},{"key":"81_CR42","doi-asserted-by":"crossref","unstructured":"Marques-Silva J (2008) Practical applications of boolean satisfiability. In: Proceedings of the 9th international workshop on discrete event systems. WODES08, pp 74\u201380","DOI":"10.1109\/WODES.2008.4605925"},{"key":"81_CR43","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1109\/ICCAD.1996.569607","volume-title":"International conference on computer-aided design (ICCAD\u201996)","author":"J Marques-Silva","year":"1996","unstructured":"Marques-Silva J, Sakallah K (1996) GRASP: A new search algorithm for satisfiability. In: International conference on computer-aided design (ICCAD\u201996). IEEE, New York, pp 220\u2013227"},{"key":"81_CR44","volume-title":"Fault-tolerant computing symposium (FTCS)","author":"J Marques-Silva","year":"1997","unstructured":"Marques-Silva J, Sakallah K (1997) Robust search algorithms for test pattern generation. In: Fault-tolerant computing symposium (FTCS). IEEE Computer Society, Los Alamitos"},{"key":"81_CR45","series-title":"LNCS","volume-title":"Int. conf. on computer aided verification (CAV\u201903)","author":"KL McMillan","year":"2003","unstructured":"McMillan KL (2003) Interpolation and SAT-based model checking. In: Int. conf. on computer aided verification (CAV\u201903). LNCS, vol 2725. Springer, New York"},{"key":"81_CR46","series-title":"LNCS","volume-title":"International conference on formal methods in computer-aided design (FMCAD\u201904)","author":"H Mony","year":"2004","unstructured":"Mony H, Baumgartner J, Paruthi V, Kanzelman R, Kuehlmann A (2004) Scalable Automated verification via expert-system guided transformations. In: International conference on formal methods in computer-aided design (FMCAD\u201904). LNCS, vol 3312. Springer, New York"},{"key":"81_CR47","volume-title":"Design automation conf. (DAC\u201901)","author":"M Moskewicz","year":"2001","unstructured":"Moskewicz M, Madigan C, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient SAT solver. In: Design automation conf. (DAC\u201901). IEEE, New York"},{"key":"81_CR48","volume-title":"International symposium on field programmable gate arrays","author":"GJ Nam","year":"1999","unstructured":"Nam GJ, Sakallah KA, Rutenbar RA (1999) Satisfiability-based layout revisited: detailed routing of complex FPGAs via search-based boolean SAT. In: International symposium on field programmable gate arrays. ACM, New York"},{"key":"81_CR49","series-title":"LNCS","first-page":"294","volume-title":"Int. conf. on theory and applications of satisfiability testing (SAT\u201907)","author":"K Pipatsrisawat","year":"2007","unstructured":"Pipatsrisawat K, Darwiche A (2007) A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva J, Sakallah KA (eds) Int. conf. on theory and applications of satisfiability testing (SAT\u201907). LNCS, vol 4501. Springer, New York, pp 294\u2013299"},{"key":"81_CR50","doi-asserted-by":"crossref","unstructured":"Prasad M, Biere A, Gupta A (2005) A survey of recent advances in SAT-based formal verification. In: Intl. journal on software tools for technology transfer (STTT), vol 7, no 2","DOI":"10.1007\/s10009-004-0183-4"},{"issue":"1","key":"81_CR51","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1137\/0325013","volume":"25","author":"PJ Ramadge","year":"1987","unstructured":"Ramadge PJ, Wonham WM (1987) Supervisory control of a class of discrete event processes. SIAM J Control Optim 25(1):206\u2013230","journal-title":"SIAM J Control Optim"},{"issue":"1","key":"81_CR52","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1109\/5.21072","volume":"77","author":"PJG Ramadge","year":"1989","unstructured":"Ramadge PJG, Wonham WM (1989) The control of discrete event systems. Proc IEEE 77(1):81\u201398","journal-title":"Proc IEEE"},{"key":"81_CR53","volume-title":"Second int. conf. on reliability, maintainability and safety (ICRMS \u201994)","author":"M S\u00e4flund","year":"1994","unstructured":"S\u00e4flund M (1994) Modelling and formally verifying systems and software in industrial applications. In: Second int. conf. on reliability, maintainability and safety (ICRMS \u201994). International Academic, London"},{"key":"81_CR54","volume-title":"Proc. fourth international workshop on microprocessor test and verification, common challenges and solutions (MTV 2003)","author":"O Shacham","year":"2003","unstructured":"Shacham O, Zarpas E (2003) Tuning the VSIDS decision heuristic for bounded model checking. In: Proc. fourth international workshop on microprocessor test and verification, common challenges and solutions (MTV 2003). IEEE Computer Society, Los Alamitos"},{"issue":"1","key":"81_CR55","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1023\/A:1008725524946","volume":"16","author":"M Sheeran","year":"2000","unstructured":"Sheeran M, St\u00e5lmarck G (2000) A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic. Form Methods Syst Des 16(1):23\u201358","journal-title":"Form Methods Syst Des"},{"key":"81_CR56","series-title":"LNCS","first-page":"108","volume-title":"Formal methods in computer-aided design (FMCAD\u201900)","author":"M Sheeran","year":"2000","unstructured":"Sheeran M, Singh S, St\u00e5lmarck G (2000) Checking safety properties using induction and a SAT-solver. In: Formal methods in computer-aided design (FMCAD\u201900). LNCS, vol 1954. Springer, New York, pp 108\u2013125"},{"key":"81_CR57","volume-title":"Automation of reasoning","year":"1983","unstructured":"Siekman J, Wrightson G (eds) (1983) Automation of reasoning. Springer, New York"},{"key":"81_CR58","series-title":"LNCS","volume-title":"Int. conf. on formal methods in computer-aided design","year":"1996","unstructured":"Srivas M, Camilleri A (eds) (1996) Int. conf. on formal methods in computer-aided design. LNCS, vol 1146. Springer, New York"},{"key":"81_CR59","unstructured":"St\u00e5lmarck G (1989) A system for determining propositional logic theorems by applying values and rules to triplets that are generated from a formula. Swedish patent no. 467 076 (approved 1992), U.S. patent no. 5 276 897 (approved 1994), European patent no. 0403 454 (approved 1995)"},{"key":"81_CR60","unstructured":"Tseitin G (1968) On the complexity of derivation in propositional calculus. In: Studies in constr. math. and math. logic"},{"key":"81_CR61","volume-title":"Int. conf. on design automation and test in Europe (DATE\u201998)","author":"C Eijk van","year":"1998","unstructured":"van Eijk C (1998) Sequential equivalence checking without state space traversal. In: Int. conf. on design automation and test in Europe (DATE\u201998). IEEE Computer Society, Los Alamitos"},{"key":"81_CR62","doi-asserted-by":"crossref","unstructured":"Voronov A, \u00c5kesson K (2008) Supervisory control using satisfiability solvers. In: Proceedings of the 9th international workshop on discrete event systems. WODES08, pp 81\u201386","DOI":"10.1109\/WODES.2008.4605926"},{"key":"81_CR63","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/3-540-63104-6_28","volume-title":"International conference on automated deduction, CADE-14","author":"H Zhang","year":"1997","unstructured":"Zhang H (1997) Sato: an efficient propositional prover. In: International conference on automated deduction, CADE-14. LNCS, vol 1249. Springer, New York, pp 272\u2013275"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-009-0081-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10626-009-0081-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-009-0081-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,12]],"date-time":"2025-02-12T01:27:59Z","timestamp":1739323679000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10626-009-0081-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,9,10]]},"references-count":63,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,12]]}},"alternative-id":["81"],"URL":"https:\/\/doi.org\/10.1007\/s10626-009-0081-8","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"value":"0924-6703","type":"print"},{"value":"1573-7594","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,9,10]]}}}