Allow JSON I/O for embedded applications
In order to lower the cost of using Sat4j in a mobile device, it would be nice to allow interacting with the solver using the JSON format.
It is not a problem to read Dimacs formatted input that way: the CNF would be a list of list of non null integers.
The answer would be either "true" associated with a model (list of satisfied literals) or "false" associated with the empty list. We probably also need to consider the case in which the solver cannot answer ("unknown").
It is not clear if offering a Dimacs interface in JSON really makes sense for the end user, or if the input should be a string based propositional variables and that the mapping should be managed by the solver.
Another issue is the represent cardinality constraints and pseudo boolean constraints.
Would {"literals": {1,-2,3,-4,5}, "op"="=", "degree":3} be ok to represent for instance x1 + \lnot x2 + x3 + \lnot x4 + x5 = 3 cardinality constraint?