Old techniques in new ways: clause weighting, unit propagation and hybridization for maximum satisfiability

DOI10.1016/J.ARTINT.2020.103354MaRDI QIDQ2211872zbMATH OpenOpenAlexFDO

Authors Shaowei Cai, Zhendong Lei

Publication date 16 November 2020

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.artint.2020.103354

zbMATH Keywords

clause weightinghybridizationindustrial instanceslocal searchmaximum satisfiabilityunit propagation

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Combinatorial optimization (90C27) Approximation methods and heuristics in mathematical programming (90C59)

Recommendations

• Solving maximum weight clique using maximum satisfiability reasoning
• MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability
• scientific article; zbMATH DE number 1954173
• Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms
• Principles and Practice of Constraint Programming – CP 2004
• An exact algorithm based on MaxSAT reasoning for the maximum weight clique problem
• Towards a better understanding of (partial weighted) MaxSAT proof systems
• On Inconsistent Clause-Subsets for Max-SAT Solving

Cites work

• Algorithms for Weighted Boolean Optimization
• CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability
• CCLS: An Efficient Local Search Algorithm for Weighted Maximum Satisfiability
• scientific article; zbMATH DE number 1954176 (Why is no real title available?)
• Iterative and core-guided maxsat solving: a survey and assessment
• New local search methods for partial MaxSAT
• On Solving the Partial MAX-SAT Problem
• Open-WBO: a modular MaxSAT solver
• QMaxSAT: A partial Max-SAT solver
• SAT-based MaxSAT algorithms
• Solving (Weighted) Partial MaxSAT through Satisfiability Testing
• WPM3: an (in)complete algorithm for weighted partial MaxSAT

Cited in

(21)

• Solving MaxSAT with bit-vector optimization
• WPM3: an (in)complete algorithm for weighted partial MaxSAT
• An iterative path-breaking approach with mutation and restart strategies for the MAX-SAT problem
• Using the method of conditional expectations to supply an improved starting point for CCLS
• Efficient local search for pseudo Boolean optimization
• Local search with a SAT oracle for combinatorial optimization
• On preprocessing for weighted MaxSAT
• LMHS: a SAT-IP hybrid MaxSat solver
• New local search methods for partial MaxSAT
• SAT-based MaxSAT algorithms
• scientific article; zbMATH DE number 1954176 (Why is no real title available?)
• Using merging variables-based local search to solve special variants of MaxSAT problem
• SATLike
• Exploiting subproblem optimization in SAT-based maxsat algorithms
• Solving maximum weight clique using maximum satisfiability reasoning
• Generalization of the subset sum problem and cubic forms
• \texttt{TT-Open-WBO-Inc}: an efficient anytime MaxSAT solver
• Integrating multi-armed bandit with local search for MaxSAT
• Enhancing MaxSAT local search via a unified soft clause weighting scheme
• Improving local search for weighted partial MaxSAT by initializing with historical information
• Local-MIP: efficient local search for mixed integer programming

Describes a project that uses

Uses Software

• RC2
• QMaxSAT
• WPM3
• Sat4j
• Open-WBO
• MaxHS
• CCEHC
• CCLS

This page was built for publication: Old techniques in new ways: clause weighting, unit propagation and hybridization for maximum satisfiability

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