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.
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.
In order to generate a random dense system of multivariate quadratic equations with m equations and n variables, we type:
Examples of dense MQ problems generated by this program can be seen here: few MQ challenges to solve. They have no trapdoor and no hidden structure. We encourage the researchers to solve these systems by their favourite method (one solution is enough, it is not demanded to find all of them). We will post their timings on this page.
no option but with switch /up3 will expand the equations to the degree 3 as in the XL algorithm, and then apply the ElimLin algorithm as one possible final step. It can be seen as a powerful version of the XL algorithm, neiher the best, nor the worst.
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:
- option /elite uses a preprocessor, famous SatElite, this can be combined with any other SAT solver, but should not be needed with MiniSat because it is already kind of embedded inside(!). It requires the file SatElite2005.exe to be present in the current directory.
- by default it uses MiniSat 2.0.6. compiled under cygwin but only if it is present under the fixed path c:\cygwin\sat\minisat20.exe exactly.
- otherwise it will try to use MiniSat2.exe compiled under windows which needs to be present in the current directory.
- option /minisat114 uses even an older version 1.14 if present under c:\cygwin\sat\MiniSat_v1.14_cygwin exactly.
- /minisat206 and /minisat207 and /minisat220 will use a specific version like MiniSat206.exe or MiniSat207.exe or MiniSat220.exe exactly, and only if present.
- /minisat64220 and /minisat64206 are two 64-bit versions of MiniSat to try. Requires Windows x64 and the right exe file: MiniSatx64v220.exe or MiniSatx64v206.exe to be present in the current directory.
- /cryptominisat209 and /cryptominisat64209 are two recent versions (2011) of the famous CryptoMiniSat by Mate Soos. The second being 64-bit. Requires the corresponding compiled exe file and dll bundled here for convenience: CryptoMiniSat209_32-bit_Intel.zip or CryptoMiniSat209_64-bit_Intel.zip to be present in the current directory.
- /pico will use PicoSat which needs picostat.exe to be in the same directory.
- /goX /depY is a stochastic parallel SAT solver. Here we split the task through adding extra Y assumptions. /depY does NOT need to be specified, and will be decreased automatically.
- /koX is the same but only variables starting with k_i are used for assumptions.
- also /zooX is another major parallelization option which tries different solvers, it is very messy, requires XL0.exe and extra files, creates subdirectories with even more extra files.
- /soos1 and /soos2 are two different versions of MiniSat with embedded Gauss, developed by Mate Soos, the file minisat_gauss.exe or this one minisat_gauss2.exe needs to be in the same directory.
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:
- option /elite uses a preprocessor, famous SatElite, requires SatElite2005.exe to be present.
- /minisat64206 is a 64-bit version of MiniSat to try. Requires Windows x64 and the right exe file MiniSatx64v206.exe to be present.
- /goX is an experimental parallel SAT solver which will use X CPUs.
- used alone, option /zooX is another major parallelization option.
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...