Aim of Paper

• Answer question “Can we encode cryptographic key search as a SAT problem so that AI search techniques can solve it?”

• Provide benchmarks for SAT research

  • help to find out which algorithms are best
  • failures and successes help to design new algorithms

• Don’t expect to solve full DES

  • extensive research by special purpose methods
  • aim to study use of general purpose methods