Felienne talks with Moshe Vardi about P versus NP. Why is this problem so central to computer science? Are we close to solving it?\xa0 Is it necessary to solve it? Progress toward computing hard problems efficiently with SAT solvers.\xa0 How SAT solvers work,; applications of SAT like formal verification.