MUST: Provide a Finer-Grained Explanation of Unsatisfiability

DOI10.1007/978-3-540-74970-7_24MaRDI QIDQ3523066zbMATH OpenOpenAlexFDO

Authors E. Grégoire, Bertrand Mazure, Cedric Piette

Publication date 2 September 2008

Published in Principles and Practice of Constraint Programming – CP 2007 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-74970-7_24

zbMATH Keywords

constraint networksCSPexplanationMUCMUSMUSTunsatisfiability

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Restoring CSP satisfiability with MaxSAT
• Local-search extraction of mUSes
• Debugging unsatisfiable constraint models
• Algorithms for computing minimal unsatisfiable subsets of constraints
• On getting rid of the preprocessing minimization step in MUC-finding algorithms

Cites work

• Approximating minimal unsatisfiable subformulae by means of adaptive core search
• Choco
• Generalized filtering algorithms for infeasibility analysis
• scientific article; zbMATH DE number 4162321 (Why is no real title available?)
• scientific article; zbMATH DE number 1149402 (Why is no real title available?)
• scientific article; zbMATH DE number 1163815 (Why is no real title available?)
• scientific article; zbMATH DE number 2080311 (Why is no real title available?)
• scientific article; zbMATH DE number 2080324 (Why is no real title available?)
• Local-search extraction of mUSes
• On the complexity of propositional knowledge base revision, updates, and counterfactuals
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

Cited in

(9)

• Progress towards the Holy Grail
• Debugging unsatisfiable constraint models
• Restoring CSP satisfiability with MaxSAT
• Towards a notion of unsatisfiable and unrealizable cores for LTL
• Algorithms for computing minimal equivalent subformulas
• Enhancing unsatisfiable cores for LTL with information on temporal relevance
• MUPS identification based on discrimination rules
• Super-reparametrizations of weighted CSPs: properties and optimization perspective
• On getting rid of the preprocessing minimization step in MUC-finding algorithms

Describes a project that uses

Uses Software

• Choco
• AMUSE

This page was built for publication: MUST: Provide a Finer-Grained Explanation of Unsatisfiability

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