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
| 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 |
Topics
| 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
Sponsors
Quick Links
Abstracts and activities
Probable program
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: franco@gauss.ececs.uc.edu |
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 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.Rationale
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.Program
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 .
Submissions
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.
Proceedings
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:
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.Registration
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:
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 Articles
To be announced.Cost
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.
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