Iterative and core-guided maxsat solving: a survey and assessment
From MaRDI portal
Publication:2348540
DOI10.1007/s10601-013-9146-2zbMath1317.90199OpenAlexW2029958553MaRDI QIDQ2348540
Antonio Morgado, Jordi Planes, Federico Heras, Mark H. Liffiton, João P. Marques-Silva
Publication date: 15 June 2015
Published in: Constraints (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10601-013-9146-2
Approximation methods and heuristics in mathematical programming (90C59) Boolean programming (90C09)
Related Items (32)
Fast, flexible MUS enumeration ⋮ Quantified maximum satisfiability ⋮ MaxSAT by improved instance-specific algorithm configuration ⋮ Advances in WASP ⋮ Exploiting Resolution-Based Representations for MaxSAT Solving ⋮ SAT-Based Formula Simplification ⋮ Propositional SAT Solving ⋮ New local search methods for partial MaxSAT ⋮ A logic-based Benders decomposition for microscopic railway timetable planning ⋮ An Experimental Evaluation of Fast Approximation Algorithms for the Maximum Satisfiability Problem ⋮ Minimal sets on propositional formulae. Problems and reductions ⋮ WPM3: an (in)complete algorithm for weighted partial MaxSAT ⋮ Understanding the complexity of axiom pinpointing in lightweight description logics ⋮ Time-expanded graph-based propositional encodings for makespan-optimal solving of cooperative path finding problems ⋮ Model enumeration in propositional circumscription via unsatisfiable core analysis ⋮ Old techniques in new ways: clause weighting, unit propagation and hybridization for maximum satisfiability ⋮ Propositional proof systems based on maximum satisfiability ⋮ On the performance of MaxSAT and MinSAT solvers on 2SAT-MaxOnes ⋮ Cost-optimal constrained correlation clustering via weighted partial maximum satisfiability ⋮ Exploiting subproblem optimization in SAT-based maxsat algorithms ⋮ Discrete Optimization with Decision Diagrams ⋮ Using Merging Variables-Based Local Search to Solve Special Variants of MaxSAT Problem ⋮ On the complexity of inconsistency measurement ⋮ Polarity and Variable Selection Heuristics for SAT-Based Anytime MaxSAT ⋮ On Using Incremental Encodings in Unsatisfiability-based MaxSAT Solving ⋮ MiFuMax—a Literate MaxSAT Solver ⋮ RC2: an Efficient MaxSAT Solver ⋮ Clause redundancy and preprocessing in maximum satisfiability ⋮ Ranking with multiple reference points: efficient SAT-based learning procedures ⋮ Proofs and Certificates for Max-SAT ⋮ Assessing progress in SAT solvers through the Lens of incremental SAT ⋮ A refined branching algorithm for the maximum satisfiability problem
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A linear-time transformation of linear inequalities into conjunctive normal form
- SAT-based MaxSAT algorithms
- Boolean lexicographic optimization: algorithms \& applications
- Curriculum-based course timetabling with SAT and MaxSAT
- Cardinality networks: a theoretical and empirical study
- Haplotype inference with pseudo-Boolean optimization
- Solving satisfiability problems with preferences
- A new bounding procedure and an improved exact algorithm for the Max-2-SAT problem
- Improving exact algorithms for MAX-2-SAT
- Solving weighted CSP by maintaining arc consistency
- Answer set programming based on propositional satisfiability
- Soft arc consistency revisited
- Resolution for Max-SAT
- A theory of diagnosis from first principles
- A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems
- A logical approach to efficient Max-SAT solving
- MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability
- Algorithms for computing minimal unsatisfiable subsets of constraints
- Improvements to Core-Guided Binary Search for MaxSAT
- Efficient and Accurate Haplotype Inference by Combining Parsimony and Pedigree Information
- Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions
- Antichain-Based QBF Solving
- Solving SAT and SAT Modulo Theories
- Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms
- Exploiting Unit Propagation to Compute Lower Bounds in Branch and Bound Max-SAT Solvers
- Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
- Local Consistency in Weighted CSPs and Inference in Max-SAT
- optsat: A Tool for Solving SAT Related Optimization Problems
- Satisfiability Modulo the Theory of Costs: Foundations and Applications
- Variable Dependency in Local Search: Prevention Is Better Than Cure
- Solving (Weighted) Partial MaxSAT through Satisfiability Testing
- Algorithms for Weighted Boolean Optimization
- Max-ASP: Maximum Satisfiability of Answer Set Programs
- NP trees and Carnap's modal logic
- Consistent subsets of inconsistent systems: structure and behaviour
- New Upper Bounds for Maximum Satisfiability
- Improving Unsatisfiability-Based Algorithms for Boolean Optimization
- Optimal Protein Structure Alignment Using Maximum Cliques
- Theory and Applications of Satisfiability Testing
- A Modular Approach to MaxSAT Modulo Theories
- Community-Based Partitioning for MaxSAT Solving
- Unsatisfiability-based optimization in clasp
- Logic programming with satisfiability
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- On Solving the Partial MAX-SAT Problem
- On SAT Modulo Theories and Optimization Problems
- Principles and Practice of Constraint Programming – CP 2003
- Principles and Practice of Constraint Programming – CP 2003
- Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems
- Principles and Practice of Constraint Programming – CP 2004
- A ``logic-constrained knapsack formulation and a tabu algorithm for the daily photograph scheduling of an earth observation satellite
This page was built for publication: Iterative and core-guided maxsat solving: a survey and assessment
