Rodrigue Konan Tchinda ; Clémentin Tayou Djamegni - Enhancing Reasoning with the Extension Rule in CDCL SAT Solvers

arima:6434 - Revue Africaine de Recherche en Informatique et Mathématiques Appliquées, November 9, 2021, Volume 33 - Special issue CRI 2019 - 2020-21 -
Enhancing Reasoning with the Extension Rule in CDCL SAT SolversArticle

Authors: Rodrigue Konan Tchinda 1,2,3,4; Clémentin Tayou Djamegni 1

  • 1 Université de Dschang
  • 2 University of Bamenda, Bambili, Cameroon
  • 3 University of Bamenda
  • 4 Higher Teachers' Training College, University of Maroua

The extension rule first introduced by G. Tseitin is a simple but powerful rule that, when added to resolution, leads to an exponentially stronger proof system known as extended resolution (ER). Despite the outstanding theoretical results obtained with ER, its exploitation in practice to improve SAT solvers' efficiency still poses some challenging issues. There have been several attempts in the literature aiming at integrating the extension rule within CDCL SAT solvers but the results are in general not as promising as in theory. An important remark that can be made on these attempts is that most of them focus on reducing the sizes of the proofs using the extended variables introduced in the solver. We adopt in this work a different view. We see extended variables as a means to enhance reasoning in solvers and therefore to give them the ability of reasoning on various semantic aspects of variables. Experiments carried out on the 2018 and 2020 SAT competitions' benchmarks show the use of the extension rule in CDCL SAT solvers to be practically beneficial for both satisfiable and unsatisfiable instances.

Volume: Volume 33 - Special issue CRI 2019 - 2020-21
Published on: November 9, 2021
Accepted on: October 23, 2021
Submitted on: April 28, 2020
Keywords: SAT,CDCL,Extension Rule,SAT,CDCL,Règle d'extension,[INFO]Computer Science [cs],[INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI]

Consultation statistics

This page has been seen 326 times.
This article's PDF has been downloaded 229 times.