Exact Qrisp SAT Solver

[tubadzin]

• Works on Add exact qrisp SAT solver #110
• This PR depends on Implement SharpSAT Solution Space Approximator for Exact Qrisp Sat Solver #112
• This branch implements python qrisp solver, which solves given SAT dimacs with the exact groover algorithm.
• It requires both update-docker-image and sharp-sat branches to work.

exact_sat.py and the corresponding ExactQrispSatSolver class

This variant utilizes (almost) the same logic as the default QrispSatSolver. The key difference is that this version (in theory) avoids considering impossible variable assignments. For this, the Oracle needs to know the size of the solution space.

sharp-sat-solver

As mentioned above, exact_sat.py requires the size of the solution space to function correctly. To address this, I have added a Linux binary that, given a .cnf file, approximates the number of solutions. Unfortunately, this approximation fails in trivial cases where the .cnf file is unsatisfiable, such as:

p cnf 1 2
1 0
-1 0

This case should obviously return 0, but the solver instead returns 1 or 2 (if pre-processing is disabled). The issue arises because the solver simplifies contradictory clauses, and once removed, the remaining formula is interpreted as having no constraints, allowing x to take any value (both true and false).

Additionally, I attempted to compile this program for Windows, but to no avail. Both cross-compiling and building it on my Windows machine failed. This led me down a long rabbit hole where I replaced platform-dependent code iteratively. While I eventually managed to build an .exe, it still produced errors when running. I have yet to find another SharpSAT solver that works on Windows. Some alternatives I considered are:

• sharpSAT
• d4
• sharpSAT-TD
• miniC2D
• Ganak
• approxmc

[Elscrux]

Looks good! Just one small request.

[sonarqubecloud]

Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
6.3% Duplication on New Code

See analysis details on SonarQube Cloud