An In-Label Prioritizing Variable Branching Strategy of SAT Solvers for a Preferred Extension of Argumentation Frameworks
摘要
The SAT-based reduction methods have shown significant effectiveness in solving preferred extensions problem in argumentation frameworks. As a general-purpose solver, SAT solvers does not fully utilize the inherent properties of argumentation framework problems for customized design, resulting in suboptimal performance. Therefore, this paper proposes an in-label prioritizing variable branching strategy to improve the SAT solver from two aspects: the initialization of the polarity values of decision variables and the evaluation criteria for variable’s activity, enabling efficient solving of a preferred extension of argumentation frameworks. We implement this method in the state-of-the-art argumentation algorithm ArgSemSAT and conducted experimental analysis using the internationally recognized benchmarks ICCMA 2023 and ICCMA 2021. The experimental results show that the proposed method significantly enhances the performance of the original algorithm in solving a preferred extension, increasing the proportion of instances solved by the original algorithm by 6.96% for ICCMA 2023 and 37.5% for ICCMA 2021. Furthermore, the optimized algorithm outperforms \(\mu \) -toksia (cmsat) which ranks the third-place in the competition ICCMA 2023. Notably, the proposed algorithm demonstrates very efficient performance on the AFGen instances, reducing the average solving time of the original algorithm from 350.88 s to 5.75 s.