Solving WCSP by Extraction of Minimal Unsatisfiable Cores
Usual techniques to solve WCSP are based on cost transfer operations coupled with a branch and bound algorithm. In this paper, we focus on an approach integrating extraction and relaxation of Minimal Unsatisfiable Cores in order to solve this problem. We decline our approach in two ways: an incomplete, greedy, algorithm and a complete one.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Enumerating Minimal Unsatisfiable Cores of LTLf formulas
Linear Temporal Logic over finite traces ($\text{LTL}_f$) is a widely used formalism with applications in AI, process mining, model checking, and more. The primary reasoning task for $\text{LTL}_f$ is satisfiability chec…
Unsatisfiable Cores for Constraint Programming
Constraint Programming (CP) solvers typically tackle optimization problems by repeatedly finding solutions to a problem while placing tighter and tighter bounds on the solution cost. This approach is somewhat naive, espe…
Unsatisfiable Cores and Lower Bounding for Constraint Programming
Constraint Programming (CP) solvers typically tackle optimization problems by repeatedly finding solutions to a problem while placing tighter and tighter bounds on the solution cost. This approach is somewhat naive, espe…
Improving MUC extraction thanks to local search
ExtractingMUCs(MinimalUnsatisfiableCores)fromanunsatisfiable constraint network is a useful process when causes of unsatisfiability must be understood so that the network can be re-engineered and relaxed to become sat- i…
An ASP-Based Framework for MUSes
Given an unsatisfiable formula, understanding the core reason for unsatisfiability is crucial in several applications. One effective way to capture this is through the minimal unsatisfiable subset (MUS), the subset-minim…
Computational Efficiency