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

Answer 1

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.

Answer 2

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

Answer 3

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.