[Enhancement Proposal] Only one type of problem for Solve, Explain and MaxSAT

[Mystelven]

You have three structures Problem one in the packageexplain, one in the package maxsat and one in the package solver.

However, It seems that it could be convenient to first solve a problem and if the result is unsatisfiable, then find an explanation (MUS or just an unsatisfiable subset).

A simple (but inefficient) way is to do it as follows:

func Convert(problem *solver.Problem) (*explain.Problem, error) {

	reader := strings.NewReader(problem.CNF())
	return explain.ParseCNF(reader)
}

But having only one type of structure for both packages seems more convenient in my opinion.
Same principle with the problem structure for MaxSAT problem.

If you accept this "improvement", I will propose a PR for it.

Keep me informed @fdelorme

[fdelorme]

That's a very good idea! That kind of thing was on my TODO-list anyway.

There's one potential pitfal you must be aware: in the solver package, problems are simplified as soon as they are parsed (meaning the problem (a or b or c) and not a will be transmitted as b or c to the solver).

That's not something you want when searching for MUSes or for MAXSAT problems though, so there are probably a few things to modify here and there in the solver package.

I'm looking forward to seeing your PR!