By: Daniel Le Berre (leberre) Date: 2011-08-24 18:47 Subject: RE: Minimal Solution
Timothy,
I agree with you.
When it comes to use SAT in practice, there is much work to do to adapt current SAT technology to a particular problem, because those problems often do not come directly in CNF. The current facilities in Sat4j (GateTranslator and DependencyHelper) have been designed to help people at Eclipse to enter into such technology.
BTW, in Eclipse, we query the solver for the truth value of specific Java objects using the DependencyHelper, so we do not really care about all the additional variables created by the solver. It is completely hidden.
I do work mostly in constraint programming, in which a conjunction of constraints is the usual way to work. As such, Sat4j does not provide much to help the user when the input is not that way.
Do not hesitate to tell us if you have simple ideas to improve that, we will do our best to implement them (the complicated ideas are good for the PhD proposal :))
Start New Thread
