An experimental evaluation of Max-SAT and PB solvers on over-subscription planning problems
Marco Maratea · 2010
We present an evaluation of Max-SAT and Pseudo-Boolean (PB) solvers on a novel and interesting application domain involving planning problems with preferences expressed on actions preconditions and/or goals. These are over-subscription planning problems, i.e., planning problems in which not all the goals can be satisfied, thus practically very important, where a cost is associated to the violation of goals and/or actions preconditions, which include all domains from the “SimplePreferences ” track of the 5th International Planning Competition (IPC-5). Such benchmarks are reduced to Max-SAT and PB problems, which provide two very natural ways to express this situation. We run a wide experimental analysis involving all best performing Max-SAT and PB solvers, and all the domains from the “SimplePreferences ” track of the IPC-5. Our analysis reveals what are the solvers that, at the moment, perform best on these benchmarks, and identifies, at the same time, challenging Max-SAT and PB benchmarks that we plan to submit to the next evaluations. 1