Downloads

SatPlan

• SatPlan took first place for optimal deterministic planning at the International Planning Competition at the 14th International Conference on Automated Planning & Scheduling in 2004.
• Source
• Linux Binaries
• Description

BlackBox

• Entered in the First International Planning Competition.
  
• Incorporates the first scalable clause-learning SAT solver, Chaff.
• BlackBox home page
  

Papers

SatPlan: Planning as Satisfiability

Henry Kautz, Bart Selman, and Joerg Hoffmann. Abstracts of the 5th International Planning Competition, 2006.

Unifying SAT-based and Graph-based Planning

Henry Kautz and Bart Selman. Proc. IJCAI-99, Stockholm, 1999.

Encoding Plans in Propositional Logic

Henry Kautz, David McAllester, and Bart Selman, Proc. KR-96.

Pushing the Envelope: Planning, Propositional Logic, and Stochastic Search

Henry Kautz and Bart Selman, Proc. AAAI-96.

Planning as Satisfiability

Henry Kautz and Bart Selman, Proceedings ECAI-92.

Credits

• SatPlan was created by Henry Kautz and Dr. Jörg Hoffman
• BlackBox was created by Henry Kautz and Bart Selman
  
• SAT solver siege was created by Lawrence Ryan.
• SAT solver BerkMin was created by Eugene Goldberg and Yakov Novikov
• SAT solver Jerusat was created by Alexander Nadel
• SAT solver satz was created by Chu Min Li
  
• SAT solver chaff was created by by Sharad Malik