\documentclass[conference]{IEEEtran}
\IEEEoverridecommandlockouts
% The preceding line is only needed to identify funding in the first footnote. If that is unneeded, please comment it out.
%Template version as of 6/27/2024

\usepackage{cite}
\usepackage{url}
\usepackage{makecell}
\usepackage{amsmath,amssymb,amsfonts}
\usepackage{algorithmic}
\usepackage{graphicx}
\usepackage{float}
\usepackage{tabularx}
\usepackage{booktabs}
\usepackage{array}
\usepackage{textcomp}
\usepackage{xcolor}
\def\BibTeX{{\rm B\kern-.05em{\sc i\kern-.025em b}\kern-.08em
		T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX}}
\begin{document}
	
	\title{Enhanced SAT-based Argumentation Solvers Using $in$ Label Priority Strategy and Large Language Model Tuning\\
	}
\author{
	\small
	\begin{tabular*}{\textwidth}{@{\extracolsep{\fill}} c c c}
		Qi Liu & Guangcheng Dong & Aoxu Ji \\
		\textit{Hubei University of Technology} & \textit{Hubei University of Technology} & \textit{Hubei University of Technology} \\
		Wuhan, China & Wuhan, China & Wuhan, China \\
		102401137@hbut.edu.cn & a257158281@126.com & jiaoxu@hbut.edu.cn \\
		\\[1.5ex]
		
		Hang Ding & Mao Luo & Ningning He \\
		\textit{Hubei University of Technology} & \textit{Hubei University of Technology} & \textit{Hubei University of Technology} \\
		Wuhan, China & Wuhan, China & Wuhan, China \\
		dinghang@hbut.edu.cn & luomao@hbut.edu.cn & hnn102211103@163.com \\
		\\[1.5ex]
		
		Caiquan Xiong & Xinyun Wu & Yuanzhi Ke \\
		\textit{Hubei University of Technology} & \textit{Hubei University of Technology} & \textit{Hubei University of Technology} \\
		Wuhan, China & Wuhan, China & Wuhan, China \\
		xiongcq@hbut.edu.cn & xinyun@hbut.edu.cn & keyuanzhi@hbut.edu.cn \\
	\end{tabular*}
}


	
	
	\maketitle
	
	\begin{abstract}
We present four solvers---\textbf{ASSAT\_inPriority}, \textbf{ASSAT\_Amsat}, \textbf{ASSAT\_Cadical} and \textbf{ASSAT\_LLM} to ICCMA 2025, all of which are improved versions of \textit{ArgSemSAT}. Some solvers replace the original \textit{Minisat} solver used in \textit{ArgSemSAT}, and all solvers incorporate optimizations to the rephasing strategies of the SAT solver. All four solvers participate in the following subtracks of the Main and No-Limits track:
\textbf{SE-\{PR, ST, SST\}}.
	\end{abstract}
	\vspace{-1.2em}
	\begin{IEEEkeywords}
		Abstract Argumentation, Solver
	\end{IEEEkeywords}

	
	\section{Introduction}
		\textit{ArgSemSAT} is a well-established solver for abstract argumentation frameworks\cite{b1}. In particular, \textit{ArgSemSAT} participated in the ICCMA 2017 and was the winner of the preferred semantics track, demonstrating its effectiveness and efficiency in computing argumentation semantics.
		
		\textit{ArgSemSAT} employs a encoding approach grounded in the three-valued labelling-based semantics\cite{b2}. In this method, each argument in the argumentation framework is assigned exactly one of three mutually exclusive labels:
		
\begin{itemize}
	\item \texttt{in} ($I_i$): the argument is justified.
	\item \texttt{out} ($O_i$): the argument is overruled.
	\item \texttt{undec} ($U_i$): the argument is neither justified nor overruled due to uncertainty.
\end{itemize}

	In our work, we observe that arguments assigned the \texttt{in} label typically lead to stronger propagation effects during the SAT solving process, compared to those assigned \texttt{out} or \texttt{undec} labels. Based on this observation, we adopt the rephasing strategy that prioritizes assigning \texttt{in}-label decision variables to true during the SAT solving process.
		
	
	\section{Architecture}
	
	\subsection{ASSAT\_inPriority}
	
	In our previous work \cite{b3}, our team proposed an in-label prioritizing variable branching strategy that significantly improved 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 further found that the \texttt{in}-variable-priority strategy can also be effectively applied in the search process of SAT solvers. In particular, it can be integrated into the rephasing strategy used after each restart, further enhancing the solver's performance and robustness.
	
	Building upon these promising results, We retained the original \textit{Minisat} solver used in \textit{ArgSemSAT}, and based on our observation of the advantages associated with variables labeled as \texttt{in}, we modified the original variable polarity initialization strategy, as well as the rephasing strategy. Specifically, during the initial polarity assignment, variables corresponding to \texttt{in}-labeled arguments are initialized with negative polarity, whereas variables associated with other labels are initialized with positive polarity. Separately, in the phase saving process of \textit{Minisat}, if a variable corresponds to an \texttt{in}-labeled argument, we assign its polarity with a 35\% probability of being negative, a 15\% probability of being positive, and a 50\% probability of preserving its previous polarity. For variables associated with other labels, we assign 15\% probability to both negative and positive polarities, while maintaining the previous polarity with a 70\% probability. This probabilistic polarity strategy introduces a degree of diversification, and our experimental results demonstrate that it significantly improves solving performance.
	
	
	\subsection{ASSAT\_AmSAT}
	
	In this solver, we replace the original \textit{Minisat} SAT solver of \textit{ArgSemSAT} with the \textit{AmSAT} SAT solver\cite{b4}, which improves the rephasing strategy and significantly enhances solving efficiency. The \textit{Relaxed CDCL Approach}\cite{b5} employed by AmSAT aims at preserving ``promising'' partial assignments. A partial assignment is considered ``promising'' if it satisfies two conditions: it does not lead to a conflict and it has a relatively long assignment trail.
	 
	Building on this, we further modified \textit{AmSAT}'s rephasing strategy. Specifically, \textit{AmSAT}'s original rephasing strategy randomly selects between two branches, \texttt{info\_based} and \texttt{rand\_based}, after each restart. We extended this approach to randomly select among three branches: \texttt{info\_based}, \texttt{rand\_based}, and \texttt{in\_priority}. The implementation of \texttt{in\_priority} is exactly the same as the rephasing strategy used in \textit{ASSAT\_inPriority}.
	
	
	

	\subsection{ASSAT\_Cadical}

In this solver, we replace the original the \textit{Minisat} SAT solver of \textit{ArgSemSAT} with the \textit{Cadical} SAT solver. Motivated by our empirical observations regarding the propagation strength of \texttt{in}-labeled arguments, we configure the initial phase assignments such that variables corresponding to \texttt{in} labels are initialized to \texttt{true}, whereas all other variables are initialized to \texttt{false}. This heuristic notably improves the solver’s performance by guiding the search toward promising regions of the solution space.

	\subsection{ASSAT\_LLM}

In this solver, we integrate \textit{ArgSemSAT} with large language models to enhance the branching decision process by associating the polarity selection of branching variables with the historical frequency of conflict triggers. Specifically, the solver prefers to explore the polarity direction that has led to fewer conflicts. Leveraging large language models, we generate diverse heuristic strategies and establish an automated framework for code generation and strategy evaluation. Through an evolutionary iteration strategy, we enable a directed exploration of the strategy space, ultimately identifying the optimal conflict-driven branching heuristic.

	
	

	
	
	\section{Summary}
	
	We presented four SAT-based solvers designed for various reasoning tasks in abstract argumentation frameworks. These solvers integrate techniques including customized rephasing strategies based on \texttt{in}-labelled argument behaviors, relaxed backtracking for preserving promising partial assignments, and the use of large language models to automatically generate and refine branching heuristics via evolutionary search. Each solver targets a different aspect of search efficiency and solution quality. The source code for all solvers is available at The source code for all solvers is available at \url{https://github.com/36298liu/Solvers-for-ICCMA-2025}.
	
	
	
	
	
	
	\begin{thebibliography}{00}
		
		\bibitem{b1} F. Cerutti, M. Vallati, and M. Giacomin, ``ArgSemSAT: Solving Argumentation Problems Using SAT,'' in \textit{Proc. 5th Int. Conf. on Computational Models of Argument (COMMA 2014)}, Frontiers in Artificial Intelligence and Applications, vol. 266, IOS Press, 2014, pp. 455--456.
		
		\bibitem{b2} S. Modgil and M. Caminada, ``Proof theories and algorithms for abstract argumentation frameworks,'' in \textit{Argumentation in Artificial Intelligence}, I. Rahwan and G. R. Simari, Eds. Boston, MA: Springer, 2009, pp. 105--129.
		
		\bibitem{b3} M. Luo, J. Xiong, N. He, C. Xiong, X. Wu, and J. Wu, ``An in-label prioritizing variable branching strategy of SAT solvers for a preferred extension of argumentation frameworks,'' in \textit{PRICAI 2024: Trends in Artificial Intelligence}, vol. 5, Springer, 2025, pp. 216--231.
		
		\bibitem{b4} S. Li, C.-M. Li, M. Luo, J. Coll, S. Cherif, D. Habet, and F. Manyà, ``ESA Solvers, Kissat MAB Binary and AMSAT in SAT competition 2023,'' in \textit{Proc. of SAT Competition 2023 – Solver and Benchmark Descriptions}, 2023, pp. 32--33.
		
		\bibitem{b5}S. Cai and X. Zhang, ``Four Relaxed CDCL Solvers,'' in \textit{Proceedings of SAT Race 2019: Solver and Benchmark Descriptions}, University of Helsinki, 2019, pp. 35--38.	
		
		
		
		
		
		
		
		
			
		
	\end{thebibliography}
	
	
	
\end{document}
