Qrisp sat solver

[tubadzin]

Qrisp-grover-sat solver implementation. Works on #114.

[tubadzin]

Intro

Here’s a brief recap of the changes:

Changes

sat.py and the corresponding QrispSatSolver.java class

A detailed explanation of what is happening can be found in the qrisp_sat_utils.py script, specifically in the comments for the sat_oracle method.

Exclusion of Quantum SAT Solvers in the dead/anomaly tests

The QrispSatSolver has a notable issue: in cases such as:

p cnf 1 2
1 0
-1 0

It outputs a result indicating a 50% probability of true and a 50% probability of false assignments. I attempted to differentiate between cases where both assignments (true and false) are valid versus cases that are outright impossible using SharpSAT—by checking if the number of solutions is greater than 0. However, this approach is unreliable due to inconsistencies in SharpSAT's output. Since SAT solving is NP-hard, using exact solvers without approximators is impractical.

Anomaly tests take as input a featureModelSolver, problemType, input, and satSolver. In these tests, SAT solvers are used as subroutines on the given feature model. Because of this, it is difficult to hand-pick small examples that would run correctly on the quantum simulation—and even if they did, the results would likely be incorrect. Consequently, I decided to exclude QrispSatSolvers entirely from these tests.

---

Problems & Questions

1. Code Duplication:
   SonarCloud code analysis reports 27.5% code duplication between sat.py and exact_sat.py. While I could artificially remove the duplications, I believe the code is currently more readable as it is. Should I prioritize readability or reduce duplication?

2. SharpSAT on Windows:
   What should I do about the lack of a working SharpSAT binary for Windows?

[tubadzin]

Meeting notes 13.01.24

• Split exact Grover, approximate Grover and CI / CD changes into different branches
• Change SonarCloud restrictions. They are at times too limiting - in this case would lead to less readable code.
• Domenik and me scheduled a separate meeting. The goal is to think about if the exact groover approach is needed, especially if the needed sharpSAT dependency is faulty and does not yield the wanted solutions.

[sonarqubecloud]

Quality Gate failed

Failed conditions
28.4% Duplication on New Code (required ≤ 3%)

See analysis details on SonarQube Cloud

[tubadzin]

This PR is now complemented by:

• Update Docker Image Update Docker Image for Qrisp SAT Solver #111
• Add Sharp SAT Variant Implement SharpSAT Solution Space Approximator for Exact Qrisp Sat Solver #112
• Add Exact Qrisp SAT Solver Variant Add Exact Qrisp SAT Solver Variant #113

Although both this issue and #113 are similar, the latter has required changes in dependencies, extra binaries and deeper changes to the project. For simplicity and good structure, they are now separated.

[koalamitice]

Looks good. I would prefer to have the small naming changes included, then its ready to merge. I will write a reminder that we improve the names of the other solvers aswell...
I just looked them up for reference... :D

[koalamitice]

I would prefer a more descriptive name (we messed this up at some other solvers aswell).
How about "Grover-Search (Qrisp)"

[koalamitice]

Maybe name this "grover" and the exact one "exact_grover" (cause sat is specified in the parent directory)