## Author: Alexander Nadel

## Paper Information

Title: | Solving MaxSAT with Bit-Vector Optimization |

Authors: | Alexander Nadel |

Proceedings: | SAT Proceedings |

Editors: | Christoph M. Wintersteiger and Olaf Beyersdorff |

Keywords: | MaxSAT, Optimization Modulo Bit-Vectors, Unweighted Partial MaxSAT, SAT-based Optimization |

Abstract: | ABSTRACT. We explore the relationships between two closely related optimization problems: MaxSAT and Optimization Modulo Bit-Vectors (OBV). Given a bit-vector or a propositional formula F and a target bit-vector T, Unweighted Partial MaxSAT maximizes the number of satisfied bits in T, while OBV maximizes the value of T. The contribution of this paper is twofold. First, we propose a new OBV-based Unweighted Partial MaxSAT algorithm. Our resulting solver–Mrs. Beaver–is incremental: it can be re-used across multiple invocations with different target bit-vectors. Mrs. Beaver outscores the state-of-the-art solvers when run with the settings of the Incomplete-60-Second-Timeout Track of the MaxSAT Evaluation 2017. Second, we introduce and study a new problem–Ordered MaxSAT (OMaxSAT). In OMaxSAT, instead of a target bit-vector T, there are multiple target bit-vectors T_{m−1} ,T_{m−2},...,T_0. The goal is to maximize the number of satisfied bits in each of the targets, where satisfying one bit of T_i is preferred to satisfying all the bits in T_{i−1}, T_{i−2} ,..., T_0 . OMaxSAT has a critical application at Intel: cleaning-up weak design rule violations during the Physical Design stage of Computer-Aided-Design. We propose a Mrs. Beaver-based OMaxSAT algorithm which takes advantage of Mrs. Beaver’s incremental features and is significantly faster than a non-incremental solution. |

Pages: | 20 |

Talk: | Jul 09 15:00 (Session 49F: MaxSAT) |

Paper: |