Nowadays, we enjoy the expressivity of modern modeling languages. However, does it exists a modeling language that takes in input a declarative problem definition (like AMPL or MiniZinc, or similar), and produces as output a SAT instance, for instance in the DIMACS format, which can be later solved with any SAT solver which support a standard format?
This is for achieving something similar to what we do using the .mps or .lp format for ILP problems.
NOTE: This question is related to this other (but it is not exactly the same): Extracting CNF representation of my problem from SAT solver
Thanks.