基于MiniSat的多项式方程组求解实现

摘要

在许多分析验证研究中,经常要对问题中的多项式组进行求解。当多项式方程组规模较大时,求解比较困难,大大限制了分析研究的效率。针对该问题设计了一种算法,将具有一定格式的多项式转化为合取范式形式,使多项式求解问题转化为SAT求解问题。利用SAT求解器Mini Sat对二元域上的多项式组进行求解,使得密码分析过程更加高效。实验结果表明:该算法能正确地将多项式进行转化,并能快速利用Mini Sat求出结果。