Lògica a la Informàtica
Lab 5 / Lab 6

  • Pràctica 3: Codificació 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 solve the problem

Setting-up

To find a solution of a contraint satisfacion problem we:

  • define the variables of the problem
  • generate the clauses encoding the contraints at a high level
  • translate the clauses to DIMACS format
  • feed the clauses to a SAT solver (e.g. kissat)
  • reconstruct a human readable solution from the answer given by the SAT solver (for us kissat)

Useful predicates

?- help(between).

?- between(1,4,2).

?- between(1,4,X), write(X), nl, fail.

?- help(findall).

Informally findall(X,G,L) \approx L = \{X\mid G \text{ is true}\}. If you need the list without repetitions use sort/2 to eliminate the duplicates from L.

?- findall(X,(between(1,7,X),1 is X mod 2),L).

?- findall(Y,(between(1,7,X),1 is X mod 2,Y is X*X),L).

?- help(nth1).

?- nth1(2, [15,42,55,79], Elem).

?- nth1(2, [[4,2],[7,5]], Row), nth1(1, Row, Elem).

Similar to this is nth0/3.

Useful predicates from the helper library

L is a list of literals \ell_1,\dots,\ell_n

Predicate Generates a set of clauses equivalent to
writeOneClause(L) \ell_1\lor \dots\lor \ell_n
exactly(K,L) \ell_1+\cdots+\ell_n=K
atMost(K,L) \ell_1+\cdots+\ell_n\leq K
atLeast(K,L) \ell_1+\cdots+\ell_n\geq K
expressOr(V,L) V\leftrightarrow \ell_1\lor \cdots\lor \ell_n
expressAnd(V,L) V\leftrightarrow \ell_1\land \cdots\land \ell_n

Caution

The behaviour is different when symbolicOutput(1) (the predicates above generate high-level encodings of the logic restrictions) or when symbolicOutput(0) (the predicates give CNF formulas written in the DIMACS format).

Exercises

  • teams.pl (let’s look at it together)
  • events.pl
  • newBusCompany.pl

Do them in this order.