I'm happy to announce that the Pulse team at Genuitec has signed a contract with the SAT4J team to fund research to provide better explanation support in p2. Yes you heard it right. Genuitec pays the SAT4J team (a research team from the CNRS / University of Lens - France) and the work is benefiting p2!
I'm really excited about that, not only because this will improve p2, but also because Daniel and Anne from the SAT4J team have been working like nuts in the shade for nothing more than... well nothing, and it is a nice recognition of their hard work and commitment.
For the technical part, the difficult aspect of this work is to extract from a set of boolean expressions a minimal set of constraints that make the problem unsatisfiable (aka UNSAT core) and then map that back to user input.
Congrats to the SAT4J team and thank you to Genuitec!