Acquiring local preferences of weighted partial maxsat

Many real-life problems can be formulated as boolean satisfiability (SAT). In addition, in many of these problems, there are some hard clauses that must be satisfied but also some other soft clauses that can remain unsatisfied at some cost. These problems are referred to as Weighted Partial Maximum Satisfiability (WPMS). For solving them, the challenge is to find a solution that minimizes the total sum of costs of the unsatisfied clauses. Configuration problems are real-life examples of these, which involve customizing products according to a user's specific requirements. In the literature there exist many efficient techniques for finding solutions having minimum total cost. However, less attention has been paid to the fact that in many real-life problems the associated weights for soft clauses can be unknown. An example of such situations is when users cannot provide local preferences but instead express global preferences over complete assignments. In these cases, the acquisition of preferences can be the key for finding the best solution. In this paper, we propose a method to formalize the acquisition of local preferences. The process involves solving the associated system of linear equations for a set of complete assignments and their costs. Furthermore, we formalize the characteristics and size of the complete assignments required to acquire all local weights. We present an heuristic algorithm that searches for such assignments which performs promisingly on many benchmarks from the literature.