Analysis of Core-Guided MaxSat Using Cores and Correction Sets
summary
Proves that core-guided MaxSAT and hitting-set solvers recover the same original-core structure and that the minimum hitting set equals optimum when computed from cores produced by core-guided runs; experiments run a greedy randomized core extraction for six hours per instance over last-year MaxSAT benchmarks, yielding up to hundreds of thousands of cores, core sizes from 1 to 400, and cases where core-guided solvers stall while hitting-set bounds exceed reachable lower bounds; multiple hybrid solver attempts mostly fail, one is partially successful and under development.
AI-written summary · about
chapters (15)
- 0:00Start
- 2:28Weighted Partial MaxSAT problem
- 3:30Unsatisfiable Core
- 4:11Running example
- 5:25Correction Set
- 6:17Motivation
- 8:29Minimum Hitting Set-based Solver
- 13:06Core-guided Solver
- 15:17Implicit trace
- 15:45Main question
- 18:09Practical observations
- 18:50Practical opportunities
- 31:48MaxSAT Evaluation 2022
- 36:26The number of cores
- 38:06'Goodness' of core structure
related talks
29mImproved Deterministic Algorithms for Sparse Max-SAT
17mSatisfiability Algorithms Based on Concentrated Shrinkage
21mMassive proofs for the masses
39mSketching and Randomization for Distributed Submodular and Coverage Optimization
17mSolving Max-Min Fair Resource Allocations Quickly on Large Graphs
32mThe Computational Benefit of Correlated Instances
30mParallelization by Approximation
01h 21mComputational Complexity in Theory and in Practice