LMHS: a SAT-IP hybrid MaxSat solver

DOI10.1007/978-3-319-40970-2_34MaRDI QIDQ2818041zbMATH OpenOpenAlexFDO

Authors Paul Saikko, Jeremias Berg, Matti Järvisalo

Publication date 5 September 2016

Published in Theory and Applications of Satisfiability Testing – SAT 2016 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-40970-2_34

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)

Recommendations

• Minimaxsat: an efficient weighted Max-SAT solver
• Solving (Weighted) Partial MaxSAT through Satisfiability Testing
• Exploiting the power of MIP solvers in MAXSAT
• Old techniques in new ways: clause weighting, unit propagation and hybridization for maximum satisfiability
• An efficient solver for weighted Max-SAT

Cites work

• Exploiting the power of MIP solvers in MAXSAT
• Formula preprocessing in MUS extraction
• Inprocessing rules
• MaxSAT-based cutting planes for learning graphical models
• MaxSAT-based encodings for Group MaxSAT
• SAT-based preprocessing for MaxSAT
• SCIP: solving constraint integer programs
• The implicit hitting set approach to solve combinatorial optimization problems with an application to multigenome alignment
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

Cited in

(17)

• A constraint optimization approach to causal discovery from subsampled time series data
• DRMaxSAT with MaxHS: first contact
• Propositional proof systems based on maximum satisfiability
• Discovering causal graphs with cycles and latent confounders: an exact branch-and-bound approach
• Improved WPM encoding for coalition structure generation under MC-nets
• Pakota: a system for enforcement in abstract argumentation
• Open-WBO: a modular MaxSAT solver
• Unsatisfiable core analysis and aggregates for optimum stable model search
• MiFuMax -- a literate MaxSAT solver. System description
• \textsf{Open-WBO-Inc}: approximation strategies for incomplete weighted MaxSAT
• Boosting branch-and-bound MaxSAT solvers with clause learning
• Exploiting the power of MIP solvers in MAXSAT
• Unsatisfiability-based algorithms for multi-objective combinatorial optimization
• ASP-based approaches for solving the nuclear medicine scheduling problem
• Solving weighted maximum satisfiability with branch and bound and clause learning
• Scheduling pre-operative assessment clinic with answer set programming
• An efficient algorithm for power dominating set

Describes a project that uses

Uses Software

• LMHS
• Coprocessor
• SCIP
• MiniSat
• CPLEX
• MaxHS
• Lingeling

This page was built for publication: LMHS: a SAT-IP hybrid MaxSat solver

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