We propose a new optimization problem “Q-MaxSAT”, an extension of the well-known Maximum Satisfiability or MaxSAT problem. In contrast to MaxSAT, which aims to find an assignment to all variables in the formula, Q-MaxSAT computes an assignment to a desired subset of variables (or queries) in the formula. Indeed, many problems in diverse domains such as program reasoning, information retrieval, and mathematical optimization can be naturally encoded as Q-MaxSAT instances. Being query-guided allows us to focus on the subproblem relevant to the queries, therefore greatly improving efficiency. We describe an iterative algorithm for solving Q-MaxSAT. In each iteration, the algorithm solves a subproblem that is relevant to the queries, and applies a novel technique to check whether the partial assignment found is a solution to the Q-MaxSAT problem. If the check fails, the algorithm grows the subproblem with a new set of clauses identified as relevant to the queries. Our empirical evaluation shows that our Q-MaxSAT solver Pilot achieves significant improvements in runtime and memory consumption over conventional MaxSAT solvers on several Q-MaxSAT instances generated from real-world problems in program analysis and information retrieval.
|Poster For "Query-Guided Maximum Satisfiability" (popl16.pdf)||580KiB|
Wed 20 Jan
|14:20 - 14:45|
|14:45 - 15:10|
String Solving with Word Equations and Transducers: Decidability and Applications to Detecting Mutation XSSMedia Attached
|15:10 - 15:35|
|15:35 - 16:00|