Updated 15 May 2002
Fifth International Symposium on the
Theory and Applications of Satisfiability Testing
Some of the participants waiting for the shuttle (courtesy of Renato Bruni)
May 6-9, 2002
Cincinnati, Ohio, USA
John Franco, University of Cincinnati Henry Kautz, University of Washington Hans Kleine Büning, Universität Paderborn Hans van Maaren, University of Delft Bart Selman, Cornell University Ewald Speckenmeyer. Universität Köln
Dimitris Achlioptas, Microsoft Research Endre Boros, Rutcor, Rutgers University Nadia Creignou, Université de la Méditerranée, Marseille Joe Culberson, University of Alberta, Edmonton Olivier Dubois, Université Paris 6 Thomas Eiter, Technische Universität Wien John Franco, University of Cincinnati Ian Gent, St. Andrews University Andreas Goerdt, Technische Universität Chemnitz Edward A. Hirsch, Steklov Institute of Mathematics at St. Petersburg Holger Hoos, University of British Columbia Russell Impagliazzo, UC San Diego Henry Kautz, University of Washington Lefteris Kirousis, University of Patras Hans Kleine Büning, Universität Paderborn Oliver Kullmann, University of Wales Swansea Daniel Le Berre, CRIL, Université d'Artois Chu-Min Li, LaRIA, Université de Picardie Jules Verne Hans van Maaren, University of Delft Paul W. Purdom, Indiana University Bart Selman, Cornell University Ewald Speckenmeyer, Universität Köln Allen Van Gelder, UC Santa Cruz Miroslav N. Velev, Carnegie Mellon University Toby Walsh, University of York Lintao Zhang, Princeton University
Edmund Clarke, Carnegie Mellon University João Marques-Silva, Instituto Superior Técnico, Universidade Técnica de Lisboa Uwe Schöning, Universität Ulm
SAT Solver Competition (BDD packages welcome)
Laurent Simon, LRI Laboratory, Université Paris-Sud Daniel Le Berre, CRIL, Université d'Artois Edward A. Hirsch, Steklov Institute of Mathematics at St. Petersburg
Special Mini-Workshop on QBF
Enrico Giunchiglia, Università di Genova Toby Walsh, University of York
Several aspects of Satisfiability testing will be explored including: propositional proof systems, search techniques, relationship between BDDs and search, applications such as in formal verification, probabilistic analysis of SAT algorithms and SAT properties, upper bounds on SAT algorithm performance, specific solvers, empirical results, quantified boolean formulas, and related topics.
Submission of extended abstracts: February 6, 2002. Submission of SAT solvers: March 10, 2002 (new). Submission of SAT benchmarks: March 24, 2002 (new). Decisions on extended abstracts returned: March 6, 2002. Buggy solvers returned: March 24, 2002 (new). Bugfixes for solvers: March 31, 2002 (new). SAT Solver Competition: Starting April 6, 2002, until the conference. Requests to participate without submission: April 10, 2002. Second stage of competition begins: May 6, 2002. Competition results and awards: May 9, 2002. Conference: May 6 - 9, 2002. Submission of final journal articles: May 30, 2002.
Abstracts and activities Probable program
Submitted SAT solvers
QBF Panel Summary (19 Jun) List of participants Cincinnati Weather
May 12 - Presentation of Edmund Clarke is now posted under "Abstracts and activities"
May 14 - Presentation of João Marques-Silva is now posted under "Abstracts and activities"
News, updates, general information
Hotel and transportation information. Answers to questions raised when registering. More. Last update 1 May.
(Note late breaking information for Executive Shuttle users)
John Franco ECECS University of Cincinnati Cincinnati, Ohio 45221-0030 USA tel: +513 556 1817 fax: +513 556 7326 e-mail: email@example.com
Kingsgate Conference Center University of Cincinnati 151 Goodman Drive Cincinnati, Ohio 45219 USA tel: +513 487 3800 fax: +513 487 3810
Click Here for Details
Click on the square marked UC for a more detailed view of the local area
Views of the University Campus
Architectural Tour of Cincinnati
Cincinnati has a Castle...
...but it is too small for us.
Note: The first three workshops were held in European castles and the fourth in Boston which is beautiful enough to be called a castle
History of the conferenceThe conference follows the 1st, 2nd, and 3rd Workshops on Satisfiability held in Siena (1996), Paderborn (1998), and Renesee (2000) (here is an interactive photo of the participants), and the workshop on Theory and Applications of Satisfiability Testing held in Boston (2001). Attendence at the workshops has been invited and has steadily increased from about 20 to over 50. Moreover, the scope has broadened considerably and now includes both theoretical and application areas. All interested parties are welcome to attend this conference.
RationaleGreat strides have been made in recent years in the theory and practice of propositional satisfiability testing. On the theoretical side, a wide range of mathematical approaches -- ranging from classical combinatorial analysis to arguments based on statistical physics -- have increased our understanding of problem hardness. On the practical side, new systematic and non-systematic search algorithms have increased the size of problems that can be solved by several orders of magnitude. As a result there is growing interest in using SAT solvers as the basis for practical tools for solving real-world problems, as well as using the insights gained from SAT research to create problem-specific solutions.
Purpose of the conferenceThe aim of the conference is to bring together researchers working on both theoretical and practical aspects of the satisfiability problem. Such people can be found in many disciplines including theoretical computer science, electrical engineering, artificial intelligence, formal verification, mathematical theorem-proving, and operations research, among others. Our hope is to facilitate sharing of ideas and increase synergy between theoretical and empirical work.
ProgramHere is the list of speakers with links to the abstracts of the research that will be presented at the conference (under construction). Page numbers are consecutive, increasing across abstracts to allow citation. Printed copies of the complete set will be printed and distributed at the conference. Expect some revisions up to the date of the conference.
Here is the preliminary program .
SubmissionsArticle submissions will be of two types: extended abstracts and full length articles. The conference program will be based on extended abstracts only. Each extended abstract will be reviewed by two program committee members. Full length article submissions will be rigorously refereed and accepted articles will appear in a major journal, to be decided. Program committee members are themselves encouraged to submit extended abstracts and/or full length journal quality articles.
SAT Solver submissions: SAT solvers should be submitted in source to be compiled on a Unix-like environment determined after submission. Machine-dependent submissions are not possible. The solvers are expected to read input files in the DIMACS format. For more information see the competiton web page.
SAT Benchmarks submissions: new challenging benchmarks can be submitted either as a generator or as a set of instances in the DIMACS format. Benchmarks generators and submissions composed of a range of similar instances scaling a problem are encouraged. The program committee will not be involved in judging the competition.
ProceedingsElectronic versions of the extended abstracts will be available via the world wide web before the conference. Full length articles will be rigorously refereed and accepted articles will be published in a major journal, to be decided.
SAT Solver CompetitionThe purpose of the competition is to identify new challenging benchmarks and to promote new SAT solvers. We strongly encourage people thinking about SAT-based techniques in their area (planning, hardware or software verification, etc.) to submit benchmarks to be used for the competition. The result of the competition will be a good indicator of the current feasibility of such approach. The competition will be completely automated using the SAT-Ex system and will be made completely transparent in order to allow people from the committees of both the competition and the conference to submit their own benchmarks and solvers. An open discussion about the policy of the competition has started at the Competition Forum page. We accept both complete and incomplete solvers, to be evaluated and awarded separately.
There will be several categories of benchmarks to be decided later. Awards, by category and amounting to $2,500, will be distributed for both benchmarks and solvers.
Useful Competition Links:
Competition Home Page
QBF Mini-WorkshopThere is considerable interest at present in Quantified Boolean Formulas (QBFs) which many regard to be the next step after propositional Satisfiability. There will be a special mini-workshop, second in a series, on this topic on site, during the conference. For details see this link.
RegistrationAll persons attending are requested to register using the online registration form.
Attendees not Submitting an Extended AbstractIf you wish to participate in the conference but not submit an abstract may register using the online registration form.
Guidelines for Extended AbstractsExtended abstracts should be limited to 8 pages (postscript or pdf format, 12 pt font size) not including appendices (see below). They should be submitted electronically by February 6, 2002. The submission procedure is as follows: send an email message to firstname.lastname@example.org with the following information:
title: speaking author name: speaking author email: speaking author telephone: speaking author home page: names of coauthors: brief overview:Attach to the email a postscript or pdf file containing the extended abstract. Please name the file as follows: your first and last names separated by a dash, then with ps or pdf extension, depending on whether the file is in postscript or pdf format (e.g. henry-kautz.ps). Each extended abstract will be reviewed by at least two members of the program committee. If you think that adding mathematical detail will be important for the reviewers to make a decision, you may include those details in one or more appendices. However, please realize the reviewers are not under any obligation to look at them.
Guidelines for Full Length ArticlesTo be announced.
CostThe cost of the conference is subsidized by a fixed amount for university faculty and students and is expected to be $475 per person. This includes hotel room for four nights, three meals a day, continuous coffee, use of facilities, the excursion, parking, internet access, and so on. This figure is based on an expected turnout of 70 university participants. If many more show up, the figure will have to rise accordingly. At some point, about two months before the conference, the actual figure will be set in stone.
The cost to researchers from industry is $690 per person.
There is a bar on the premises but, of course, you will have to pay additionally for wine, beer, and other alcoholic drinks.
It is time for us to inquire on special wishes you might have and to focus on some extra facilities:
Local EnvironmentUnlike Renesse, bicycles are not available. Nor would there be a decent place to ride them even if they were: we are, after all, practically in downtown Cincinnati! However, the University has one of the best music schools in the USA and an excellent school of art housed in one of the strangest university buildings ever. So, there will probably be a number of enjoyable things to do and see on the campus if you are in need of a break. Across the street is a pleasant park called Burnet Woods where you can have a nice walk. About four blocks away is the world famous Cincinnati Zoo. About 3 Km away is Main Street which hosts most of the interesting yuppie nightlife (some nice micro-breweries are there for example) and about 4 Km away is Mount Adams which hosts the rest (and has nice views). The Art Museum is also about 4 Km away. Two charming parks, Ault Park and Eden Park, are nearby; both are worth a visit if plants make you smile. Near Ault Park you can find the University Observatory which still opens its doors to the general public. Forget about using the Cincinnati Subway - although a tunnel was built about 80 years ago, no one ever bothered to lay the track or buy the rolling stock. There is (inexpensive) city bus service to downtown and to the northern suburbs, where most of the upscale shopping is, but the bus is slow and relatively infrequent. Schedules will be posted during the conference.
The excursion, on Tuesday night, will be an old fashioned American recreational experience: a picnic at Cincinnati's Cinergy Field while watching a classic baseball game pitting the Cincinnati Reds, America's oldest professional baseball team, against the Milwaukee Brewers. Originally we were scheduled to watch the proceedings from the middle deck in a private glass-enclosed room called the Champions Room (see picture below: the group area near entry point 12). Unfortunately, due to the size of the group we have moved to the Stadium Club in right field (group area near entry point 8). The advantage of the Stadium Club is there is a lot of room to move around and have a good time. This will appeal to those people wanting to talk more than watch. The following will be served continuously, buffet style, for our enjoyment: Hot Dogs, Fried Chicken, Crudites, Fruit, Cheese, Potato Salad, String Beans, Soft Drinks, and Draft Beer. Have as much as you want. Baseball/Cricket expert Ian Gent will be on hand to explain what you see.
For those acquainted with the stadium and remembering that the seats used to completely enclose the playing area, the seating hole in left field is due to construction in progress of a new stadium to replace the existing one. This is the last year that Cinergy Field, formerly Riverfront Stadium, will exist.
Possibly Interesting Facts About the University
- Joseph Strauss, an 1892 Civil Engineering graduate of UC, designed and built the Golden Gate Bridge (why did you think the bridge is painted red?). A brick from the old McMicken Hall is cemented into the base of the south anchorage.
- Donald Shell discovered the Shell Sort algorithm while working on a Masters degree in the Mathematics Department
- Vinod Dham, chief architect of the Pentium Chip, is a graduate of the department of Electrical and Computer Engineering and Computer Science.
- Albert Sabin developed the oral polio vaccine while on the faculty at UC
- George Rieveschl Jr. discovered the first commercial antihistamine agent, known as Benadryl, while on the faculty at UC. He also holds Undergraduate, Masters, and Ph.D. degrees from UC.
- Brian Rose, a faculty member in the Classics Department, is in charge of the Troy excavations. Carl Blegen of UC established modern scientific methods in archaeology during his excavations of the Troy site which lasted six years beginning in 1932.
- Neil Armstrong, first man on the Moon, was a member of the Aerospace Engineering faculty at UC and is a graduate of the College of Engineering.
- William Howard Taft, the only US President to serve as Chief Justice of the United States, graduated from the UC Law School and served as its Dean.
- Sports greats Sandy Koufax and Oscar Robinson played for UC as students. Koufax came to UC on a basketball scholarship.
- Herman Schneider started cooperative education in the United States, as Dean of the College of Engineering, in 1906. To this day the College of Engineering requires all its graduates to have co-op training.
- Heather French, a student of Design, Art, Architecture, and Planning, is Miss America for the year 2000.
- The work of Cleveland Abbe, former director of the Cincinnati Observatory, led to the creation of the National Weather Service.
- Kathleen Battle earned Undergraduate and Masters degrees from UC's Cincinnati Conservatory of Music in the early 1970s. Recently, she was granted an honorary Doctorate as well.
- Thomas Berger, author of Little Big Man, Crazy in Berlin and the "Rhinehart" Trilogy, graduated from the College of Arts and Sciences in 1948.
- Miller Huggins, feared manager of the New York Yankees, started out with a Law Degree from UC in 1902.
- Jerry Rubin, the anti-war protestor of the 1960's, graduated from UC in 1961 before briefly attending UC, Berkeley.
- More improbable Cincinnatians to follow.
Page started: July 13 2000; last modified: May 12 2002