diff --git a/.github/workflows/ci-cd-develop.yml b/.github/workflows/ci-cd-develop.yml index 34401629..18835680 100644 --- a/.github/workflows/ci-cd-develop.yml +++ b/.github/workflows/ci-cd-develop.yml @@ -7,7 +7,7 @@ jobs: check: runs-on: ubuntu-latest container: - image: debian:bookworm-slim # use the same image as our docker runner + image: debian:bullseye-slim # use the same image as our docker runner steps: - name: Clone repo (shallow) uses: actions/checkout@v3 diff --git a/Dockerfile b/Dockerfile index 1bc8bacd..64e16eae 100644 --- a/Dockerfile +++ b/Dockerfile @@ -29,7 +29,7 @@ RUN jlink \ --compress=2 # Step 2: Install the toolbox + external dependencies to a runner container -FROM debian:bookworm-slim AS runner +FROM debian:bullseye-slim AS runner WORKDIR /app COPY scripts scripts diff --git a/solvers/custom/sharp-sat/README.md b/solvers/custom/sharp-sat/README.md deleted file mode 100644 index 016f398e..00000000 --- a/solvers/custom/sharp-sat/README.md +++ /dev/null @@ -1,9 +0,0 @@ -# Usage - * sharpSAT [options] [CNF_File] - * Options: - * -noPP turn off preprocessing - * -noCC turn off component caching - * -noIBCP turn off implicit BCP - * -q quiet mode - * -t [s] set time bound to s seconds - * -cs [n] set max cache size to n MB diff --git a/solvers/custom/sharp-sat/sharp-sat-solver-linux b/solvers/custom/sharp-sat/sharp-sat-solver-linux deleted file mode 100755 index d29f698d..00000000 Binary files a/solvers/custom/sharp-sat/sharp-sat-solver-linux and /dev/null differ diff --git a/solvers/qrisp/sat/exact_sat.py b/solvers/qrisp/sat/exact_sat.py deleted file mode 100644 index 81bb7ef9..00000000 --- a/solvers/qrisp/sat/exact_sat.py +++ /dev/null @@ -1,93 +0,0 @@ -import argparse -import os -import platform -import subprocess -import tempfile -from qrisp.grover import grovers_alg -from qrisp import * -from qrisp_sat_utils import parse_dimacs, sat_oracle, write_output - -parser = argparse.ArgumentParser( - prog="Qrisp Grover SAT Solver", - description="A CLI Program to solve SAT problems in DIMACS CNF format with Qrisp" -) - -parser.add_argument("input_file") -parser.add_argument("--sharp-sat-directory", required=True) -parser.add_argument("--output-file") -args = parser.parse_args() - -sharp_sat_directory = os.path.abspath(args.sharp_sat_directory) -if not os.path.isdir(sharp_sat_directory): - raise FileNotFoundError(f"Sharp-SAT directory not found: {sharp_sat_directory}") - -# temporary .cnf file for the binary -input_file_path = os.path.abspath(args.input_file) -if not os.path.isfile(input_file_path): - raise FileNotFoundError(f"Input file not found: {input_file_path}") - -with tempfile.TemporaryDirectory() as temp_dir: - temp_cnf_path = os.path.join(temp_dir, "problem.cnf") - - with open(input_file_path, "r") as src, open(temp_cnf_path, "w") as dest: - dest.write(src.read()) - - system = platform.system().lower() - - if system == "windows": - binary_name = "sharp-sat-solver-win.exe" - elif system == "darwin": # macOS - binary_name = "sharp-sat-solver-mac" - elif system == "linux": - binary_name = "sharp-sat-solver-linux" - else: - raise OSError("Unsupported operating system") - - binary_path = os.path.join(sharp_sat_directory, binary_name) - - if not os.path.isfile(binary_path): - raise FileNotFoundError(f"Solver binary not found at {binary_path}") - - try: - result = subprocess.run( - [binary_path, temp_cnf_path], - cwd=sharp_sat_directory, - stdout=subprocess.PIPE, - stderr=subprocess.PIPE, - text=True, - check=True, - ) - sharpSolverResult = result.stdout - - except subprocess.CalledProcessError as e: - raise RuntimeError(f"Solver execution failed: {e.stderr}") from e - -try: - start_tag = "# solutions" - end_tag = "# END" - start_idx = sharpSolverResult.index(start_tag) + len(start_tag) - end_idx = sharpSolverResult.index(end_tag) - solutionNumber = int(sharpSolverResult[start_idx:end_idx].strip()) -except (ValueError, IndexError): - raise ValueError("Failed to parse the output. Ensure the output contains the expected tags.") - -if solutionNumber == 0: - if args.output_file: - with open(args.output_file, 'w') as f: - f.write("s UNSATISFIABLE\n") - else: - print("s UNSATISFIABLE") - exit() - -num_vars, clauses = parse_dimacs(args.input_file) -qvars = [QuantumBool() for _ in range(num_vars)] - -grovers_alg( - qvars, - sat_oracle, - exact=True, - winner_state_amount=solutionNumber, - kwargs={"sat_clauses": clauses}, -) - -write_output(qvars, args.output_file) diff --git a/src/main/java/edu/kit/provideq/toolbox/featuremodel/anomaly/dead/SatBasedDeadFeatureSolver.java b/src/main/java/edu/kit/provideq/toolbox/featuremodel/anomaly/dead/SatBasedDeadFeatureSolver.java index 5625edbf..c86eccce 100644 --- a/src/main/java/edu/kit/provideq/toolbox/featuremodel/anomaly/dead/SatBasedDeadFeatureSolver.java +++ b/src/main/java/edu/kit/provideq/toolbox/featuremodel/anomaly/dead/SatBasedDeadFeatureSolver.java @@ -20,7 +20,6 @@ import reactor.util.function.Tuple2; import reactor.util.function.Tuples; -// TODO: understand timeout error for qrisp sat solver. /** * This problem solver solves the {@link DeadFeatureConfiguration#FEATURE_MODEL_ANOMALY_DEAD} * problem by building {@link SatConfiguration#SAT} formulae that are solved by a corresponding diff --git a/src/main/java/edu/kit/provideq/toolbox/sat/SatConfiguration.java b/src/main/java/edu/kit/provideq/toolbox/sat/SatConfiguration.java index 3b433558..6a52617b 100644 --- a/src/main/java/edu/kit/provideq/toolbox/sat/SatConfiguration.java +++ b/src/main/java/edu/kit/provideq/toolbox/sat/SatConfiguration.java @@ -6,7 +6,6 @@ import edu.kit.provideq.toolbox.meta.Problem; import edu.kit.provideq.toolbox.meta.ProblemManager; import edu.kit.provideq.toolbox.meta.ProblemType; -import edu.kit.provideq.toolbox.sat.solvers.ExactQrispSatSolver; import edu.kit.provideq.toolbox.sat.solvers.GamsSatSolver; import edu.kit.provideq.toolbox.sat.solvers.QrispSatSolver; import java.io.IOException; @@ -35,12 +34,11 @@ public class SatConfiguration { ProblemManager getSatManager( GamsSatSolver gamsSolver, QrispSatSolver qrispSolver, - ExactQrispSatSolver exactQrispSolver, ResourceProvider resourceProvider ) { return new ProblemManager<>( SAT, - Set.of(gamsSolver, qrispSolver, exactQrispSolver), + Set.of(gamsSolver, qrispSolver), loadExampleProblems(resourceProvider) ); } diff --git a/src/main/java/edu/kit/provideq/toolbox/sat/solvers/ExactQrispSatSolver.java b/src/main/java/edu/kit/provideq/toolbox/sat/solvers/ExactQrispSatSolver.java deleted file mode 100644 index b0450c57..00000000 --- a/src/main/java/edu/kit/provideq/toolbox/sat/solvers/ExactQrispSatSolver.java +++ /dev/null @@ -1,82 +0,0 @@ -package edu.kit.provideq.toolbox.sat.solvers; - -import edu.kit.provideq.toolbox.Solution; -import edu.kit.provideq.toolbox.exception.ConversionException; -import edu.kit.provideq.toolbox.format.cnf.dimacs.DimacsCnf; -import edu.kit.provideq.toolbox.format.cnf.dimacs.DimacsCnfSolution; -import edu.kit.provideq.toolbox.meta.SolvingProperties; -import edu.kit.provideq.toolbox.meta.SubRoutineResolver; -import edu.kit.provideq.toolbox.process.ProcessResult; -import edu.kit.provideq.toolbox.process.ProcessRunner; -import edu.kit.provideq.toolbox.process.PythonProcessRunner; -import edu.kit.provideq.toolbox.sat.SatConfiguration; -import org.springframework.beans.factory.annotation.Value; -import org.springframework.context.ApplicationContext; -import org.springframework.stereotype.Component; -import reactor.core.publisher.Mono; - -/** - * {@link SatConfiguration#SAT} solver using the Exact QRISP implementation. - */ -@Component -public class ExactQrispSatSolver extends SatSolver { - private final String scriptPath; - private final String sharpSatDirectory; - private final ApplicationContext context; - - public ExactQrispSatSolver( - @Value("${qrisp.script.exact-sat}") String scriptPath, - @Value("${custom.directory.sharp-sat.directory}") String sharpSatDirectory, - ApplicationContext context) { - this.scriptPath = scriptPath; - this.sharpSatDirectory = sharpSatDirectory; - this.context = context; - } - - @Override - public String getName() { - return "Exact QRISP SAT"; - } - - @Override - public Mono> solve( - String input, - SubRoutineResolver subRoutineResolver, - SolvingProperties properties - ) { - var solution = new Solution<>(this); - - DimacsCnf dimacsCnf; - try { - dimacsCnf = DimacsCnf.fromString(input); - solution.setDebugData("Using CNF input: " + dimacsCnf); - } catch (ConversionException | RuntimeException e) { - solution.setDebugData("Parsing error: " + e.getMessage()); - solution.abort(); - return Mono.just(solution); - } - - ProcessResult processResult = context - .getBean(PythonProcessRunner.class, scriptPath) - .withArguments( - ProcessRunner.INPUT_FILE_PATH, - "--sharp-sat-directory", sharpSatDirectory, - "--output-file", ProcessRunner.OUTPUT_FILE_PATH - ) - .writeInputFile(dimacsCnf.toString()) - .readOutputFile() - .run(getProblemType(), solution.getId()); - - if (processResult.success()) { - var dimacsCnfSolution = - DimacsCnfSolution.fromString(dimacsCnf, processResult.output().orElse("")); - - solution.setSolutionData(dimacsCnfSolution); - solution.complete(); - } else { - solution.setDebugData(processResult.errorOutput().orElse("Unknown error occurred.")); - solution.fail(); - } - return Mono.just(solution); - } -} diff --git a/src/main/resources/application.properties b/src/main/resources/application.properties index 2dff2cd7..111df634 100644 --- a/src/main/resources/application.properties +++ b/src/main/resources/application.properties @@ -28,7 +28,6 @@ qrisp.directory=${solvers.directory}/qrisp qrisp.script.vrp=${qrisp.directory}/vrp/grover.py qrisp.script.qubo=${qrisp.directory}/qubo/qaoa.py qrisp.script.sat=${qrisp.directory}/sat/sat.py -qrisp.script.exact-sat=${qrisp.directory}/sat/exact_sat.py dwave.directory=${solvers.directory}/dwave dwave.script.qubo=${dwave.directory}/qubo/main.py @@ -37,7 +36,6 @@ dwave.script.qubo=${dwave.directory}/qubo/main.py custom.directory=${solvers.directory}/custom custom.script.hs_knapsack=${custom.directory}/hs-knapsack/knapsack.py custom.directory.lkh.directory=${custom.directory}/lkh -custom.directory.sharp-sat.directory=${custom.directory}/sharp-sat custom.script.lkh=${custom.directory.lkh.directory}/vrp_lkh.py custom.directory.berger-vrp=${custom.directory}/berger-vrp diff --git a/src/test/java/edu/kit/provideq/toolbox/api/FeatureModelAnomalySolversTest.java b/src/test/java/edu/kit/provideq/toolbox/api/FeatureModelAnomalySolversTest.java index 4d26f496..b6a2e360 100644 --- a/src/test/java/edu/kit/provideq/toolbox/api/FeatureModelAnomalySolversTest.java +++ b/src/test/java/edu/kit/provideq/toolbox/api/FeatureModelAnomalySolversTest.java @@ -10,7 +10,6 @@ import edu.kit.provideq.toolbox.meta.ProblemSolver; import edu.kit.provideq.toolbox.meta.ProblemState; import edu.kit.provideq.toolbox.meta.ProblemType; -import edu.kit.provideq.toolbox.sat.solvers.ExactQrispSatSolver; import edu.kit.provideq.toolbox.sat.solvers.QrispSatSolver; import java.time.Duration; import java.util.stream.Stream; @@ -56,8 +55,7 @@ Stream getArguments( var satManager = problemManagerProvider.findProblemManagerForType(SAT).get(); var satSolver = satManager.getSolvers().stream() - .filter(solver -> !(solver instanceof QrispSatSolver - || solver instanceof ExactQrispSatSolver)) + .filter(solver -> !(solver instanceof QrispSatSolver)) .toList(); return ApiTestHelper.getAllArgumentCombinations(featureModelManager, satSolver)