Logical Cryptanalysis as a SAT-Problem: Encoding and Analysis of the U.S. Data Encryption Standard