Solving Optimization Problems with DLL

Propositional satisfiability (SAT) is a success story in Computer Science and Artificial Intelligence: SAT solvers are currently used to solve problems in many different application domains, including planning and formal verification. The main reason for this success is that modern SAT solvers can successfully deal with problems having millions of variables. All these solvers are based on the DavisLogemann-Loveland procedure (DLL). DLL is a decision procedure: Given a formula , it returns whether is satisfiable or not. Further, DLL can be easily modified in order to return an assignment satisfying , assuming one exists. However, in many cases it is not enough to compute a satisfying assignment: Indeed, the returned assignment has also to be "optimal" in some sense, e.g., it has to minimize/maximize a given objective function. In this paper we show that DLL can be very easily adapted in order to solve optimization problems like MAX-SAT and MIN-ONE. In particular these proble...

• Type: Conference
• Year: 2006
• Where: ECAI
• Authors: Enrico Giunchiglia, Marco Maratea
• Keywords: Artificial Intelligence, ECAI 2006, Modern Sat Solvers, Problems, SAT Solvers