Axel Kemper

Using Msys64 (MingGW), the following will build CaDiCal under Windows: ``` #!/bin/bash # change ~/cppsrc to your source root directory cd ~/cppsrc [ -d cadical ] && rm -rf cadical...

Thank you for your time and your gracious help. I tried the following: ``` bit7z::Bit7zLibrary lib{ LR"(C:\util\7z.dll)" }; void compress(const std::vector& data, std::vector& compressed) { try { bit7z::BitArchiveWriter writer(lib, bit7z::BitFormat::GZip);...

That makes sense. Thank you again! I've now managed to make it work. Please find my code attached as example usage of `bit7z`. [BZip7.zip](https://github.com/user-attachments/files/16589759/BZip7.zip)

Perhaps, my Boolean simplifier for MiniZinc might be of interest to you: https://github.com/hakank/hakank/issues/20 Greetings, Axel Kemper

Cryptominisat has a hard-coded limit of `2^28 = 268,435,456` variables. See source code line 150 in [dimacsparser.h](https://github.com/msoos/cryptominisat/blob/master/src/dimacsparser.h). Perhaps you can try to come up with some preprocessing to partition your...

358,404,470 is 2^28.41 and therefore beyond the limit. The high number of clauses is problematic. I don't have CNF examples with more than 200,000 clauses. Have a look at [this...

This variant works on [Playground](https://play.minizinc.dev/#project=%7B%22files%22%3A%5B%7B%22name%22%3A%22Playground.mzn%22%2C%22contents%22%3A%22set%20of%20int%3A%20emptySet%20%3D%20%7B%7D%3B%5Cnset%20of%20int%3A%20X%20%3D%20%7B1%2C3%2C5%7D%20diff%20(2..5%20union%201..0)%3B%5Cnset%20of%20int%3A%20Y%20%3D%20%7B1%2C3%2C5%7D%20diff%20(2..5%20union%20emptySet)%3B%5Cnoutput%20show(%5BX%2CY%5D)%3B%22%7D%5D%2C%22tab%22%3A0%2C%22solverId%22%3A%22org.minizinc.gecode_presolver%22%2C%22solverConfig%22%3A%7B%22enableTimeLimit%22%3Afalse%2C%22timeLimit%22%3A1%2C%22allSolutions%22%3Afalse%2C%22verboseCompilation%22%3Afalse%2C%22verboseSolving%22%3Afalse%2C%22compilerStatistics%22%3Afalse%2C%22solvingStatistics%22%3Afalse%2C%22outputTime%22%3Afalse%2C%22freeSearch%22%3Afalse%7D%2C%22minizincVersion%22%3A%22latest%22%7D): ``` set of int: emptySet = {}; set of int: X = {1,3,5} diff (2..5 union 1..0); set of int: Y = {1,3,5} diff (2..5...

Internally, `-9223372036854775808` seems to be fine: ``` int: a = -9223372036854775807 - 1; int: b = 9223372036854775807; output ["\(a) \(b)"]; ``` The backend solvers have their own integer limits.