This paper introduces the XOR-OR-AND normal form (XNF) for logical formulas. It is a generalization of the well-known Conjunctive Normal Form (CNF) where literals are replaced by XORs of literals. As a first theoretic result, we show that every formula is equisatisfiable to a formula in 2-XNF, i.e., a formula in XNF where each disjunction involves at most two XORs of literals. Subsequently, we present an algorithm which converts Boolean polynomials efficiently from their Algebraic Normal Form (ANF) to formulas in 2-XNF. Experiments with the cipher ASCON-128 show that cryptographic problems, which by design are based strongly on XOR-operations, can be represented using far fewer variables and clauses in 2-XNF than in CNF. In order to take advantage of this compact representation, new SAT solvers based on input formulas in 2-XNF need to be designed. By taking inspiration from graph-based 2-CNF SAT solving, we devise a new DPLL-based SAT solver for formulas in 2-XNF. Among others, we present advanced pre- and in-processing techniques. Finally, we give timings for random 2-XNF instances and instances related to key recovery attacks on round reduced ASCON-128, where our solver outperforms state-of-the-art alternative solving approaches.

翻译：本文提出逻辑公式的XOR-OR-AND范式（XNF），它是经典合取范式（CNF）的推广形式，其中文字被替换为文字的异或运算。作为首个理论结果，我们证明每个公式均可等可满足地转换为2-XNF公式，即每个析取项最多包含两个文字异或运算的XNF公式。随后，我们提出一种算法，可将布尔多项式从代数标准型（ANF）高效转换为2-XNF公式。针对密码算法ASCON-128的实验表明，因设计特性而强烈依赖于异或运算的密码问题，在2-XNF中使用的变量和子句数量远少于CNF中。为利用这种紧凑表示，需要设计基于2-XNF输入公式的新型SAT求解器。受图论驱动的2-CNF SAT求解方法启发，我们为2-XNF公式开发了基于DPLL的新SAT求解器，并提出了先进的预处理与内处理技术。最后，针对随机2-XNF实例及与轮缩减ASCON-128上的密钥恢复攻击相关实例的计时结果表明，我们的求解器在性能上优于现有最优替代求解方案。