Scientists Solve 90-Year-Old Geometry Problem

Math puzzle resolved by translating it into satisfiability problem. Carnegie Mellon University computer scientists and mathematicians have resolved the last, stubborn piece of Keller's conjecture, a geometry problem that scientists have puzzled over for 90 years. By structuring the puzzle as what computer scientists call a satisfiability problem, the researchers put the problem to rest with four months of frenzied computer programming and just 30 minutes of computation using a cluster of computers. "I was really happy when we solved it, but then I was a little sad that the problem was gone," said John Mackey , a teaching professor in the Computer Science Department (CSD) and Department of Mathematical Sciences who had pursued Keller's conjecture since he was a graduate student 30 years ago. "But then I felt happy again. There's just this feeling of satisfaction." The solution was yet another success for an approach pioneered by Marijn Heule , an associate professor of computer science who joined CSD last August. Heule has used an SAT solver - a computer program that uses propositional logic to solve satisifiability (SAT) problems - to conquer several hoary math challenges, including the Pythagorean triples problem and Schur number 5.