Solving satisfiability problems with preferences

Abstract. 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 Davis-Logemann-Loveland procedure (DLL). In its original version, DLL is a decision procedure, but it can be very easily modified in order to return one or all assignments satisfying the input set of clauses, assuming at least one exists. However, in many cases it is not enough to compute assignments satisfying all the input clauses: Indeed, the returned assignments have also to be "optimal" in some sense, e.g., they have to satisfy as many other constraints

• Type: Journal
• Year: 2010
• Where: CONSTRAINTS
• Authors: Emanuele Di Rosa, Enrico Giunchiglia, Marco Maratea
• Keywords: Computer Networks, CONSTRAINTS 2010, Optimal Models, Qualitative Preference, SAT Solvers