Updated 15 May 2002

SAT 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

Organizing Committee
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

Program Committee
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

Invited Speakers
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.

Important Dates
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.


Quick Links

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)


Contact address

John Franco
University of Cincinnati
Cincinnati, Ohio 45221-0030
tel: +513 556 1817
fax: +513 556 7326
e-mail: franco@gauss.ececs.uc.edu


Conference Center

Kingsgate Conference Center
University of Cincinnati
151 Goodman Drive
Cincinnati, Ohio 45219
tel: +513 487 3800
fax: +513 487 3810

Travel Information
Click Here for Details

University of Cincinnati Cincinnati Subway Site Cincinnati Zoo Ault Park Observatory Eden Park Mount Adams Art Museum Cincinnati Airport Riverboat Gambling Loveland Castle Downtown Cincinnati

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 conference

The 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.


Great 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 conference

The 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.


Here 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 .


Article 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.


Electronic 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 Competition

The 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
Competition Discussion

QBF Mini-Workshop

There 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.


All persons attending are requested to register using the online registration form.

Attendees not Submitting an Extended Abstract

If you wish to participate in the conference but not submit an abstract may register using the online registration form.

Guidelines for Extended Abstracts

Extended 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 franco@gauss.ececs.uc.edu with the following information:
      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 Articles

To be announced.


The 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.

Special Concerns

It is time for us to inquire on special wishes you might have and to focus on some extra facilities:

Local Environment

Unlike 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