A SAT Based Scheduler for Tournament Schedules

We present a scheduler with a web interface for generating fair game schedules of a tournament. The tournament can be either single or double round-robin or something in between. The search engine inside the scheduler is a SAT solver which can handle a mix of ordinary and TL (True-Literal) clauses. The latter are the formulas using the function TL which counts the number of true literals in a clause. By using TL clauses, we could solve a typical scheduling problem in a few of seconds. If we convert them into ordinary clauses, the state-of-the-art SAT solvers could not solve them in one week. We showed how to integrate TL clauses into a SAT solver and take advantages of the advanced SAT techniques. Our scheduler provides a free service to all the people who are interested in fair sports schedules.

• Type: Conference
• Year: 2004
• Where: SAT
• Authors: Hantao Zhang, Dapeng Li, Haiou Shen
• Keywords: SAT 2004, Sat Solver, State-of-the-art Sat Solvers, TL Clauses