×

zbMATH — the first resource for mathematics

The state of SAT. (English) Zbl 1121.68108
Summary: The papers in this special issue originated at SAT 2001, the Fourth International Symposium on the Theory and Applications of Satisfiability Testing. This foreword reviews the current state of satisfiability testing and places the papers in this issue in context.

MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Achlioptas, D.; Beame, P.; Molloy, M., A sharp threshold in proof complexity, (), 337-346 · Zbl 1323.03088
[2] D. Achlioptas, C.P. Gomes, H.A. Kautz, B. Selman, Generating satisfiable problem instances, in: AAAI/IAAI, 2000, pp. 256-261.
[3] Achlioptas, D.; Kirousis, L.M.; Kranakis, E.; Krizanc, D., Rigorous results for (2\(+\)p)-sat, Theoret. comput. sci., 265, 109-129, (2001) · Zbl 0992.68073
[4] F.A. Aloul, I.L. Markov, K.A. Sakallah, Efficient symmetry breaking for boolean satisfiability, in: Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), 2003. · Zbl 1205.68366
[5] F. Aloul, A. Ramani, I. Markov, K. Sakallah, Generic ilp versus specialized 0-1 ilp: an update, in: International Conference on Computer Aided Design (ICCAD), 2002.
[6] F. Bacchus, S. Dalmao, T. Pitassi, Dpll with caching: A new algorithm for #sat and bayesian inference, 2003, Technical Report TR03-003, Electronic Cooloquium in Computational Complexity, \(\langle\)http://www.ecc.uni-trier.de/eccc/⟩. · Zbl 1182.68294
[7] F. Bacchus, J. Winter, Effective preprocessing with hyper-resolution and equality reduction, in: Proceedings of SAT-2003, 2003. · Zbl 1204.68176
[8] L. Baptista, J.P. Marques Silva, Using randomization and learning to solve hard real-world instances of satisfiability, in: Principles and Practice of Constraint Programming, 2000, pp. 489-494. · Zbl 1044.68736
[9] R.J. Bayardo Jr., R.C. Schrag, Using CST look-back techniques to solve real-world SAT instances, in: Proceedings, AAAI-97: 14th National Conference on Artificial Intelligence, 1997, pp. 203-208.
[10] P. Beame, A. Agarwal, H. Kautz, Using problem structure for efficient clause learning, in: Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing, 2003. · Zbl 1204.68210
[11] P. Beame, R. Impagliazzo, T. Pitassi, N. Segerlind, Memoization and DPLL: formula caching proof systems, in: Proceedings of the 18th Annual IEEE Conference on Computer Complexity, Aarhus, Denmark, July 2003, to appear. · Zbl 1322.68175
[12] P. Beame, R. Impagliazzo, T. Pitassi, N. Segerlind, Memoization and dpll: formula caching proof systems, in: IEEE Conference on Computational Complexity, 2003. · Zbl 1322.68175
[13] Beame, P.; Kautz, H.; Sabharwal, A., Understanding the power of clause learning, () · Zbl 1080.68651
[14] E. Ben-Sasson, R. Impagliazzo, A. Wigderson, Near-optimal separation of treelike and general resolution, Technical Report TR00-005, Electronic Colloquium in Computation Complexity, \(\langle\)http://www.eccc.uni-trier.de/eccc/⟩, 2000. · Zbl 1063.03043
[15] E. Ben-Sasson, R. Impagliazzo, A. Wigderson, Near-optimal separation of treelike and general resolution, Technical Report TR00-005, Electronic Colloquium in Computation Complexity, \(\langle\)http://www.eccc.uni-trier.de/eccc/⟩, 2000. · Zbl 1063.03043
[16] C. Bessiere, E. Hebrard, T. Walsh, Local consistencies in sat, in: Proceedings of SAT-2003, 2003. · Zbl 1204.68184
[17] Biere, A.; Cimatti, A.; Clarke, E.M.; Zhu, Y., Symbolic model checking without bdds, (), 193-207
[18] P. Bjesse, T. Leonard, A. Mokkedem, Finding bugs in an alpha microprocessor using satisfiability solvers, in: Proceedings of the 13th International Conference on Computer Aided Verification, 2001. · Zbl 0996.68578
[19] Bollobas, B.; Borgs, C.; Chayes, J.T.; Han Kim, J.; Wilson, D.B., The scaling window of the 2sat transition, Rand. struct. alg., 18, 301, (2001)
[20] Bonet, M.L.; Esteban, J.L.; Galesi, N.; Johansen, J., On the relative complexity of resolution refinements and cutting planes proof systems, SIAM J. comput., 30, 5, 1462-1484, (2000) · Zbl 0976.03062
[21] Bonet, M.L.; Galesi, N., A study of proof search algorithms for resolution and polynomial calculus, (), 422-432
[22] J.A. Boyan, A.W. Moore, Learning evaluation functions for global optimization and Boolean satisfiability, in: Proceedings of the Fifteenth National Conference on Artificial Intelligence (AAAI-98), 1998, pp. 3-10.
[23] R.I. Brafman, A simplifier for propositional formulas with many binary clauses, in: Proceedings of IJCAI-2001, 2001, pp. 515-520.
[24] Burch, J.R.; Clarke, E.M.; McMillan, K.L.; Dill, D.L.; Hwang, L.J., Symbolic model checking: \(10^{20}\) states and beyond, Inform. comput., 98, 2, 142-170, (1992) · Zbl 0753.68066
[25] H. Chen, C. Gomes, B. Selman, Formal models of heavy-tailed behavior in combinatorial search, in: Principles and Practices of Constraint Programming (CP-01), 2001. · Zbl 1067.68620
[26] Chvatal, V.; Szemeredi, E., Many hard examples for resolution, J. ACM, 35, 4, 208-759, (1988) · Zbl 0712.03008
[27] Clarke, E.M.; Biere, A.; Raimi, R.; Zhu, Y., Bounded model checking using satisfiability solving, Formal methods in system design, 19, 1, 7-34, (2001) · Zbl 0985.68038
[28] S. Cook, D. Mitchell. Finding hard instances of the satisfiability problem: a survey, in: DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 35, 1997, pp. 1-17. · Zbl 0889.68073
[29] Cook, S.A.; Reckhow, R.A., The relative efficiency of propositional proof systems, J. symbolic logic, 44, 1, 36-50, (1977) · Zbl 0408.03044
[30] J. Crawford, M. Ginsberg, E. Luks, A. Roy, Symmetry-breaking predicates for search problems, in: Proceedings of International Conference Principles of Knowledge Representation and Reasoning, 1996, pp. 148-159.
[31] J.M. Crawford, M.J. Kearns, R.E. Schapire, The minimal disagreement parity problem as a hard satisfiability problem, 1995, unpublished manuscript.
[32] Davis, R., Diagnostic reasoning based on structure and behavior, Artif. intell., 24, 347-410, (1984)
[33] Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem proving, Commun. ACM, 5, 394-397, (1962) · Zbl 0217.54002
[34] Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem proving, Commun. ACM, 5, 394-397, (1979) · Zbl 0217.54002
[35] Davis, M.; Putnam, H., A computing procedure for quantification theory, J. ACM, 7, (1960) · Zbl 0212.34203
[36] O. Dubois, G. Dequen, A backbone-search heuristic for efficient solving of hard 3-sat formulae, in: Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI ’01), 2001.
[37] Dubois, O.; Monasson, R.; Selman, B.; Zecchina, R., Phase transitions in combinatorial problems (special issue), Theoret. comput. sci., 265, (2001)
[38] M. Ernst, T.D. Millstein, D.S. Weld, Automatic SAT-compilation of planning problems, in: IJCAI, 1997, pp. 1169-1177.
[39] Frank, J.; Cheeseman, P.; Stutz, J., When gravity fails: local search topology, J. artif. intell. res., 7, 249-281, (1997) · Zbl 0894.68041
[40] Friedgut, E., Sharp thresholds of graph properties, and the k-sat problem, J. amer. math. soc., 12, 1017-1054, (1999) · Zbl 0932.05084
[41] Gent, I.; Walsh, T., Easy problems are sometimes hard, Artif. intell., 70, 335-345, (1993) · Zbl 0824.68107
[42] M.L. Ginsberg, A.J. Parkes, A. Roy, Supermodels and robustness, in: AAAI/IAAI, 1998, pp. 334-339.
[43] E. Goldberg, Y. Novikov, Berkmin: a fast and robust sat solver, in: Proceedings of Design Automation and Test in Europe (DATE) 2002, 2002, pp. 142-149. · Zbl 1121.68106
[44] C.P. Gomes, B. Selman, Problem structure in the presence of perturbations, in: Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI-97), AAAI Press, New Providence, RI, 1997, pp. 221-227.
[45] Gomes, C.; Selman, B., Satisfied with physics (perspective article), Science, 297, 784-785, (2002)
[46] Gomes, C.P.; Selman, B.; Crato, N.; Kautz, H., Heavy-tailed phenomena in satisfiability and constraint satisfaction problems, J. automated reason., 24, 1-2, 67-100, (2000) · Zbl 0967.68145
[47] C.P. Gomes, B. Selman, H. Kautz, Boosting combinatorial search through randomization, in: Proceedings of the 15th National Conference on Artificial Intelligence (AAAI-98), 1998, pp. 431-438.
[48] D. Habet, C.M. Li, L. Devendeville, M. Vasquez, A hybrid approach for sat, in: Proceedings of the Eighth International Conference on Principles and Practice of Constraint Programming (CP’2002), Lecture Notes in Computer Science, Ithaca (NY), Springer, Berlin, 2002, pp. 172-184.
[49] Haken, A., The intractability of resolution, Theoret. comput. sci., 39, 297-308, (1985) · Zbl 0586.03010
[50] E.A. Hirsch, A. Kojevnikov, Unitwalk: a new sat solver that uses local search guided by unit clause elimination, in: PDMI preprint 9/2001, Steklov Institute of Mathematics at St. Petersburg, 2001. · Zbl 1100.68621
[51] T. Hogg, B . Huberman, C. Williams (Eds.), Phase transitions and complexity (special issue), Artif. Intell. 81 (1-2) (1996).
[52] Hooker, J., Resolution vs. cutting plane solution of inference problems: some computational experience, Oper. res. lett., 7, 1-7, (1988) · Zbl 0639.90070
[53] H. Hoos, Stochastic local search—methods, models, applications, Ph.D. Thesis, TU Darmstadt, 1998.
[54] H. Hoos, On the run-time behaviour of stochastic local search algorithms for SAT, in: Proceedings of AAAI-99, AAAI Press, New York, 1999, pp. 661-666.
[55] E. Horvitz, Y. Ruan, C. Gomes, H. Kautz, B. Selman, M. Chickering, A Bayesian approach to tackling hard computational problems, in: Proceedings of the 17th Conference on Uncertainty in Artificial Intelligence (UAI-2001), 2001. · Zbl 0991.68564
[56] D. Johnson, Experimental analysis of algorithms: the good, the bad, and the ugly, 1996, Invited Lecture, AAAI-96, Portland, OR. See also \(\langle\)http://www.research.att.com/dsj/papers/exper.ps⟩.
[57] D.S. Johnson, M.A. Trick (Ed.), Cliques, Coloring and Satisfiability: Second DIMACS Implementation Challenge, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, AMS, Providence, RI, 1996. · Zbl 0875.68678
[58] A.P. Kamath, N.K. Karmarker, K.G. Ramakrishnan, M.G.C. Resende, Computational experience with an interior point algorithm on the satisfiability problem, in: Proceedings of Integer Programming and Combinatorial Optimization, 1990. · Zbl 0716.90083
[59] H.A. Kautz, D.A. McAllester, B. Selman, Encoding plans in propositional logic, in: Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning, Boston, MA, November 1996, pp. 374-384.
[60] H. Kautz, B. Selman, Pushing the envelope: planning, propositional logic, and stochastic search, in: Proceedings of the 13th AAAI, 1996, pp. 1194-2001.
[61] H.A. Kautz, B. Selman, Unifying SAT-based and graph-based planning, in: Proceedings of the 16th International Joint Conference on Artificial Intelligence, Stockholm, Sweden, August 1999, pp. 318-325.
[62] de Kleer, J.; Williams, B.C., Diagnosing multiple faults, Artif. intell., 32, 1, 97-130, (1987) · Zbl 0642.94045
[63] Krishnamurthy, B., Short proofs for tricky formulas, Acta informatica, 22, 253-275, (1985) · Zbl 0552.03009
[64] D. Le Berre, L. Simon, The essentials of the sat’03 competition, 2003, Under review, Draft available at \(\langle\)http://www.lri.fr/∼simon/contest03/results/⟩. · Zbl 1204.68203
[65] C.M. Li, Integrating equivalency reasoning into davis-putnam procedure, in: Proceedings of the National Conference on Artificial Intelligence, 2000, pp. 291-296.
[66] C.M. Li, S. Gerard, On the limit of branching rules for hard random unsatisfiable 3-sat, in: Proceedings of ECAI, 2000. · Zbl 1029.68081
[67] X.Y. Li, M. Stallman, F. Brglez, Qingting: a local search sat solver using an effective switching strategy and efficient unit propagation, in: Proceedings of SAT-2003, 2003.
[68] M. Luby, A. Sinclair, D. Zuckerman, Optimal speedup of las vegas algorithms, Inform. Process. Lett. (1993), 173-180. · Zbl 0797.68139
[69] J.P. Marques-Silva, An overview of backtrack search satisfiability algorithms, in: Fifth International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida, January 1998.
[70] Marques-Silva, J.P.; Sakallah, K.A., GRASP—a new search algorithm for satisfiability, (), 220-227
[71] Martin, O.; Monasson, R.; Zecchina, R., Statistical mechanics methods and phase transitions in optimization problems, Theoret. comput. sci., 265, (2001) · Zbl 1032.90075
[72] F. Massacci, Using walk-SAT and rel-sat for cryptographic key search, in: Proceedings of IJCAI-99, pp. 290-295.
[73] B. Mazure, L. Sais, E. Gregoire, Boosting complete techniques thanks to local search methods, in: Proceedings of Mathematics and Artificial Intelligence, 1996. · Zbl 0905.68143
[74] McMillan, K.L., Symbolic model checking, (1993), Kluwer Academic Publishers Dordrecht · Zbl 1132.68474
[75] Mézard, M.; Parisi, G.; Zecchina, R., Analytic and algorithmic solution of random satisfiability problems, Science, 297, 812, (2002)
[76] D.G. Mitchell, B. Selman, H.J. Levesque, Hard and easy distributions for SAT problems, in: Proceedings of the Tenth National Conference on Artificial Intelligence, 1992, pp. 459-465.
[77] Monasson, R.; Zecchina, R.; Kirkpatrick, S.; Selman, B.; Troyansky, L., Determining computational complexity from characteristic phase transitions, Nature, 400, 8, 133-137, (1999) · Zbl 1369.68244
[78] P. Morris, The breakout method for escaping from local minima, in: Proceedings of AAAI-93, 1993, pp. 40-45.
[79] Moskewicz, M.W.; Madigan, C.F.; Zhao, Y.; Zhang, L.; Malik, S., Chaffengineering an efficient SAT solver, (), 530-535
[80] R. Ostrowski, E. Grigoire, B. Mazure, L. Sais, Recovering and exploiting structural knowledge from cnf formulas, in: Proceedings of the Eighth International Conference on Principles and Practice of Constraint Programming (CP’2002), Lecture Notes in Computer Science, Ithaca (NY), Springer, Berlin, 2002, pp. 185-199.
[81] A. Parkes, Pb-lib: the pseudo-boolean library, 2003.
[82] R. Paturi, P. Pudlak, F. Zane, Satisfiability coding lemma. in: Proceedings of the 38th Annual IEEE Symposium on Foundations of Computer Science, FOCS’97, 1997, pp. 566-574. · Zbl 0940.68049
[83] Phase transitions and algorithmic complexity ipam, July 2002, \(\langle\)www.ipam.ucla.edu/programs/ptac2002/ptac2002-schedule.html⟩.
[84] S.D. Prestwich, Randomised backtracking for linear pseudo-boolean constrainty problems, in: Proceedings of AI-OR-CP, 2002.
[85] S. Prestwich, Local search on sat-encoded csps, in: Proceedings of SAT-2003, 2003. · Zbl 1204.68208
[86] Y. Ruan, E. Horvitz, H. Kautz, Restart policies with dependence among runs: a dynamic programming approach, in: Principles and Practice of Constraint Programming—CP 2002, 2002.
[87] Y. Ruan, E. Horvitz, H. Kautz, Hardness-aware restart policies, 2003, under review.
[88] D. Schuurmans, F. Southey, Local search characteristics of incomplete SAT procedures, in: Proceedings of the Seventeenth National Conference on Artificial Intelligence (AAAI-2000), 2000, pp. 297-302. · Zbl 0983.68180
[89] B. Selman, H. Kautz, An empirical study of greedy local search for satisfiability testing, in: Proceedings of AAAI-93, 1993, pp. 46-51.
[90] B. Selman, H. Kautz, B. Cohen, Local search strategies for satisfiability testing, in: Dimacs Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, AMS, Providence, RI, 1996, pp. 521-532. · Zbl 0864.90093
[91] B. Selman, H.A. Kautz, D.A. McAllester, Ten challenges in propositional reasoning and search, in: Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI’97), 1997, pp. 50-54.
[92] B. Selman, H. Levesque, D. Mitchell, Gsat: a new method for solving hard satisfiability problems, in: Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI-92), AAAI Press, San Jose, CA, 1992, pp. 440-446.
[93] G. Semerjian, R. Monasson, A study of pure random walk on random satisfiability problems with physical methods, in: Proceedings of SAT-2003, 2003. · Zbl 1204.68211
[94] L. Simon, D. Le Berre, E. Hirsch, The sat2002 competition, 2002, \(\langle\)http://www.satlive.org/SATCompetition/onlinereport.pdf⟩.
[95] Stallman, R.; Sussman, G., Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis, Artif. intell., 9, 2, (1977) · Zbl 0372.94024
[96] Urquhart, A., The symmetry rule in propositional logic, Discrete appl. math., 96, 177-193, (1999) · Zbl 0938.03023
[97] van Beek, P.; Dechter, R., Constraint tightness and looseness versus local and global consistency, J. ACM, 44, 4, 549-566, (1997) · Zbl 0890.68075
[98] M.N. Velev, R.E. Bryant, Effective use of boolean satisfiability procedures in the formal verification of superscalar and vliw microprocessors, in: Proceedings of the 38th Design Automation Conference (DAC ’01), 2001, pp. 226-231. · Zbl 1069.68119
[99] Wah, B.W.; Shang, Y., A discrete Langrangian-based global-search method for solving satisfiability problems, J. global optim., 12, (1998)
[100] J. Walser, Solving linear pseudo-boolean constraint problems with local search, in: Proceedings of the 14th National Conference on Artificial Intelligence (AAAI-97), 1998.
[101] Walsh, T., Search in a small world, ()
[102] T. Walsh, Reformulating propositional satisfiability as constraint satisfaction, Lecture Notes in Computer Science, vol. 1864, 2000. · Zbl 0989.68526
[103] J.P. Warners, E. de Klerk, H. van Maaren, Relaxations of the satisfiability problem using semidefinite programming, 1999. · Zbl 0979.68050
[104] Warners, J.; van Maaren, H., A two phase algorithm for solving a class of hard satisfiability problems, Oper. res. lett., 23, 81-88, (1999) · Zbl 0960.90100
[105] W. Wei, B. Selman, Accelerating random walks, in: Proceedings of the Eighth International Conference on the Principles and Practice of Constraint Programming (CP-2002), 2002.
[106] R. Williams, C. Gomes, B. Selman, Backdoors to typical case complexity, in: Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence (IJCAI-03), 2003.
[107] Z. Wu, B.W. Wah, Trap escaping strategies in discrete lagrangian methods for solving hard satisfiability and maximum satisfiability problems, in: Proceedings of AAAI-99, 1999, pp. 673-678.
[108] H. Zhang, SATO: an efficient propositional prover, in: Proceedings of the International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 1249, July 1997, pp. 272-275.
[109] Zhang, L.; Madigan, C.F.; Moskewicz, M.H.; Malik, S., Efficient conflict driven learning in a Boolean satisfiability solver, (), 279-285
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.