Effectively Encoding SAT and Other Intractable Problems into Ising Models for Quantum Computing

Quantum computing theory posits that a computer exploiting quantum mechanics can be strictly more powerful than classical models. Several quantum computing devices are under development, but current technology is limited by noise sensitivity. Quantum Annealing is an alternative approach that uses a noisy quantum system to solve a particular optimization problem. Problems such as SAT and MaxSAT need to be encoded to make use of quantum annealers. Encoding SAT and MaxSAT problems while respecting the constraints and limitations of current hardware is a difficult task. This thesis presents an approach to encoding SAT and MaxSAT problems that is able to encode bigger and more interesting problems for quantum annealing. A software implementation and preliminary evaluation of the method are described.