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 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
14:20 - 16:00 | Track 1: Decision ProceduresResearch Papers at Grand Bay North Chair(s): Loris D'Antoni University of Pennsylvania | ||
14:20 25mTalk | Query-Guided Maximum Satisfiability Research Papers Xin Zhang Georgia Tech, Ravi Mangal Georgia Institute of Technology, Aditya Nori Microsoft Research, UK, Mayur Naik Georgia Tech File Attached | ||
14:45 25mTalk | String Solving with Word Equations and Transducers: Decidability and Applications to Detecting Mutation XSS Research Papers Media Attached | ||
15:10 25mTalk | Symbolic Computation of Differential Equivalences Research Papers Luca Cardelli Microsoft Research and University of Oxford, Mirco Tribastone IMT Institute for Advanced Studies Lucca, Italy, Max Tschaikowski IMT Institute for Advanced Studies Lucca, Italy, Andrea Vandin IMT Institute for Advanced Studies Lucca, Italy Media Attached | ||
15:35 25mTalk | Unboundedness and Downward Closures of Higher-Order Pushdown Automata Research Papers Matthew Hague Royal Holloway University of London, UK, Jonathan Kochems Department of Computer Science, University of Oxford, C.-H. Luke Ong University of Oxford, UK Media Attached |