The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
Lexico-Optimization does not work with ManyCore (parallel) solvers.
During the LION 9 challenge, two versions of Sat4j was used.
That challenge is about solving multi-objective boolean functions, in that case lexicographic one.
The pure resolution based one worked fine while the one using the parallel solver Both answered sub-optimal solutions.
The parallel solver has been used successfully for years on PB benchmarks.
The main issue with lexicographic optimization is that an UNSAT answer is not final contrariwise to the mono-objective optimization.
Initial investigation of the problem shows that the parallel solvers always answer UNSAT after a while.