Exploiting resolution-based representations for MaxSAT solving

DOI10.1007/978-3-319-24318-4_20zbMATH Open1471.68257arXiv1505.02405OpenAlexW2210398979MaRDI QIDQ3453232FDOQ3453232

Vasco Manquinho, Ruben Martins, Miguel M. Neves, Mikoláš Janota, Inês Lynce

Publication date: 20 November 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: Most recent MaxSAT algorithms rely on a succession of calls to a SAT solver in order to find an optimal solution. In particular, several algorithms take advantage of the ability of SAT solvers to identify unsatisfiable subformulas. Usually, these MaxSAT algorithms perform better when small unsatisfiable subformulas are found early. However, this is not the case in many problem instances, since the whole formula is given to the SAT solver in each call. In this paper, we propose to partition the MaxSAT formula using a resolution-based graph representation. Partitions are then iteratively joined by using a proximity measure extracted from the graph representation of the formula. The algorithm ends when only one partition remains and the optimal solution is found. Experimental results show that this new approach further enhances a state of the art MaxSAT solver to optimally solve a larger set of industrial problem instances.

Full work available at URL: https://arxiv.org/abs/1505.02405

Recommendations

• Exploiting subproblem optimization in SAT-based maxsat algorithms
• Community-Based Partitioning for MaxSAT Solving
• SAT-based MaxSAT algorithms
• Resolution for Max-SAT
• Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• PackUp: tools for package upgradability solving
• Community structure in social and biological networks
• Efficient CNF encoding of Boolean cardinality constraints
• Iterative and core-guided maxsat solving: a survey and assessment
• QMaxSAT: A partial Max-SAT solver
• Improvements to Core-Guided Binary Search for MaxSAT
• Title not available (Why is that?)
• On Solving the Partial MAX-SAT Problem
• Curriculum-based course timetabling with SAT and MaxSAT
• Variable Independence and Resolution Paths for Quantified Boolean Formulas
• The Community Structure of SAT Formulas
• Community-Based Partitioning for MaxSAT Solving
• Open-WBO: A Modular MaxSAT Solver,
• Blocked clause elimination
• On a generalization of extended resolution
• Resolution graphs

Cited In (4)

• Generating SAT instances with community structure
• Theory and Applications of Satisfiability Testing
• Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms
• A comparative analysis and improvement of MaxSAT encodings for coalition structure generation under MC-nets

Uses Software

• QMaxSAT
• Open-WBO
• PackUp

This page was built for publication: Exploiting resolution-based representations for MaxSAT solving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3453232)