Exploiting resolution-based representations for MaxSAT solving

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

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

Publication date 20 November 2015

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

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

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)

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.

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

Cites work

• Blocked clause elimination
• Community structure in social and biological networks
• Community-Based Partitioning for MaxSAT Solving
• Curriculum-based course timetabling with SAT and MaxSAT
• Efficient CNF encoding of Boolean cardinality constraints
• Improvements to core-guided binary search for MaxSAT
• Iterative and core-guided maxsat solving: a survey and assessment
• On Solving the Partial MAX-SAT Problem
• On a generalization of extended resolution
• Open-WBO: a modular MaxSAT solver
• PackUp: tools for package upgradability solving
• Progression in maximum satisfiability
• QMaxSAT: A partial Max-SAT solver
• Resolution graphs
• The community structure of SAT formulas
• Variable independence and resolution paths for quantified Boolean formulas

Cited in

(8)

• A comparative analysis and improvement of MaxSAT encodings for coalition structure generation under MC-nets
• Analysis and solving SAT and MAX-SAT problems using an \(L\)-partition approach
• On using incremental encodings in unsatisfiability-based MaxSAT solving
• Generating SAT instances with community structure
• SAT-based MaxSAT algorithms
• Exploiting subproblem optimization in SAT-based maxsat algorithms
• Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms
• Theory and Applications of Satisfiability Testing

Describes a project that uses

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)