Sciweavers

CONSTRAINTS
2010

Solving satisfiability problems with preferences

13 years 1 months ago
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
Emanuele Di Rosa, Enrico Giunchiglia, Marco Marate
Added 01 Mar 2011
Updated 01 Mar 2011
Type Journal
Year 2010
Where CONSTRAINTS
Authors Emanuele Di Rosa, Enrico Giunchiglia, Marco Maratea
Comments (0)