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 Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change
14:20 - 16:00: Track 1: Decision ProceduresResearch Papers at Grand Bay North Chair(s): Loris D'AntoniUniversity of Pennsylvania | |||
14:20 - 14:45 Talk | Query-Guided Maximum Satisfiability Research Papers Xin ZhangGeorgia Tech, Ravi MangalGeorgia Institute of Technology, Aditya NoriMicrosoft Research, UK, Mayur NaikGeorgia Tech File Attached | ||
14:45 - 15:10 Talk | String Solving with Word Equations and Transducers: Decidability and Applications to Detecting Mutation XSS Research Papers Media Attached | ||
15:10 - 15:35 Talk | Symbolic Computation of Differential Equivalences Research Papers Luca CardelliMicrosoft Research and University of Oxford, Mirco TribastoneIMT Institute for Advanced Studies Lucca, Italy, Max TschaikowskiIMT Institute for Advanced Studies Lucca, Italy, Andrea VandinIMT Institute for Advanced Studies Lucca, Italy Media Attached | ||
15:35 - 16:00 Talk | Unboundedness and Downward Closures of Higher-Order Pushdown Automata Research Papers Matthew HagueRoyal Holloway University of London, UK, Jonathan KochemsDepartment of Computer Science, University of Oxford, C.-H. Luke OngUniversity of Oxford, UK Media Attached |