ACM SIGPLAN Notices • Vol 51 • No 1
Query-guided maximum satisfiability
January 2016 • Xin Zhang, Ravi Mangal, Aditya V. Nori, Mayur Naik
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 solvi…