The IJCAI Computational Challenge
in Propositional Reasoning and Search
|
Henry Kautz
|
|
Bart Selman
|
|
University of Washington
|
|
Cornell University
|
This is a repository for challenges, problem instances, problem generators,
solvers, and benchmark results for propositional satisfiability testing,
as described in the paper:
- Bart Selman, Henry Kautz,
& David
McAllester, Ten Challenges in Propositional Reasoning and
Search, Proceedings of the Fifteenth
International Joint Conference on Artificial Intelligence (IJCAI-97),
Nagoya, Japan,1997.
- Overview of progress from IJCAI-99.
- New! Henry Kautz &
Bart Selman, Ten Challenges
Redux: Recent Progress in Propositional Reasoning and
Search. Invited paper, Ninth International
Conference on Principles and Practice of Constraint Programming (CP 2003),
Cork, Ireland, 2003.
SAT Resources
-
SATLIB, a library of info and tools
for satisfiability testing.
-
Local copy of the 1993 DIMACS Challenge Satisfiability
Testing Benchmarks.
-
The DIMACS Challenge
ftp site (for all challenges, not just satisfiability).
An extensive set of
test problems from the
Second DIMACS Implementation Challenge (1992-1993),
NP Hard Problems: Maximum Clique, Graph Coloring, and
Satisfiability. Results up to 1996 published in
Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, October
11-13, 1993, Editors: David S. Johnson and Michael A. Trick; AMS, Providence, RI, 1996.
-
Sat Live!, a collection of links
for satisfiability testing.
-
Sat-Ex, collects
a huge number of experimental results evaluating various satisfiability
solvers.
-
Douglas D. Edward's Research Summary - a good overview of SAT techniques up to 1996.
- Blackbox - A planning system based on translating problems to Boolean satisfiability. The system can be used to convert any STRIPS-style
planning problem in
PDDL notation into a CNF formula.
Responses to Challenges
Other Resources