One of the most efficient techniques for solving polynomial systems over is to convert the problem to a satisfiability problem and to use a standard SAT solver. In the past, I have used CryptoMiniSat and either my own ANF to CNF converter scripts based on Gregory Bard’s ideas or PolyBoRi’s script.
However, this setup leaves much to be desired:
- It’s all based on string parsing which has some overhead.
- Usually the instances produced using PolyBoRi’s conversion method are faster to solve. However, as the number of variables per equation increase this method becomes essentially exponentially more expensive. Hence, a compromise between the two techniques is needed.
- We don’t have access to learnt clauses and conflict clauses.
- It all feels a bit duct taped and fragile, partly because the code is not shipped with Sage.