Realization of Solving Polynomial System of Equations Based on MiniSat
Zou Xiang-jin · 2015
In many research works of formal analysis and verification,it is often required to solve the polynomial equations associated with a problem. When the scale of the polynomial equations is large,it is difficult to get the solution,which greatly limits the efficiency of analysis. To solve the problem,an algorithm was designed in this paper which transforms polynomial equations with a certain format into conjunctive normal forms,thus the problem of solving polynomial equations can be turned to solve a boolean satisfiability problem( SAT). The SAT solver Mini Sat was applied to solve the polynomial equations in GF(2) so that a solution can be found quickly and make the analysis more efficient. Experiment results show that the proposed algorithm can convert polynomial equations correctly,and a solution can be found quickly with Mini Sat.