Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems

MaxSAT, the optimization version of the well-known SAT problem, has attracted a lot of research interest in the last decade. Motivated by the many important applications and inspired by the success of modern SAT solvers, researchers have developed many MaxSAT solvers. Since most research is algorith...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2021-07
Main Authors: Larrosa, Javier, Rollon, Emma
Format: Article
Language:English
Subjects:
Completeness
Inference
Optimization
Solvers
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:MaxSAT, the optimization version of the well-known SAT problem, has attracted a lot of research interest in the last decade. Motivated by the many important applications and inspired by the success of modern SAT solvers, researchers have developed many MaxSAT solvers. Since most research is algorithmic, its significance is mostly evaluated empirically. In this paper we want to address MaxSAT from the more formal point of view of Proof Complexity. With that aim we start providing basic definitions and proving some basic results. Then we analyze the effect of adding split and virtual, two original inference rules, to MaxSAT resolution. We show that each addition makes the resulting proof system stronger, with the virtual rule capturing the recently proposed concept of circular proof.
ISSN:2331-8422