and Niklas Sörensson| Entry Name: | The MiniSat solver, the Pseudo-boolean solver MiniSat+ and the CNF minimizer/preprocessor SatELite (winners of the 2005 SAT contest) | |
| Groups/PIs: | Niklas Eén and Niklas Sörensson | |
| Status: | available |
| Entry Name: | Pseudo-Boolean Solver and Optimizer Vallst | |
| Groups/PIs: | Daniel Vallstrom | |
| Status: | available |
| Entry Name: | SATLIB a comprehensive site on SAT | |
| Groups/PIs: | Dr. Holger H. Hoos at UBC | |
| Status: | available |
| Entry Name: | SAT 2002 contest: detailed empirical results | |
| Groups/PIs: | Laurent Simon at U. Paris Sud | |
| Status: | available |
| Entry Name: | SAT Benchmark Suites (for microprocessor verification) | |
| Groups/PIs: | Miroslav Velev at CMU | |
| Status: | available |
| Entry Name: | Executables (Win, Linux, Solaris) of the Berkmin 56.1 solver (complete) + newer versions + paper | |
| Groups/PIs: | Dr. Eugene Goldberg at Cadence Berkeley Labs | |
| Status: | available (non-commercial use only) |
| Entry Name: | The source code of the Chaff solver (complete) + a collection of papers on SATisfiability | |
| Groups/PIs: | Prof. Sharad Malik at Princeton | |
| Status: | available (non-commercial use only) |
| Entry Name: | Executables (Linux, Solaris, Windows) of the Satzoo solver | |
| Groups/PIs: | Niklas Eén at Chalmers University of Technology | |
| Status: | available |
| Entry Name: | The source code of the Limmat solver (complete) | |
| Groups/PIs: | Prof. Armin Bierre at Computer Systems Institute, ETH Zurich | |
| Status: | available (BSD-style license) |
| Entry Name: | The source code of the WalkSAT solver (incomplete/local search) | |
| Groups/PIs: | Prof. Henry Kautz at U. Washington and Prof. Bart Selman at Cornell U. | |
| Status: | available |
| Entry Name: | The source code of the DLM-2K solver (incomplete/local search) | |
| Groups/PIs: | Zhe Wu and prof. Benjamin Wah at UIUC | |
| Status: | available |
| Entry Name: | SAT live (news, mailing lists, papers, other resources) | |
| Groups/PIs: | Dr. Daniel Le Berre, Univ. of Newcastle, Australia | |
| Status: | available |
| Entry Name: | SAT basics and a high-quality implementation of GRASP | |
| Groups/PIs: | Prof. Karem Sakallah U.Michigan | |
| Status: | available |
| Entry Name: | GRASP home and papers | |
| Groups/PIs: | Prof. Joao Marques-Silva UT Lisbon | |
| Status: | available |
| Entry Name: | Incremental satisfiability: SATIRE | |
| Groups/PIs: | Prof. Karem Sakallah U.Michigan | |
| Status: | available |
| Entry Name: | PBS: Incremental satisfiability and 0-1 ILP | |
| Groups/PIs: | Fadi Aloul | |
| Status: | available |
| Entry Name: | Sat-Ex | |
| Groups/PIs: | Laurent Simon LRI Paris Sud | |
| Status: | available |
| Entry Name: | Shatter --- symmetry-breaking for SAT | |
| Groups/PIs: | Fadi A. Aloul, Igor L. Markov and Karem A. Sakallah at the University of Michigan | |
| Status: | available |
| Entry Name: | Difficult symmetric SAT benchmarks (SAT 2002/DAC 2002) | |
| Groups/PIs: | Fadi A. Aloul, Igor L. Markov and Karem A. Sakallah at the University of Michigan | |
| Status: | available |
| Entry Name: | 2clseq-A DPLL Solver Using Extensive Binary Clause Reasoning | |
| Groups/PIs: | Dr. Fahiem Bacchus at the University of Toronto | |
| Status: | available |
| Entry Name: | SAT Solvers from SAT Competition 2003 | |
| Groups/PIs: | | |
| Status: | available |
| Entry Name: | Tutorial | |
| Groups/PIs: | Prof. João Marques Silva | |
| Status: | available |
| Entry Name: | Forced Satisfiable SAT Benchmarks | |
| Groups/PIs: | Ke Xu at at BUAA | |
| Status: | available |
| Entry Name: | DIMACS SAT benchmarks | |
| Groups/PIs: | Dr. Holger H. Hoos at UBC | |
| Status: | available |
| Entry Name: | GLPK (GNU Linear Programming Kit) | |
| Groups/PIs: | Andrew Makhorin | |
| Status: | available |