Benchmarking Algebraic,
Logical and Constraint Solvers
and Study of Selected Hard Problems

page maintained by Nicolas T. Courtois.

Main objective: Study the hardness of randomly generated dense or sparse MQ problems, and SAT problems. We concentrate on systems which are generated at random in such a way that they have a solution (or a small number of solutions). Interesting systems are systems which are sparse, overdefined, or both.

Generating standard instances of hard problems used to benchmark different solving algorithms such as generic Gröbner basis algorithms, ElimLin, SAT solvers, constraint satisfaction algorithms, specialized or advanced methods such as (geometric) T' methods, etc.

Our Program Tool

We have a ready program axel.exe to generate as a file on a hard drive, various systems of equations and hard problems to benchmark various solvers against each other.

It also includes a number of embedded solvers which can be activated through command line options. We will give here a short legend on how to use it with some embedded solvers, the list of command line switches in terms of solvers given here is not exhaustive, and in general there are some extra options available, which will be very similar as many options which exist for another program, XL0.exe , which are documented here at tools.html.

Remark: if axel.exe does not work on your computer try to install Visual Studio 6 (or just some some missing dlls) on your PC. The file XL0.exe and for certain options even more extra files must be found in the same directory. These extra files can be downladed from tools.html.

Copyright: The exe files (closed-source code programs) provided here can be used freely if the user acknowledges that they use tools developed by Nicolas T. Courtois AND links to this page. Source code is not available.

Random Dense and Sparse MQ Systems of Equations

In order to generate a random dense system of multivariate quadratic equations with m equations and n variables, we type:

Again, all systems are generated in such a way that they have 1 solution, and may have more solutions which will occur by accident. To do this we generate a random system as above, generate a random solution, and adjust the constants in the system so that this solution satisifies all the equations. Moreover, for smaller n up to n=24 systems actually will have a unique solution, this is checked by brute force. For larger systems it is impossible to guarantee that the system have no extra solutions, but it is easy to see that on average the number of extra solutions will be small, like 0,1 or 2 extra solutions.

SAT Solving Challenges

This generator is a beta. In order to generate a random k-SAT system m clauses and n variables, we type: 

  • an internal solver to find contradictions based on unit propagation (elimination of clauses of length 1) is also implemented, currently always active
  • another internal solver to find contradictions based the graph algorithm for 2-SAT is also implemented, currently always active
  • conversion of CNF to ANF and using algebraic solvers such as ElimLin, XL or Gröbner bases, is also implemented: 
    • for now we can try the special option /tp, which does convert a 3-SAT problem to a system of cubic equations. Then it applied the ElimLin algorithm. Then it tries the (standard) T' method which is a very powerful solver able to generate new equations which would have been found by certain Gröbner bases algorithms at a higher degree and with much more memory. However it is quite slow and is far from being optimised (it kind of finds the same equations many times). Requires XL0.exe and Tp.exe.

  • Multiplicative Complexity Challenges - Linear Algebra

    These are optimisation problems which minimize the number of multiplications in various circuits. 
    We need at least these four programs, axel.exe and mp.exe with  XL0.exe and MiniSat206.exe.
    With some options more programs are needed (similar options as elsewhere).

    In order to find a method for multipying nxn matrices within m=23  multiplications we type:

    With this program we have obtained results on problems which remained open for more than 30 years, like Laderman 3x3 matrix multiplication method. See this paper.

  • Multiplicative Complexity Challenges - Sboxes

    We dispose of ready software to optimize any S-box and PROVE the one cannot do better (optimality).
    To be published soon...

  • This page is a subspace of the page.

  • Maintained by Nicolas T. Courtois
    Last updated on 18th of July 2007.