The P vs NP problem is often referred to as the most important open problem in computer science. It is one of the seven Clay Millennium Prize Problems, worth $1,000,000. Informally, it asks whether every problem whose solution can be quickly verified can also be quickly solved. Boolean Satisfiability (SAT) is the problem of determining whether a Boolean formula can be satisfied. SAT is the first problem to be established as NP-Complete, meaning SAT has a polynomial-time algorithm if and only if P=NP.
SAT solvers are computer programs that solve instances of the SAT problem in practice. Intriguingly, despite SAT being an unsolved problem theoretically, SAT solvers can routinely solve huge instances with millions and even tens or hundreds of millions of clauses.
This project is about developing the SAT solver IntelSAT. The goal is to upgrade IntelSAT to enable it to solve the optimization version of the SAT problem, called MaxSAT, where, in addition to the Boolean formula, there is also the requirement of optimizing a given linear function.
We will target improving the state of the art in MaxSAT solving and submitting the resulting solver to the MaxSAT Evaluation – a yearly competitive event that evaluates MaxSAT solvers over a large variety of benchmarks.
The project will be carried out under the supervision of Dr. Alexander Nadel (Technion & Intel). Alexander leads the development of SAT technology at Intel, where it is deployed to automate various tasks in physical design, formal verification, and other domains. Open-source SAT and MaxSAT solvers developed by Alexander have won several international competitions.
