Query-guided maximum satisfiability
Abstract
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. 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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 11, 2016
- Source ID
- 10.1145/2914770.2837658
Entities
People
- Aditya V. Nori
- Mayur Naik
- Ravi Mangal
- Xin Zhang
Organizations
- Defense Advanced Research Projects Agency
- Georgia Tech
- Microsoft
- National Science Foundation