Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States

Satisfiability (SAT) problems come up in a surprising number of situations in computer science, from optimization problems to type checking. Being able to identify when a problem can be reduced to an instance of SAT is a useful tool in a programmer’s and researcher’s toolbox. This allows the reuse of libraries and tools written for this class of problems.

In this tutorial participants will learn how to identify SAT problems and how to encode them using the ‘Ersatz Monad’, which is provided by the Haskell ersatz package. The ersatz package is not a SAT solver itself, but provides a DSL for expressing SAT problems and interfacing with external SAT solvers (such as MiniSat).

The concrete examples will be puzzles and games, allowing the attendees to learn how to spot SAT instances using simple and fun examples, without having to learn and internalize large, complex, examples (such as airline route rules). As we progress through the examples we will relate the puzzles to more ‘real-world’ problems that can be solved with the same methods.

While the tutorial will demonstrate these concepts in Haskell using ersatz, the knowledge is easily transferable to other libraries for encoding SAT instances.

Sat 29 Sep

Displayed time zone: Guadalajara, Mexico City, Monterrey change

09:00 - 12:00
T06: Getting Satisfaction out of Games: Learning to use SAT solvers through puzzles and gamesTutorials at Frisco
Chair(s): Jose Calderon Galois, Inc., Eric Mertens Galois, Inc.
09:00
3h
Other
T06: Getting Satisfaction out of Games: Learning to use SAT solvers through puzzles and games
Tutorials
Eric Mertens Galois, Inc., Jose Calderon Galois, Inc.