Abstract
The SAT 2003 Competition ran in February – May 2003, in conjunction with SAT’03 (the Sixth Fifth International Symposium on the Theory and Applications of Satisfiability Testing). One year after the SAT 2002 competition, it was not clear that significant progress could be made in the area in such a little time. The competition was a success – 34 solvers and 993 benchmarks, needing 522 CPU days – with a number of brand new solvers. Several 2003 competitors were even able to solve within 15mn benchmarks remained unsolved within 6 hours by 2002 competitors. We report here the essential results of the competition, interpret and statistically analyse them, and at last provide some suggestions for the future competitions.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Sixth International Conference on Theory and Applications of Satisfiability Testing, S. Margherita Ligure - Portofino ( Italy) (May 2003)
Alexander, N.: Backtrack search algorithms for propositional satisfiability: Review and innovations. Master’s thesis, Hebrew University of Jerusalem (November 2002)
Audemard, G., Le Berre, D., Roussel, O., Lynce, I., Marques Silva, J.P.: Open- SAT: An Open Source SAT Software Project. In: Proc. of SAT 2003 [1] (2003)
Dequen, G., Dubois, O.: Renormalization as a function of clause lengths for solving random k-sat formulae. In: Proceedings of Fifth International Symposium on Theory and Applications of Satisfiability Testing, pp. 130–132 (2002)
Dubois, O., Dequen, G.: A backbone-search heuristic for efficient solving of hard 3-sat formulae. In: Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI 2001), Seattle, Washington, USA, August 4-10 (2001)
Eén, N., Sörensson, N.: An extensible SAT solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Goldberg, E., Novikov, Y.: BerkMin: A fast and robust SAT-solver. In: Design, Automation, and Test in Europe (DATE 2002), March 2002, pp. 142–149 (2002)
Hirsch, E.A., Kojevnikov, A.: UnitWalk: A new SAT solver that uses local search guided by unit clause elimination. PDMI preprint 9/2001, Steklov Institute of Mathematics at St.Petersburg (2001)
Kullmann, O.: Heuristics for SAT algorithms: Searching for some foundations (September 1998)
Leyton-Brown, K., Nudelman, E., Andrew, G., McFadden, J., Shoham, Y.: A portfolio approach to algorithm selection. In: Proceedings of IJCAI 2003 (2003)
Leyton-Brown, K., Nudelman, E., Shoham, Y.: Learning the empirical hardness of optimization problems: The case of combinatorial auctions. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, p. 556. Springer, Heidelberg (2002)
Li, X.Y., Stallmann, M.F., Brglez, F.: QingTing: A Fast SAT Solver Using Local Search and Efficient Unit Propagation. In: Proc. of SAT 2003 [1] (2003)
Lynce, I., Marques Silva, J.: On implementing more efficient data structures. In: Proc. of SAT 2003 [1] (2003)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC 2001), June 2001, pp. 530–535 (2001)
Ostrowski, R., Grégoire, E., Mazure, B., Sais, L.: Recovering and exploiting structural knowledge from cnf formulas. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 185–199. Springer, Heidelberg (2002)
Prestwich, S.D.: Randomised backtracking for linear pseudo-boolean constraint problems. In: Proc. of 4th Int. Workshop on Integration of AI and OR techniques in CP for Combinatorial Optimisation Problems (2002)
Selman, B., Kautz, H.A., McAllester, D.A.: Ten challenges in propositional reasoning and search. In: Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI 1997), pp. 50–54 (1997)
Simon, L., Chatalic, P.: SATEx: a web-based framework for SAT experimentation. In: Kautz, H., Selman, B. (eds.), June 2001. Electronic Notes in Discrete Mathematics, vol. 9, Elsevier Science Publishers, Amsterdam (2001)
Simon, L., Berre, D.L., Hirsch, E.E.: The sat 2002 competition report. Annals of Mathematics and Artificial Intelligence, Special issue for SAT 2002 (2003) (to appear)
Sutcliff, G., Suttner, C.: Evaluating general purpose automated theorem proving systems. Artificial Intelligence 131, 39–54 (2001)
Zhang, H.: SATO: an efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 272–275. Springer, Heidelberg (1997)
Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: International Conference on Computer-Aided Design (ICCAD 2001), November 2001, pp. 279–285 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Le Berre, D., Simon, L. (2004). The Essentials of the SAT 2003 Competition. In: Giunchiglia, E., Tacchella, A. (eds) Theory and Applications of Satisfiability Testing. SAT 2003. Lecture Notes in Computer Science, vol 2919. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24605-3_34
Download citation
DOI: https://doi.org/10.1007/978-3-540-24605-3_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20851-8
Online ISBN: 978-3-540-24605-3
eBook Packages: Springer Book Archive