How can I express scheduling problems in minisat?

Question

Minisat is a constraint programming/satisfaction tool, there is a version of Minisat which works here in the browser http://www.msoos.org/2013/09/minisat-in-your-browser/

How can I express a scheduling problem with Minisat? Is there a higher level language which compiles to Minisat which would let me express it?

I mean for solving problems like exam timetabling. http://docs.jboss.org/drools/release/6.1.0.Final/optaplanner-docs/html_single/#examination

enter image description here

score 7 · Accepted Answer · answered Dec 17 '14 at 18:45

7

Another high level modeling language is Picat (http://picat-lang.org/), which have an option to solve/2 to convert to CNF when using the sat module, e.g. "solve([dump], Vars)". The syntax when using the sat module - as well as for the cp and mip modules - is similar to standard CLP syntax.

For some Picat examples, see my Picat page: http://hakank.org/picat/ .

answered Dec 17 '14 at 18:45

hakank

6,629
1
17
27

2

I'm learning minizinc, and afaik your site it the best resource (as well as your answers here on SO)... alas, it's unresponsive by some days... Anyway, your [github repo](https://github.com/hakank) is still available. Thanks – CapelliC Jan 22 '15 at 08:41
@CapelliC: Thanks for your kind words. My site http://hakank.org/ is down right now, but I do everything I can to fix it as soon as possible. Great that you found the GitHub repo. – hakank Jan 22 '15 at 16:54

score 4 · Answer 2 · edited Apr 13 '17 at 12:19

SAT solvers like Minisat or Cryptominisat typically read a clause set of logical OR expressions in Conjunctive Normal Form (CNF). It takes an encoding step to translate your problem into this CNF format.

Circuit SAT Solvers process a nested Boolean expression rather than a CNF. But it appears that this type of solvers is nowadays outperformed by the CNF SAT Solvers.

Constraint programming solvers like Minizinc use a high level language which is easier to write and to comprehend. Depending on the features being used, Minizinc can translate its input language into a CNF/DIMACS format suitable for a SAT solver.

Peter Stuckey's paper "There are no CNF Problems" explains the idea. His slides also contain some insights on scheduling.

Have a look at Minizinc examples for scheduling written by Hakan Kjellerstrand.

Emmanuel Hebrard's Scheduling and SAT is an extensive treatment of the topic.

score 0 · Answer 3 · edited May 23 '17 at 12:02

I worked on this project few months ago.

It was really interesting to do.

To use miniSAT (or any other SAT solvers), you will have to reduce the Scheduling Problem to a SAT problem.

I can recommand you this question that I asked in 3 parts.

Class Scheduling to Boolean satisfiability [Polynomial-time reduction]

Class Scheduling to Boolean satisfiability [Polynomial-time reduction] part 2

Class Scheduling to Boolean satisfiability [Polynomial-time reduction] Final Part

And you will basically see, step by step, how to transform the Scheduling Problem to a SAT problem that MiniSAT can read and solve :).

Thanks again to @amit who was a very big help in this project.

With this answer, you will be able to solve N rooms with T teachers, who are teaching S subjects to G different group of students :) which is I think, enough for 99% of Scheduling Problems.

How can I express scheduling problems in minisat?

3 Answers3