Skip to content

Conversation

@tias
Copy link
Collaborator

@tias tias commented Oct 6, 2025

hexaly calls itself a global optimizer, we should do the same (so on README, new category: GO, and in docs reademe, global opt.)

Is that OK? e.g. @IgnaceBleukx

Rest looks fine.

@hbierlee do you want to use this PR to discuss how we should categorize Pindakaas?

It accepts PB-level input, so I would consider it a PB solver... And although it uses a SAT solver, could we call it a SAT solver?

@hbierlee
Copy link
Contributor

hbierlee commented Oct 6, 2025

Short answer: SAT category (meaning, SAT-based).

Refining my comment in #728, there is the question of modeling paradigm ('what input does it support?') and solving paradigm ('what core solver tech does it us'?). If we're being precise, neither question is actually straightforward to answer.

For us, I think the most sensible way to do this categorization is to answer the solving paradigm question (for pindakaas, and for other solvers!). Quite clearly, Pindakaas is a SAT-based solver, since SAT solvers are its core, so it should go in the SAT category (along with PySAT). Note: Pindakaas is not a SAT-solver, the category should only say it's SAT-based (with SAT solvers at its core).

Using the modeling paradigm could definitely also make sense (especially if we're trying to map out the waterfall), but it is murkier for many solvers. (e.g. gurobi acceps non-linear constraints, pindakaas accepts Boolean logic whereas traditional PB solver do not..). Plus, I think that the modeling paradigm matters less to the users of CPMpy, since this is what CPMpy abstracts away.

@tias
Copy link
Collaborator Author

tias commented Oct 7, 2025

Yes, I see.

So if I look at it, it seems that the README.md talks about 'solving paradigms', so the modeling input they accept (e.g. Pindakaas is for PB solving)
While the docs/index is about the technology underneath the solver, where pindakaas is using sat solvers underneath

Updated. Can you check the install information in the docs/index? I think it is no longer local install

@tias
Copy link
Collaborator Author

tias commented Oct 7, 2025

@IgnaceBleukx I also updated the top of hexaly's file. THey don't like being called a local solver anymore, in general we should use a similar description tagline as that the solver uses on their own website, which I've adapted now. ALso slight tweak to install info, explicit on binary install.

@IgnaceBleukx
Copy link
Collaborator

Ok for hexaly changes for me!

@hbierlee
Copy link
Contributor

hbierlee commented Oct 8, 2025

Updated. Can you check the install information in the docs/index? I think it is no longer local install

Yes, it's just pip install pindakaas, and it should have the ISAT (incremental SAT) capability.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants