LMHS: A SAT-IP Hybrid MaxSAT Solver

DOI10.1007/978-3-319-40970-2_34zbMath1475.68449OpenAlexW2481363456MaRDI QIDQ2818041

Matti Järvisalo, Jeremias Berg, Paul Saikko

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)

Related Items

A constraint optimization approach to causal discovery from subsampled time series data, Boosting branch-and-bound MaxSAT solvers with clause learning, Propositional proof systems based on maximum satisfiability, Discovering causal graphs with cycles and latent confounders: an exact branch-and-bound approach, Pakota: A System for Enforcement in Abstract Argumentation, Unsatisfiable Core Analysis and Aggregates for Optimum Stable Model Search, Improved WPM encoding for coalition structure generation under MC-nets, Open-WBO-Inc: Approximation Strategies for Incomplete Weighted MaxSAT

Uses Software

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

Cites Work

• SCIP: solving constraint integer programs
• SAT-Based Preprocessing for MaxSAT
• Inprocessing Rules
• MaxSAT-based encodings for Group MaxSAT
• The Implicit Hitting Set Approach to Solve Combinatorial Optimization Problems with an Application to Multigenome Alignment
• Theory and Applications of Satisfiability Testing
• Formula Preprocessing in MUS Extraction
• Exploiting the Power of mip Solvers in maxsat
• Theory and Applications of Satisfiability Testing
• MaxSAT-Based Cutting Planes for Learning Graphical Models