Skip to content

Optimization API and Resource Management Improvements Needed #476

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
shivammm21 opened this issue Apr 5, 2025 · 6 comments · May be fixed by #477
Open

Optimization API and Resource Management Improvements Needed #476

shivammm21 opened this issue Apr 5, 2025 · 6 comments · May be fixed by #477
Assignees
@shivammm21
Labels
Blocked by Solver Support solver does not yet support this feature OR there was not yet any public release of the solver enhancement

Comments

@shivammm21
Copy link
Contributor

Inconsistent Optimization Support Across Solvers

Description

The optimization API in JavaSMT has inconsistent implementation across different solvers, leading to unpredictable behavior when applications switch between solver backends. Currently, only Z3 and MathSAT5 (via OptiMathSAT) properly support optimization capabilities, while other solvers simply throw exceptions without providing alternative functionality.

Observed Issues

Evidence in Implementation Code:

Z3 provides full implementation:

// In Z3SolverContext.java
public OptimizationProverEnvironment newOptimizationProverEnvironment0(
    Set<ProverOptions> options) {
  Z3SolverContext.ExtraOptions extraOptions = new Z3SolverContext.ExtraOptions(config);
  return new Z3OptimizationProver(
      creator,
      logger,
      (Z3FormulaManager) getFormulaManager(),
      options,
      ImmutableMap.<String, Object>builder()
          .put(OPT_ENGINE_CONFIG_KEY, extraOptions.optimizationEngine)
          .put(OPT_PRIORITY_CONFIG_KEY, extraOptions.objectivePrioritizationMode)
          .build(),
      logfile,
      shutdownNotifier);
}

While other solvers throw exceptions:

// In YicesSolverContext.java
protected OptimizationProverEnvironment newOptimizationProverEnvironment0(
    Set<ProverOptions> options) {
  throw new UnsupportedOperationException("Yices does not support optimization");
}

// In SMTInterpolSolverContext.java
public OptimizationProverEnvironment newOptimizationProverEnvironment0(
    Set<ProverOptions> options) {
  throw new UnsupportedOperationException("SMTInterpol does not support optimization");
}

// In PrincessSolverContext.java
public OptimizationProverEnvironment newOptimizationProverEnvironment0(
    Set<ProverOptions> pOptions) {
  throw new UnsupportedOperationException("Princess does not support optimization");
}

Test Code Shows Special Handling:

Tests must skip optimization tests for most solvers:

// In OptimizationTest.java
@Before
public void skipUnsupportedSolvers() {
  requireOptimization();
}

// In SolverBasedTest0.java
protected final void requireOptimization() {
  try {
    context.newOptimizationProverEnvironment().close();
  } catch (UnsupportedOperationException e) {
    assume()
        .withMessage("Solver %s does not support optimization", solverToUse())
        .that(e)
        .isNull();
  }
}

Even between supported solvers, behavior differs:

// From OptimizationTest.java - MathSAT5 specific workaround
if (solverToUse() == Solvers.MATHSAT5) {
  // see https://github.com/sosy-lab/java-smt/issues/233
  assume()
      .withMessage("OptiMathSAT 1.7.2 has a bug with switching objectives")
      .that(context.getVersion())
      .doesNotContain("MathSAT5 version 1.7.2");
  assume()
      .withMessage("OptiMathSAT 1.7.3 has a bug with switching objectives")
      .that(context.getVersion())
      .doesNotContain("MathSAT5 version 1.7.3");
}

// Different precision handling between solvers
// OptiMathSAT5 has at least an epsilon of 1/1000000. It does not allow larger values.
assume()
    .withMessage("Solver %s does not support large epsilons", solverToUse())
    .that(solver)
    .isNotEqualTo(Solvers.MATHSAT5);

Impact

  • Applications using optimization features cannot easily switch between solvers
  • Code must handle UnsupportedOperationExceptions and provide fallbacks
  • Optimization functionality is effectively limited to Z3 in many cases
  • Testing is incomplete due to varying solver capabilities
@shivammm21
Copy link
Contributor Author

shivammm21 commented Apr 5, 2025 •
edited
Loading

I'd like to assign myself to work on fixing the inconsistent optimization support issue. Based on my analysis.

  1. I understand the core problem is that optimization is fully implemented only in Z3 and partially in MathSAT5, while other solvers throw UnsupportedOperationException.

  2. I have experience with the JavaSMT codebase and am familiar with the solver interfaces.

  3. My approach would be to:

    • Create a fallback optimization implementation for solvers without native support
    • Standardize error handling and documentation across all solvers
    • Add better test coverage for mixed solver environments

I can submit an initial PR within 5 days that addresses the core inconsistencies.

Please let me know if there are any specific aspects you'd like me to prioritize.

@kfriedberger
Copy link
Member

Thanks for your interest in tackling this issue! We really appreciate your initiative and willingness to dive into the inconsistent optimization support problem.

Optimization techniques can indeed be quite complex. Full support exists only in Z3, and a partial implementation in MathSAT5, while other solvers just do not have this feature. It’s worth noting that even MathSAT doesn’t include optimization in its main library - it's actually only available in its fork called OptiMathSAT, which is maybe inactive in development.

I would assume that the UnsupportedOperationException for an unsupported feature it thrown consistently across all solvers. If you see a way of improving this, feel free to provide a PR as quick-win for JavaSMT.
Additionally, you might want to deeply go into the problem of optimization techniques to come with a valid solver-independent fallback mechanism that can be used if there is missing native support in a solver.

Looking forward to seeing your contribution—thanks again for stepping up!

@shivammm21
Copy link
Contributor Author

Hi, I'd like to take on this issue. Please assign it to me.

I've already started researching the current state of optimization support in the various solvers integrated with JavaSMT, including how UnsupportedOperationException is being handled. I'm also looking into potential improvements and exploring ideas for a solver-independent fallback mechanism when native optimization support is missing.

It would be great if you could also add relevant labels such as enhancement or good first issue, if applicable.

Thanks for the helpful context and for encouraging community contributions. I am looking forward to working on this.

@kfriedberger kfriedberger added the Blocked by Solver Support solver does not yet support this feature OR there was not yet any public release of the solver label Apr 6, 2025
@kfriedberger
Copy link
Member

Please make sure that you really understand the problem of optimization support before starting your implementation. There are reasons why several solvers do not support this feature, and one reason might be the complexity of this task: Finding an optimum for a specific constraint in SMT is considered a "hard problem".

@shivammm21
Copy link
Contributor Author

Thank you for your feedback, @kfriedberger. I appreciate the caution about the complexity of optimization in SMT.

I understand optimization is inherently a "hard problem" in SMT, which explains why many solvers don't support it. My intention isn't to implement optimization algorithms from scratch for each solver, but rather to:

  1. Create better standardization of the existing optimization API
  2. Implement consistent error handling across solvers
  3. Potentially create a basic fallback for simpler optimization cases using iterative solving approaches

Before proceeding, I'd like to better understand the specific limitations of different solvers. Would it be helpful to start with a survey of the current state and documentation improvements, before proposing any implementation changes?

@kfriedberger
Copy link
Member

Your task list sounds reasonable.

  1. Create better standardization of the existing optimization API
  2. Implement consistent error handling across solvers

Please document the inconsistencies in the current API and error handling, e.g., is there more than just "unsupported" for now regarding the API of JavaSMT. Please consider to minimize API changes due to the requirement of backwards-compatibility. . Any reasonable pull request is appreciated.

  1. Potentially create a basic fallback for simpler optimization cases using iterative solving approaches

Feel free to provide a fallback if there is a general solution. Please note that JavaSMT as such is only considered a "simple wrapper library" and as such any fallback should also be maintainable with reasonable effort in the future. Even larger SMT solver dismiss features that are not required by a larger group of users or have higher development effort as expected. A prominent example for such a feature is Craig interpolation that was removed from Z3 some years ago.

shivammm21 added a commit to shivammm21/java-smt-sosylab that referenced this issue Apr 11, 2025
@shivammm21
Improve optimization API and add fallback implementation
7844741 
This commit addresses issue sosy-lab#476 by: 1. Creating a standardized optimization API with AbstractOptimizationProver 2. Adding a fallback implementation for solvers without native optimization support 3. Implementing version compatibility checks for MathSAT5 4. Adding comprehensive tests for optimization features 5. Improving error handling with SolverOptimizationException 6. Adding documentation for optimization features

The changes provide consistent optimization support across all solvers, with a graceful fallback for unsupported solvers. The implementation uses binary search to approximate optimization results for solvers without native support.
@shivammm21 shivammm21 linked a pull request Apr 11, 2025 that will close this issue
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@shivammm21 shivammm21

Labels
Blocked by Solver Support solver does not yet support this feature OR there was not yet any public release of the solver enhancement
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Improve optimization API and add fallback implementation shivammm21/java-smt-sosylab
3 participants
@kfriedberger @daniel-raffler @shivammm21