Understanding the power of Max-SAT resolution through UP-resilience
| Autor: | Mohamed Sami Cherif, Djamal Habet, André Abramé |
|---|---|
| Přispěvatelé: | COntraintes, ALgorithmes et Applications (COALA), Laboratoire d'Informatique et Systèmes (LIS), Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS)-Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS), Logike, Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS)-Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS)-Aix Marseille Université (AMU), CHERIF, Mohamed Sami, ANR-16-CE40-0028,DE-MO-GRAPH,Décomposition de Modèles Graphiques(2016) |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
[INFO.INFO-AI] Computer Science [cs]/Artificial Intelligence [cs.AI]
Linguistics and Language Branch and bound Unit propagation Computer science 02 engineering and technology Disjoint sets Resolution (logic) Upper and lower bounds Language and Linguistics [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI] Transformation (function) Artificial Intelligence 020204 information systems Maximum satisfiability problem 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Rule of inference Algorithm ComputingMilieux_MISCELLANEOUS |
| Zdroj: | Thirtieth International Joint Conference on Artificial Intelligence (IJCAI-21) Thirtieth International Joint Conference on Artificial Intelligence (IJCAI-21), Aug 2021, Montreal-themed Virtual Reality, Canada Artificial Intelligence Artificial Intelligence, Elsevier, 2020, 289, pp.103397. ⟨10.1016/j.artint.2020.103397⟩ Artificial Intelligence, 2020, 289, pp.103397. ⟨10.1016/j.artint.2020.103397⟩ |
| ISSN: | 0004-3702 |
| DOI: | 10.1016/j.artint.2020.103397⟩ |
| Popis: | A typical Branch and Bound algorithm for Max-SAT computes the lower bound by estimating the number of disjoint Inconsistent Subsets (IS) of the formula. The IS detection is ensured by Simulated Unit Propagation (SUP). Then, the inference rule for Max-SAT, Max-SAT resolution, is applied to ensure that the detected IS is counted only once. Learning Max-SAT resolution transformations can be detrimental to the algorithm performance, so they are usually selectively learned if they match certain patterns. In this paper, we study the impact of the transformations by Max-SAT resolution on the SUP mechanism, indispensable for IS detection. We introduce the notion of UP-resilience of a transformation which quantifies this impact and provides, from a theoretical point of view, an explanation to the empirical efficiency of the learning schemes developed in the last ten years. We also focus on recently introduced patterns called Unit Clause Subsets (UCSs). We characterize the transformations of certain UCSs using UP-resilience and we explain how our result can help extend the current patterns. Finally, we present empirical observations that support the relevance of the UP-resilience property and further consolidate our theoretical results. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect