Lògica a la Informàtica
Lab 7 / Lab 8

  • Pràctica 4: Optimizació en SAT
    • given a constraint satisfaction problem
    • encode it as a CNF using prolog (and a given library as helper)
    • use a SAT solver (kissat) to optimize solutions to the problem

Setting-up

  • download all the files at Pràctica 4: Optimizació en SAT including the Makefile

  • we use minColoring.pl as an example

  • before looking at the code let’s understand the problem

The chromatic number \chi(G)

Given G=(V,E) an undirected graph,
a function c : V\to \{1,\dots, k\} is a proper coloring (with k colors) of G if for every edge \{u,v\}\in E, c(u)\neq c(v). In other words, adjacent vertices must have assigned different colors (among the k available).

The chromatic number of G (\chi(G)) is the minimum number of colors needed to color G properly.

  • What do we know a priori on \chi(G)?
  • How can we write a CNF that is satisfiable iff G is k-colorable?
  • How can we find \chi(G) using a SAT-solver as an oracle?

Exercises

  • minColoring.pl (let’s look at it together)
  • supermarket.pl
  • towers.pl