A Hybrid Approach for SAT
In: CP 2002 : principles and practice of constraint programming ; https://hal.science/hal-00359416 ; CP 2002 : principles and practice of constraint programming, Sep 2002, Ithaca NY, United States. pp.172-184, ⟨10.1007/3-540-46135-3_12⟩, 2002
Online
Konferenz
Zugriff:
International audience ; Exploiting variable dependencies has been shown very useful in local search algorithms for SAT. In this paper, we extend the use of such dependencies by hybridizing a local search algorithm, Walksat, and the DPLL procedure, Satz. At each node reached in the DPLL search tree to a fixed depth, we construct the literal implication graph. Its strongly connected components are viewed as equivalency classes. Each one is substituted by a unique representative literal to reduce the constructed graph and the input formula. Finally, the implication dependencies are closed under transitivity. The resulted implications and equivalencies are exploited by Walksat at each node of the DPLL tree. Our approach is motivated by the power of the branching rule used in Satz that may provide a valid path to a solution, and generate more implications at deep nodes. Experimental results confirm the efficiency of our approach.
Titel: |
A Hybrid Approach for SAT
|
---|---|
Autor/in / Beteiligte Person: | Habet, Djamal ; Li, Chu Min ; Brisoux Devendeville, Laure ; Vasquez, Michel ; Laboratoire des Sciences de l'Information et des Systèmes (LSIS) ; Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Arts et Métiers Paristech ENSAM Aix-en-Provence-Centre National de la Recherche Scientifique (CNRS) ; Laboratoire de Recherche en Informatique d'Amiens (LaRIA) ; Université de Picardie Jules Verne (UPJV)-Centre National de la Recherche Scientifique (CNRS) ; Laboratoire de Génie Informatique et Ingénierie de Production (LGI2P) ; IMT - MINES ALES (IMT - MINES ALES) ; Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT) |
Link: | |
Zeitschrift: | CP 2002 : principles and practice of constraint programming ; https://hal.science/hal-00359416 ; CP 2002 : principles and practice of constraint programming, Sep 2002, Ithaca NY, United States. pp.172-184, ⟨10.1007/3-540-46135-3_12⟩, 2002 |
Veröffentlichung: | HAL CCSD, 2002 |
Medientyp: | Konferenz |
DOI: | 10.1007/3-540-46135-3_12 |
Schlagwort: |
|
Sonstiges: |
|