Add solver characteristics based on theoretical paper concepts

.gitignore

@@ -43,6 +43,7 @@ out/
 
 ### virtual envs and python ###
 venv/
+.venv/
 __pycache__/
 
 ### ProvideQ toolbox-server ###

src/main/java/edu/kit/provideq/toolbox/ProblemSolverInfo.java

@@ -1,5 +1,12 @@
 package edu.kit.provideq.toolbox;
 
-public record ProblemSolverInfo(String id, String name, String description) {
+import edu.kit.provideq.toolbox.meta.SolverCharacteristics;
 
-}
+public record ProblemSolverInfo(
+    String id,
+    String name,
+    String description,
+    SolverCharacteristics characteristics
+) {
+
+}

src/main/java/edu/kit/provideq/toolbox/Solution.java

@@ -21,6 +21,7 @@ public class Solution<S> {
   private String debugData;
   private String solverName;
   private long executionMilliseconds;
+  private String guardRejection;
 
   /**
    * Internal constructor, used for de-serialization.
@@ -57,6 +58,7 @@ public static <I, S, T> Solution<T> from(
     result.metaData = source.metaData;
     result.debugData = source.debugData;
     result.executionMilliseconds = source.executionMilliseconds;
+    result.guardRejection = source.guardRejection;
     result.solutionData = source.solutionData == null ? null : mapper.apply(source.solutionData);
     return result;
   }
@@ -96,6 +98,7 @@ public Solution<String> toStringSolution(@NotNull Function<S, String> stringSele
     stringSolution.debugData = debugData;
     stringSolution.solverName = solverName;
     stringSolution.executionMilliseconds = executionMilliseconds;
+    stringSolution.guardRejection = guardRejection;
     return stringSolution;
   }
 
@@ -166,6 +169,14 @@ public void setExecutionMilliseconds(long executionMilliseconds) {
     this.executionMilliseconds = executionMilliseconds;
   }
 
+  public String getGuardRejection() {
+    return guardRejection;
+  }
+
+  public void rejectByGuard(String reason) {
+    this.guardRejection = reason;
+  }
+
   @Override
   public boolean equals(Object obj) {
     if (obj == this) {

src/main/java/edu/kit/provideq/toolbox/api/SolversRouter.java

@@ -66,7 +66,7 @@ private Mono<ServerResponse> handleSolversRouteForManager(ProblemManager<?, ?> m
   private static List<ProblemSolverInfo> getAllSolverInfos(ProblemManager<?, ?> manager) {
     return manager.getSolvers().stream()
             .map(solver -> new ProblemSolverInfo(solver.getId(), solver.getName(),
-                solver.getDescription()))
+                solver.getDescription(), solver.getCharacteristics()))
             .toList();
   }
 

src/main/java/edu/kit/provideq/toolbox/api/StrategyDto.java

@@ -0,0 +1,16 @@
+package edu.kit.provideq.toolbox.api;
+
+import edu.kit.provideq.toolbox.meta.Problem;
+import edu.kit.provideq.toolbox.meta.strategy.StrategyCorrectness;
+import edu.kit.provideq.toolbox.meta.strategy.StrategyStep;
+import java.util.List;
+
+public record StrategyDto(
+    List<StrategyStep> steps,
+    StrategyCorrectness correctness
+) {
+  public static StrategyDto fromProblem(Problem<?, ?> problem) {
+    var steps = StrategyStep.collect(problem);
+    return new StrategyDto(steps, StrategyCorrectness.evaluate(steps));
+  }
+}

src/main/java/edu/kit/provideq/toolbox/api/StrategyRouter.java

@@ -0,0 +1,89 @@
+package edu.kit.provideq.toolbox.api;
+
+import static org.springdoc.core.fn.builders.apiresponse.Builder.responseBuilder;
+import static org.springdoc.core.fn.builders.content.Builder.contentBuilder;
+import static org.springdoc.core.fn.builders.parameter.Builder.parameterBuilder;
+import static org.springdoc.core.fn.builders.schema.Builder.schemaBuilder;
+import static org.springdoc.webflux.core.fn.SpringdocRouteBuilder.route;
+import static org.springframework.http.MediaType.APPLICATION_JSON;
+import static org.springframework.http.MediaType.APPLICATION_JSON_VALUE;
+import static org.springframework.web.reactive.function.server.RequestPredicates.accept;
+import static org.springframework.web.reactive.function.server.ServerResponse.ok;
+
+import edu.kit.provideq.toolbox.meta.ProblemManager;
+import edu.kit.provideq.toolbox.meta.ProblemManagerProvider;
+import edu.kit.provideq.toolbox.meta.ProblemType;
+import io.swagger.v3.oas.annotations.enums.ParameterIn;
+import org.springdoc.core.fn.builders.operation.Builder;
+import org.springframework.beans.factory.annotation.Autowired;
+import org.springframework.context.annotation.Bean;
+import org.springframework.context.annotation.Configuration;
+import org.springframework.core.ParameterizedTypeReference;
+import org.springframework.http.HttpStatus;
+import org.springframework.web.reactive.config.EnableWebFlux;
+import org.springframework.web.reactive.function.server.RouterFunction;
+import org.springframework.web.reactive.function.server.ServerRequest;
+import org.springframework.web.reactive.function.server.ServerResponse;
+import reactor.core.publisher.Mono;
+
+@Configuration
+@EnableWebFlux
+public class StrategyRouter {
+  public static final String PROBLEM_ID_PARAM_NAME = "problemId";
+  private ProblemManagerProvider managerProvider;
+
+  @Bean
+  RouterFunction<ServerResponse> getStrategyRoutes() {
+    return managerProvider.getProblemManagers().stream()
+        .map(this::defineGetRoute)
+        .reduce(RouterFunction::and)
+        .orElseThrow();
+  }
+
+  private RouterFunction<ServerResponse> defineGetRoute(ProblemManager<?, ?> manager) {
+    return route().GET(
+        getStrategyRouteForProblemType(manager.getType()),
+        accept(APPLICATION_JSON),
+        req -> handleGet(manager, req),
+        ops -> handleGetDocumentation(manager, ops)
+    ).build();
+  }
+
+  private <InputT, ResultT> Mono<ServerResponse> handleGet(
+      ProblemManager<InputT, ResultT> manager,
+      ServerRequest req
+  ) {
+    var problemId = req.pathVariable(PROBLEM_ID_PARAM_NAME);
+    var problem = RouterUtility.findProblemOrThrow(manager, problemId);
+    var strategyDto = StrategyDto.fromProblem(problem);
+
+    return ok().body(Mono.just(strategyDto), new ParameterizedTypeReference<>() {
+    });
+  }
+
+  private void handleGetDocumentation(ProblemManager<?, ?> manager, Builder ops) {
+    ProblemType<?, ?> problemType = manager.getType();
+    ops
+        .operationId(getStrategyRouteForProblemType(problemType))
+        .tag(problemType.getId())
+        .description("Returns the meta-solver strategy configured for the given problem, meaning "
+            + "the sequence of transformation rules composed by the problem and its sub-problems, "
+            + "together with the correctness verdict that can be made about it.")
+        .parameter(parameterBuilder().in(ParameterIn.PATH).name(PROBLEM_ID_PARAM_NAME))
+        .response(responseBuilder()
+            .responseCode(String.valueOf(HttpStatus.OK.value()))
+            .content(contentBuilder()
+                .mediaType(APPLICATION_JSON_VALUE)
+                .schema(schemaBuilder().implementation(StrategyDto.class)))
+        );
+  }
+
+  private String getStrategyRouteForProblemType(ProblemType<?, ?> type) {
+    return "/problems/%s/{%s}/strategy".formatted(type.getId(), PROBLEM_ID_PARAM_NAME);
+  }
+
+  @Autowired
+  void setManagerProvider(ProblemManagerProvider managerProvider) {
+    this.managerProvider = managerProvider;
+  }
+}

src/main/java/edu/kit/provideq/toolbox/circuit/processing/solvers/MoveToExecutionSolver.java

@@ -3,6 +3,8 @@
 import edu.kit.provideq.toolbox.Solution;
 import edu.kit.provideq.toolbox.circuit.processing.solvers.executor.ExecutionResult;
 import edu.kit.provideq.toolbox.circuit.processing.solvers.executor.ExecutorConfiguration;
+import edu.kit.provideq.toolbox.meta.RuleType;
+import edu.kit.provideq.toolbox.meta.SolverCharacteristics;
 import edu.kit.provideq.toolbox.meta.SolvingProperties;
 import edu.kit.provideq.toolbox.meta.SubRoutineDefinition;
 import edu.kit.provideq.toolbox.meta.SubRoutineResolver;
@@ -29,6 +31,11 @@ public String getDescription() {
     return "Move QASM input to the executors";
   }
 
+  @Override
+  public SolverCharacteristics getCharacteristics() {
+    return SolverCharacteristics.of(RuleType.DELEGATION);
+  }
+
   @Override
   public List<SubRoutineDefinition<?, ?>> getSubRoutines() {
     return List.of(EXECUTOR_SUBROUTINE);

src/main/java/edu/kit/provideq/toolbox/circuit/processing/solvers/MoveToMitigationSolver.java

@@ -2,6 +2,8 @@
 
 import edu.kit.provideq.toolbox.Solution;
 import edu.kit.provideq.toolbox.circuit.processing.solvers.mitigation.ErrorMitigationConfiguration;
+import edu.kit.provideq.toolbox.meta.RuleType;
+import edu.kit.provideq.toolbox.meta.SolverCharacteristics;
 import edu.kit.provideq.toolbox.meta.SolvingProperties;
 import edu.kit.provideq.toolbox.meta.SubRoutineDefinition;
 import edu.kit.provideq.toolbox.meta.SubRoutineResolver;
@@ -28,6 +30,11 @@ public String getDescription() {
     return "Move QASM input to the error mitigators";
   }
 
+  @Override
+  public SolverCharacteristics getCharacteristics() {
+    return SolverCharacteristics.of(RuleType.DELEGATION);
+  }
+
   @Override
   public List<SubRoutineDefinition<?, ?>> getSubRoutines() {
     return List.of(MITIGATOR_SUBROUTINE);

src/main/java/edu/kit/provideq/toolbox/circuit/processing/solvers/MoveToOptimizationSolver.java

@@ -2,6 +2,8 @@
 
 import edu.kit.provideq.toolbox.Solution;
 import edu.kit.provideq.toolbox.circuit.processing.solvers.optimization.OptimizationConfiguration;
+import edu.kit.provideq.toolbox.meta.RuleType;
+import edu.kit.provideq.toolbox.meta.SolverCharacteristics;
 import edu.kit.provideq.toolbox.meta.SolvingProperties;
 import edu.kit.provideq.toolbox.meta.SubRoutineDefinition;
 import edu.kit.provideq.toolbox.meta.SubRoutineResolver;
@@ -28,6 +30,11 @@ public String getDescription() {
     return "Move QASM input to the optimizers";
   }
 
+  @Override
+  public SolverCharacteristics getCharacteristics() {
+    return SolverCharacteristics.of(RuleType.DELEGATION);
+  }
+
   @Override
   public List<SubRoutineDefinition<?, ?>> getSubRoutines() {
     return List.of(OPTIMIZER_SUBROUTINE);

src/main/java/edu/kit/provideq/toolbox/circuit/processing/solvers/executor/ExecutionSolver.java

@@ -3,6 +3,9 @@
 import edu.kit.provideq.toolbox.Solution;
 import edu.kit.provideq.toolbox.meta.ProblemSolver;
 import edu.kit.provideq.toolbox.meta.ProblemType;
+import edu.kit.provideq.toolbox.meta.RuleProperty;
+import edu.kit.provideq.toolbox.meta.RuleType;
+import edu.kit.provideq.toolbox.meta.SolverCharacteristics;
 import edu.kit.provideq.toolbox.meta.SolvingProperties;
 import edu.kit.provideq.toolbox.meta.SubRoutineResolver;
 import edu.kit.provideq.toolbox.meta.setting.SolverSetting;
@@ -50,6 +53,13 @@
     return "Execute an OpenQASM circuit";
   }
 
+  @Override
+  public SolverCharacteristics getCharacteristics() {
+    // TODO: valid only holds true for noise free simulation, add additional executor,
+    //  splitting noisy and noise free
+    return SolverCharacteristics.of(RuleType.SOLVE, RuleProperty.VALID);
+  }
+
   @Override
   public List<SolverSetting> getSolverSettings() {
     return List.of(

src/main/java/edu/kit/provideq/toolbox/circuit/processing/solvers/optimization/OptimizationSolver.java

@@ -4,6 +4,9 @@
 import edu.kit.provideq.toolbox.circuit.processing.solvers.CircuitProcessingSolver;
 import edu.kit.provideq.toolbox.meta.ProblemSolver;
 import edu.kit.provideq.toolbox.meta.ProblemType;
+import edu.kit.provideq.toolbox.meta.RuleProperty;
+import edu.kit.provideq.toolbox.meta.RuleType;
+import edu.kit.provideq.toolbox.meta.SolverCharacteristics;
 import edu.kit.provideq.toolbox.meta.SolvingProperties;
 import edu.kit.provideq.toolbox.meta.SubRoutineDefinition;
 import edu.kit.provideq.toolbox.meta.SubRoutineResolver;
@@ -53,10 +56,18 @@ public String getName() {
 
   @Override
   public String getDescription() {
-    return "Transform the given circuit into an optimized but equivalent circuit using"
+    return "Transform the given circuit into an optimized but equivalent circuit using "
         + "Tket compilation passes (e.g. removing redundancies).";
   }
 
+  @Override
+  public SolverCharacteristics getCharacteristics() {
+    return SolverCharacteristics.of(
+        RuleType.REFORMULATION,
+        RuleProperty.STRONGLY_CONSTRAINT_PRESERVING,
+        RuleProperty.OPTIMAL_SOLUTION_PRESERVING);
+  }
+
   @Override
   public List<SubRoutineDefinition<?, ?>> getSubRoutines() {
     return List.of(CircuitProcessingSolver.CIRCUIT_PROCESSING_SUBROUTINE);

src/main/java/edu/kit/provideq/toolbox/featuremodel/anomaly/dead/SatBasedDeadFeatureSolver.java

@@ -8,6 +8,9 @@
 import edu.kit.provideq.toolbox.format.cnf.dimacs.Variable;
 import edu.kit.provideq.toolbox.meta.ProblemSolver;
 import edu.kit.provideq.toolbox.meta.ProblemType;
+import edu.kit.provideq.toolbox.meta.RuleProperty;
+import edu.kit.provideq.toolbox.meta.RuleType;
+import edu.kit.provideq.toolbox.meta.SolverCharacteristics;
 import edu.kit.provideq.toolbox.meta.SolvingProperties;
 import edu.kit.provideq.toolbox.meta.SubRoutineDefinition;
 import edu.kit.provideq.toolbox.meta.SubRoutineResolver;
@@ -45,6 +48,13 @@ public String getDescription() {
         + " It uses a SAT solver to solve each formula per feature.";
   }
 
+  @Override
+  public SolverCharacteristics getCharacteristics() {
+    return SolverCharacteristics.of(
+        RuleType.DECOMPOSITION, RuleProperty.STRONGLY_CONSTRAINT_PRESERVING,
+        RuleProperty.OPTIMAL_SOLUTION_PRESERVING);
+  }
+
   @Override
   public List<SubRoutineDefinition<?, ?>> getSubRoutines() {
     return List.of(SAT_SUBROUTINE);
@@ -92,7 +102,7 @@ private Mono<Solution<String>> checkDeadFeatures(
 
     return Flux.fromIterable(dimacsCnf.getVariables())
         .flatMap(feature -> checkFeatureDead(dimacsCnf, feature, subRoutineResolver)
-          .map(isVoid -> Tuples.of(feature, isVoid)))
+            .map(isVoid -> Tuples.of(feature, isVoid)))
         .collectMap(Tuple2::getT1, Tuple2::getT2)
         .map(featureIsVoidMap -> {
           var stringBuilder = new StringBuilder();
@@ -123,7 +133,7 @@ private Mono<Solution<String>> checkDeadFeatures(
    *
    * @param subRoutineResolver used to evaluate a SAT formula for the check.
    * @return the solution of the given {@code feature}.
-   *         Use {@link DimacsCnfSolution#isVoid()} to check the feature.
+   *     Use {@link DimacsCnfSolution#isVoid()} to check the feature.
    */
   private static Mono<Boolean> checkFeatureDead(
       DimacsCnf cnf,

src/main/java/edu/kit/provideq/toolbox/featuremodel/anomaly/voidmodel/SatBasedVoidFeatureSolver.java

@@ -6,6 +6,9 @@
 import edu.kit.provideq.toolbox.format.cnf.dimacs.DimacsCnfSolution;
 import edu.kit.provideq.toolbox.meta.ProblemSolver;
 import edu.kit.provideq.toolbox.meta.ProblemType;
+import edu.kit.provideq.toolbox.meta.RuleProperty;
+import edu.kit.provideq.toolbox.meta.RuleType;
+import edu.kit.provideq.toolbox.meta.SolverCharacteristics;
 import edu.kit.provideq.toolbox.meta.SolvingProperties;
 import edu.kit.provideq.toolbox.meta.SubRoutineDefinition;
 import edu.kit.provideq.toolbox.meta.SubRoutineResolver;
@@ -37,6 +40,14 @@ public String getName() {
     return List.of(SAT_SUBROUTINE);
   }
 
+  @Override
+  public SolverCharacteristics getCharacteristics() {
+    return SolverCharacteristics.of(
+        RuleType.REFORMULATION,
+        RuleProperty.STRONGLY_CONSTRAINT_PRESERVING,
+        RuleProperty.OPTIMAL_SOLUTION_PRESERVING);
+  }
+
   @Override
   public String getDescription() {
     return "This solver builds SAT formulae to determine void features in a feature model. "
@@ -84,7 +95,7 @@ private Mono<Solution<String>> checkVoidFeatureModel(
           solution.setSolutionData(dimacsCnfSolution.isVoid()
               ? "The feature model is a void feature model. The configuration is never valid."
               : "The feature model has valid configurations, for example: \n"
-                + dimacsCnfSolution.toHumanReadableString());
+              + dimacsCnfSolution.toHumanReadableString());
           solution.complete();
 
           return solution;

src/main/java/edu/kit/provideq/toolbox/knapsack/solvers/PythonKnapsackSolver.java

@@ -2,6 +2,9 @@
 
 import edu.kit.provideq.toolbox.Solution;
 import edu.kit.provideq.toolbox.knapsack.KnapsackConfiguration;
+import edu.kit.provideq.toolbox.meta.RuleProperty;
+import edu.kit.provideq.toolbox.meta.RuleType;
+import edu.kit.provideq.toolbox.meta.SolverCharacteristics;
 import edu.kit.provideq.toolbox.meta.SolvingProperties;
 import edu.kit.provideq.toolbox.meta.SubRoutineResolver;
 import edu.kit.provideq.toolbox.process.ProcessRunner;
@@ -42,6 +45,11 @@ public String getDescription() {
         + "branch and search algorithm.";
   }
 
+  @Override
+  public SolverCharacteristics getCharacteristics() {
+    return SolverCharacteristics.of(RuleType.SOLVE, RuleProperty.EXACT, RuleProperty.VALID);
+  }
+
   @Override
   public Mono<Solution<String>> solve(
           String input,