Skip to content
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.

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

Introduce a simplified version of td3 with warrowing (see PR 1611) #1626

Open
wants to merge 3 commits into
base: master
Choose a base branch
from

Conversation

FelixKrayer
Copy link
Contributor

Copied from PR #1611 by @arkocal
The simplified warrowing solver

As to which solver we should keep as the simplified version, this one:

  1. Can be documented a little more for didactic purposes, but I find it to be very readable as is.
  2. We should find the paper most closely matching this solver.
  3. This one does not pass all tests due to narrowing.

I created this pullrequest so I can address comments and do changes.
Addressing comments by @sim642 :

  1. removed remove-wpoint option. Having this option is not necessary for this solver. However, I changed it to always remove wpoints, without checking the config, as this is the default setting in the config.
  2. solver data is no longer a record. There is no need for that
  3. moved query/side out. There is no real reason they were inside iterate, it was just the way it turned out after deleting
  4. TODO: decide if phases should be included. This solver does not have them, since the parallel solvers do not use them and it was created for comparison with those. However, for generalizing this solver I see the use of implementing the phases.

@michael-schwarz
Copy link
Member

@sim642 @arkocal: What is you take on phases or not?
I don't have a strong opinion here, but think we should move forward with merging this.

@arkocal
Copy link

arkocal commented Dec 19, 2024

I am fine with either variant, so I would have a light preference to just proceed and merge. @sim642 had the point that the basic example should have a termination guarantee, which is reasonable, just not a deal breaker for me as I find warrowing a little more intuitive than phases.

tldr: I would keep it as is, but have no strong preference, so Simmo please feel free to override this if you do.

@FelixKrayer FelixKrayer marked this pull request as ready for review December 19, 2024 12:34
src/solver/td_simplified.ml Show resolved Hide resolved
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants