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

✨ Parallelize asnchronous calls to the SAT solver #269

Open
pehamTom opened this issue Aug 27, 2024 · 0 comments
Open

✨ Parallelize asnchronous calls to the SAT solver #269

pehamTom opened this issue Aug 27, 2024 · 0 comments
Assignees
Labels
feature New feature or request

Comments

@pehamTom
Copy link
Member

What's the problem this feature will solve?

The iterative_search_with_timeout method in the ft_stateprep module makes repeated calls to a function with a certain timeout and tries to iteratively increase a parameter until the method does not time out. This is used to quickly search for a parameter where a SAT solver can find a satisfying assignment.

To enforce the timeout, the function is started as a separate process and is killed upon exceeding the timeout limit. Many of these calls can be executed in parallel and once a satisfying assignment is found for one parameter all other processes can be killed. Technically one does not need to kill all processes for this. One can also terminate all calls that use a larger parameter (for satisfying assignments) or smaller parameter (for proofs of UNSAT).

Describe the solution you'd like

When calling iterative_search_with_timeout, the calls should be made concurrently. An n_threads parameter would also be useful in this case.

@pehamTom pehamTom self-assigned this Aug 27, 2024
@pehamTom pehamTom added the feature New feature or request label Aug 27, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature New feature or request
Projects
Status: In Progress
Development

No branches or pull requests

1 participant