Contemporary integrated circuits are designed and manufactured in a globalized environment leading to concerns of piracy, overproduction and counterfeiting. One class of techniques to combat these threats is logic encryption. Logic encryption modifies an IC design such that it operates correctly only when a set of newly introduced inputs, called key inputs, are set to the correct values. In this paper, we use algorithms based on satisfiability checking (SAT) to investigate the security of logic encryption. We present a SAT-based algorithm which allows an attacker to 'decrypt' an encrypted netlist using a small number of carefully-selected input patterns and their corresponding output observations. We also present a 'partial-break' algorithm that can reveal some of the key inputs even when the attack is not fully successful. We conduct a thorough evaluation of our attack by examining six proposals for logic encryption from the literature. We find that all of these are vulnerable to our attack. Among the 441 encrypted circuits we examined, we were able to decrypt 418 (95%). We discuss the strengths and limitations of our attack and suggest directions that may lead to improved logic encryption algorithms.