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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

An In-Label Prioritizing Variable Branching Strategy of SAT Solvers for a Preferred Extension of Argumentation Frameworks

  • Mao Luo,
  • Jiao Xiong,
  • Ningning He,
  • Caiquan Xiong,
  • Xinyun Wu,
  • Jun Wu

摘要

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.