Does a modeling language that generates SAT instances exist?

Question

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.

Answer 1

As @sascha mentions, Picat has the option to save a SAT model to CNF, using the dump(file.cnf) option (or just dump to print the CNF to stdout). It's described a little more in the Picat Guide section 12.6.3 "Solving Options for sat" (See http://picat-lang.org/download/picat_guide.pdf)

Here's a small example how to use this for a Picat model:

import sat.

main => queens(8,Q),  

queens(N, Q) =>
    Q=new_list(N),
    Q :: 1..N,
    all_different(Q),
    all_different($[Q[I]-I : I in 1..N]),
    all_different($[Q[I]+I : I in 1..N]),

    solve($[dump("sat_dump.cnf"),ff],Q).

The output file sat_dump.cnf then contains the CNF for this model. Note that when using the dump/1 option, the model don't solves the problem, it just creates the CNF file.

With a little tweaking one can use this to generate CNF for a MiniZinc model using the PicatSAT program, see https://github.com/nfzhou/fzn_picat/ . The fix is to add the option dump(file.cnf) to the options (Option = ... ) in the file fzn_picat_sat.pi . Note that with this simple fix, after the program generated the CNF file, there will probably be an error when the program tries to print out the solution (since there is no created solution that can be printed).

Answer 2

While the @hakank answer is pretty nice and useful, I found exactly what I was looking for:

PySAT, SAT Technology in Python

With PySAT, via the PyPBLIB, it is possible to write high-level pseudo-boolean formulas (e.g., at-least-k,at-most-k,at-exactly-k, $\sum_{i \in I} a_i x_i \leq b$, ...), and then to get the global CNF formula, which can be dumped in a standard DIMACS SAT file.

Moreover, you can easily switch from one SAT solver to another. The list of SAT solvers available via PySAT is in the online documentation.

What is very nice, is that you can experiment with the different encoding of the same constraint, like binary decision diagrams (BDD), sequential weight counters, sorting networks, adder networks, ... you can find even more encoding in the documentation.

And (YES!) the fact that is accessible via Python is a plus.