{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T09:50:58Z","timestamp":1773481858781,"version":"3.50.1"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"8","license":[{"start":{"date-parts":[[2009,8,1]],"date-time":"2009-08-01T00:00:00Z","timestamp":1249084800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2009,8]]},"abstract":"<jats:p>Satisfiability solvers can now be effectively deployed in practical applications.<\/jats:p>","DOI":"10.1145\/1536616.1536637","type":"journal-article","created":{"date-parts":[[2009,7,21]],"date-time":"2009-07-21T13:32:11Z","timestamp":1248183131000},"page":"76-82","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":122,"title":["Boolean satisfiability from theoretical hardness to practical success"],"prefix":"10.1145","volume":"52","author":[{"given":"Sharad","family":"Malik","sequence":"first","affiliation":[{"name":"Princeton University, Princeton, NJ"}]},{"given":"Lintao","family":"Zhang","sequence":"additional","affiliation":[{"name":"Microsoft Research Asia, Beijing, China"}]}],"member":"320","published-online":{"date-parts":[[2009,8]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"R., Seshia, S., and Tinelli, C. Satisfiability modulo theories","author":"Barrett C.","year":"2009","unstructured":"]] Barrett , C. , sebastiani , R., Seshia, S., and Tinelli, C. Satisfiability modulo theories . A. Biere, H. van Maaren, T. Walsh, Eds. Handbook of Satisfiability 4, 8 ( 2009 ), IOS Press , Amsterdam. ]]Barrett, C., sebastiani, R., Seshia, S., and Tinelli, C. Satisfiability modulo theories. A. Biere, H. van Maaren, T. Walsh, Eds. Handbook of Satisfiability 4, 8 (2009), IOS Press, Amsterdam."},{"key":"e_1_2_1_2_1","volume-title":"National Conference on Artificial Intelligence","author":"Bayardo R.","year":"1997","unstructured":"]] Bayardo R. , and Schrag , R . Using CSP look-back techniques to solve real-world SAT instances . National Conference on Artificial Intelligence , 1997 . ]]Bayardo R., and Schrag, R. Using CSP look-back techniques to solve real-world SAT instances. National Conference on Artificial Intelligence, 1997."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/646483.691738"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.v27:2"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_6_1","volume-title":"Model Checking","author":"Clarke E.M.","year":"1999","unstructured":"]] Clarke , E.M. , Grumberg , O. , and Peled , D.A . Model Checking . MIT Press , Cambridge, MA , 1999 . ]]Clarke, E.M., Grumberg, O., and Peled, D.A. Model Checking. MIT Press, Cambridge, MA, 1999."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/647770.734252"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_5"},{"key":"e_1_2_1_12_1","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"Garey M.R.","year":"1979","unstructured":"]] Garey , M.R. , and Johnson , D.S . Computers and Intractability: A Guide to the Theory of NP-Completeness . W. H. Freeman , 1979 ]]Garey, M.R., and Johnson, D.S. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, 1979"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of National Conference on Artificial Intelligence","author":"Gomes C. P.","year":"1998","unstructured":"]] Gomes , C. P. , Selman , B. , and Kautz , H . Boosting combinatorial search through randomization . In Proceedings of National Conference on Artificial Intelligence ( Madison, WI , 1998 ). ]]Gomes, C. P., Selman, B., and Kautz, H. Boosting combinatorial search through randomization. In Proceedings of National Conference on Artificial Intelligence (Madison, WI, 1998)."},{"key":"e_1_2_1_14_1","unstructured":"]]Hamadi Y. Jabbour S. and Sais L. ManySat: Solver description. Microsoft Research TR-2008-83.  ]]Hamadi Y. Jabbour S. and Sais L. ManySat: Solver description. Microsoft Research TR-2008-83."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/975331"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1333874.1334161"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/347324.383378"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2007.10.007"},{"key":"e_1_2_1_20_1","volume-title":"European Conference on Artificial Intelligence","author":"Kautz H.","year":"1992","unstructured":"]] Kautz , H. and Selman , B . Planning as satisfiability . European Conference on Artificial Intelligence , 1992 . ]]Kautz, H. and Selman, B. Planning as satisfiability. European Conference on Artificial Intelligence, 1992."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.108614"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the Genetic and Evolutionary Computation Conference","author":"Marchiori E.","year":"1999","unstructured":"]] Marchiori , E. and Rossi , C . A flipping genetic algorithm for hard 3-SAT problems . In Proceedings of the Genetic and Evolutionary Computation Conference ( Orlando, FL , 1999 ), 393--400. ]]Marchiori, E. and Rossi, C. A flipping genetic algorithm for hard 3-SAT problems. In Proceedings of the Genetic and Evolutionary Computation Conference (Orlando, FL, 1999), 393--400."},{"key":"e_1_2_1_24_1","volume-title":"IEEE International Conference on Tools with Artificial Intelligence","author":"Marques-Silva J.P","year":"1996","unstructured":"]] Marques-Silva , J.P , and Sakallah , K.A . Conflict analysis in search algorithms for propositional satisfiability . IEEE International Conference on Tools with Artificial Intelligence , 1996 . ]]Marques-Silva, J.P, and Sakallah, K.A. Conflict analysis in search algorithms for propositional satisfiability. IEEE International Conference on Tools with Artificial Intelligence, 1996."},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the 14th National Conference on Artificial Intelligence","author":"Mazure B.","year":"1997","unstructured":"]] Mazure , B. , Sas L. , and Grgoire , E ., Tabu search for SAT . In Proceedings of the 14th National Conference on Artificial Intelligence ( Providence, RI , 1997 ). ]]Mazure, B., Sas L., and Grgoire, E., Tabu search for SAT. In Proceedings of the 14th National Conference on Artificial Intelligence (Providence, RI, 1997)."},{"key":"e_1_2_1_26_1","series-title":"Lecture Notes In Computer Science 2404","volume-title":"Proceedings of the 14th International Conference on Computer Aided Verification","author":"McMillan K.L.","year":"2002","unstructured":"]] McMillan , K.L. , Applying SAT methods in unbounded symbolic model checking . In Proceedings of the 14th International Conference on Computer Aided Verification . Lecture Notes In Computer Science 2404 ( 2002 ). Springer-Verlag , London , 250--264. ]]McMillan, K.L., Applying SAT methods in unbounded symbolic model checking. In Proceedings of the 14th International Conference on Computer Aided Verification. Lecture Notes In Computer Science 2404 (2002). Springer-Verlag, London, 250--264."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(98)00068-X"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/296399.296450"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10922-008-9108-y"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 12th National Conference on Artificial Intelligence","author":"Selman B.","year":"1994","unstructured":"]] Selman , B. , Kautz , H.A. , and Cohen , B . Noise strategies for improving local search . In Proceedings of the 12th National Conference on Artificial Intelligence ( Seattle, WA , 1994 ). American Association for Artificial Intelligence, Menlo Park, CA, 337--343. ]]Selman, B., Kautz, H.A., and Cohen, B. Noise strategies for improving local search. In Proceedings of the 12th National Conference on Artificial Intelligence (Seattle, WA, 1994). American Association for Artificial Intelligence, Menlo Park, CA, 337--343."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/1867135.1867203"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775945"},{"key":"e_1_2_1_33_1","volume-title":"Second DIMACS Implementation Challenge. DIMACS Series in Discrete Mathematics and Theoretical Computer Science","author":"Spears W.M.","year":"1993","unstructured":"]] Spears , W.M. Simulated annealing for hard satisfiability problems. Cliques, Coloring and Satisfiability , Second DIMACS Implementation Challenge. DIMACS Series in Discrete Mathematics and Theoretical Computer Science . D.S. Johnson and M.A. Trick, Eds. American Mathematical Society ( 1993 ), 533--558. ]]Spears, W.M. Simulated annealing for hard satisfiability problems. Cliques, Coloring and Satisfiability, Second DIMACS Implementation Challenge. DIMACS Series in Discrete Mathematics and Theoretical Computer Science. D.S. Johnson and M.A. Trick, Eds. American Mathematical Society (1993), 533--558."},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the 1996 International Conference on Neural Networks, 1121--1126","author":"Spears W. M.","unstructured":"]] Spears , W. M. A NN algorithm for Boolean satisfiability problems . In Proceedings of the 1996 International Conference on Neural Networks, 1121--1126 . ]]Spears, W. M. A NN algorithm for Boolean satisfiability problems. In Proceedings of the 1996 International Conference on Neural Networks, 1121--1126."},{"key":"e_1_2_1_35_1","first-page":"5276897","article-title":"A system for determining prepositional logic theorems by applying values and rules to triplets that are generated from a formula","author":"St\u00e5lmarck G","year":"1994","unstructured":"]] St\u00e5lmarck , G . A system for determining prepositional logic theorems by applying values and rules to triplets that are generated from a formula . U.S. Patent Number 5276897 , 1994 . ]]St\u00e5lmarck, G. A system for determining prepositional logic theorems by applying values and rules to triplets that are generated from a formula. U.S. Patent Number 5276897, 1994.","journal-title":"U.S. Patent Number"},{"key":"e_1_2_1_36_1","volume-title":"Studies in Constructive Mathematics and Mathematical Logic, Part 2","author":"Tseitin G.","year":"1968","unstructured":"]] Tseitin , G. On the complexity of derivation in propositional calculus . In Studies in Constructive Mathematics and Mathematical Logic, Part 2 ( 1968 ), 115--125. Reprinted in Automation of reasoning vol. 2 . J. Siekmann and G. Wrightson, Eds. Springer Verlag , Berlin, 1983, 466--483. ]]Tseitin, G. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, Part 2 (1968), 115--125. Reprinted in Automation of reasoning vol. 2. J. Siekmann and G. Wrightson, Eds. Springer Verlag, Berlin, 1983, 466--483."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/1630659.1630827"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the International Conference on Theory and Applications of Satisfiability Testing","author":"Williams R.","year":"2003","unstructured":"]] Williams , R. , Gomes , C. , and Selman , B . On the connections between heavy-tails, backdoors, and restarts in combinatorial search . In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing , 2003 . ]]Williams, R., Gomes, C., and Selman, B. On the connections between heavy-tails, backdoors, and restarts in combinatorial search. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, 2003."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622673.1622687"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the 5th International Symposium on Theory and Applications of Satisfiability Testing.","author":"Zhang H.","year":"2002","unstructured":"]] Zhang , H. Generating college conference basketball schedules by a SAT solver . In Proceedings of the 5th International Symposium on Theory and Applications of Satisfiability Testing. ( Cincinnati, OH , 2002 ). ]]Zhang, H. Generating college conference basketball schedules by a SAT solver. In Proceedings of the 5th International Symposium on Theory and Applications of Satisfiability Testing. (Cincinnati, OH, 2002)."}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1536616.1536637","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1536616.1536637","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:38:52Z","timestamp":1750253932000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1536616.1536637"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,8]]},"references-count":39,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2009,8]]}},"alternative-id":["10.1145\/1536616.1536637"],"URL":"https:\/\/doi.org\/10.1145\/1536616.1536637","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,8]]},"assertion":[{"value":"2009-08-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}