Given a Weighted Partial Max SAT problem (WPM-SAT) - are there generally used algorithms or techniques to generate 'approximate' solutions, which are not necessarily optimal, but found faster than solving directly? The approximate solutions must satisfy the hard clauses.
I have a series of very large (millions of literals, billions of hard clauses, millions of soft clauses) WPM-SAT problems, that I would like to get an answer to. However, I do not want to wait days for the absolute optimal result. I would like a reasonable (possibly sub-optimal) answer in a shorter amount of time.
In my brief literature review, perhaps I am not searching with the right terms, I haven't found too many good results for specifically approximating weighted partial max SAT.
Some methods seem to solve the hard clauses separately and then use various schemes for selecting literals to make true/false. Based on various randomized 3/4 approximation stuff. I'm not too interested in setting the hard clauses just once, or even just a few times. I know that, at least in my problems, there are many, many different solutions to the hard clauses.
In terms of solving the WPM-SAT problem there is the Fu-Malik paper, where they proposed 2 SAT based solvers for PM-SAT:
- Diagnosis Based, which seems to originally create an UNSAT core and then sort of successively relax clauses to arrive at the final optimal result. - This does not seem aplicable because it goes 'backwards', starting unsatisfiable and then slowly becoming satisfied at the maximum.
- Encoding Based, where an efficient ranking type scheme is created and then through a binary search / linear scan the optimal is arrived at. - This seems very promising, is this normally how this approximation would be done - just stopping early in the linear scan, or stopping the binary search after only a few iterations?
Opposed to SAT based techniques there are also branch and bound based techniques to solving WPM-SAT problems. Where we generate some upper / lower bounds on a given partial solution, if the upper bound is lower than our best so far we don't need to bother looking at it. When we arrive at a full solution it's upper bound is possibly better than our best, and we could stop after a certain amount of time maybe.
The Question, (again)
I have some big WPM-SAT problems, I want a reasonable solution to them; fast not necessarily optimal.
- Should I modify/implement the encoding based Fu-Malik algorithm to exit early?
- Should I modify/implement the branch and bound based algorithm to exit early?
- Is there something else that I have not found? References / survey papers that I haven't found for this stuff? Anyone working on this?
Bonus question: If I have a reasonable heuristic already can I use that to seed the optimization to go faster? What if that heuristic does not satisfy the hard clauses?