6

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

SecretAgentMan
  • 1,895
  • 2
  • 13
  • 39
Stefano Gualandi
  • 1,750
  • 1
  • 13
  • 26
  • 1
    I guess Picat/PicatSAT (or all those other CSP to SAT converters: page 6) somewhat do this, although i never looked into those. I'm also not fully sure how to interpret the question as DIMACS CNF is the SAT-equivalent of LP/MPS files in MP to me: low-lvl instance-definitions. Both variants imho already passed the modelling layer (e.g. core decisions like cardinality-encoding in SAT; compact vs. non-compact encodings in MP) and some solvers even try to reconstruct now lost information again (e.g. cardinality constraints in SAT). – sascha Nov 07 '21 at 13:54
  • Thanks @sascha, I will look into the tutorial! Regarding the DIMACS CNF format, the question is related to the possibility of writing the encoding of an instance once and then reusing it easily with different SAT solvers: a fast way of comparing SAT solvers on instances of my interest. – Stefano Gualandi Nov 07 '21 at 15:00
  • A friend has suggested an interesting answer on another stack-site: How can I express scheduling problems in-MiniSat – Stefano Gualandi Nov 09 '21 at 16:23

2 Answers2

5

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).

hakank
  • 934
  • 6
  • 15
4

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.

Stefano Gualandi
  • 1,750
  • 1
  • 13
  • 26