Write a Blog >>
Wed 20 Jan 2016 14:20 - 14:45 at Grand Bay North - Track 1: Decision Procedures Chair(s): Loris D'Antoni

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

Displayed 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
25m
Talk
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
25m
Talk
String Solving with Word Equations and Transducers: Decidability and Applications to Detecting Mutation XSS
Research Papers
Anthony Widjaja Lin Yale-NUS College, Singapore, Pablo Barcelo University of Chile, Chile
Media Attached
15:10
25m
Talk
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
25m
Talk
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