Problem Solving

Next Tutoring Sessions

On demand...

Slides

Every week, I'll update the slides with the last version.

Previous Years Exams

  1. Course 2022/23
    1. First Partial
    2. Second Partial
    3. Retake First Partial
    4. Retake Second Partial
  2. Course 2023/24
    1. First Partial
    2. Second Partial
    3. Retake First Partial
    4. Retake Second Partial
    5. Second Retake Second Partial

Recorded classes

  1. Nov. 25, 2022Restarts and Clause deletion
  2. Dec 2, 2022Introduction to Cardinality Constraints

Solutions to some proposed exercices

  1. Exercice 15
  2. Exercice 17
  3. Exercice 18

Install a SAT solver in your laptop

For the practices, you will need a SAT solver. You can get cadical executing: 

git clone https://github.com/arminbiere/cadical.git
cd cadical
./configure
make
Save into test.cnf this example of CNF formula written in DIMACS format: 
c This is an example
c with 4 vars and 6 clauses
p cnf 4 6
120
-1 3 4 0
-3 -4 0
-2 3 -4 0
-3 4 0
1 -2 3 4 0
After executing: 
./built/cadical test.cnf
You should get something like: 
c --- [ banner ] -------------------------------------------------------------
c 
c CaDiCaL Radically Simplified CDCL SAT Solver
c Copyright (c) 2016-2021 A. Biere, M. Fleury, N. Froleyks
c 
c Version 1.5.2 a5f15211db36c3956764e18194dd5bd63bf3b5e6
c g++ (Ubuntu 7.5.0-3ubuntu1~18.04) 7.5.0 -Wall -Wextra -O3 -DNDEBUG
c Wed Sep 14 15:23:07 CEST 2022 Linux XPS-15 4.15.0-192-generic x86_64
c 
c --- [ parsing input ] ------------------------------------------------------
c 
c reading DIMACS file from 'test.cnf'
c opening file to read 'test.cnf'
c found 'p cnf 4 6' header
c parsed 6 clauses in 0.00 seconds process time
c closing file 'test.cnf'
c after reading 110 bytes 0.0 MB
c 
c --- [ options ] ------------------------------------------------------------
c 
c all options are set to their default value
c 
c --- [ solving ] ------------------------------------------------------------
c 
c time measured in process time since initialization
c 
c  seconds  reductions  redundant irredundant
c         MB    restarts       trail    variables
c          level   conflicts       glue     remaining
c 
c *  0.00  2  0 0   0    0    0  0% 0    6   4 100%
c l  0.00  2  0 0   0    0    0  0% 0    6   4 100%
c 1  0.00  2  0 0   0    0    0  0% 0    6   4 100%
c 
c --- [ result ] -------------------------------------------------------------
c 
s SATISFIABLE
v 1 -2 -3 4 0
c 
c --- [ run-time profiling ] -------------------------------------------------
c 
c process time taken by individual solving procedures
c (percentage relative to process time for solving)
c 
c         0.00   26.46% parse
c         0.00   24.76% search
c         0.00   23.30% lucky
c         0.00    0.00% simplify
c   =================================
c         0.00   37.39% solve
c 
c last line shows process time for solving
c (percentage relative to total process time)
c 
c --- [ statistics ] ---------------------------------------------------------
c 
c lucky:                         1       100.00 %  of tried
c minimized:                     0         0.00 %  learned literals
c shrunken:                      0         0.00 %  learned literals
c minishrunken:                  0         0.00 %  learned literals
c propagations:                  0         0.00 M  per second
c 
c seconds are measured in process time for solving
c 
c --- [ resources ] ----------------------------------------------------------
c 
c total process time since initialization:         0.00    seconds
c total real time since initialization:            0.00    seconds
c maximum resident set size of process:            2.55    MB
c 
c --- [ shutting down ] ------------------------------------------------------
c 
c exit 10
Notice the lines starting with "v" that describe the model got by the solver.

Sudoku

All of you have to implement a sudoku solver based on a SAT solver.

Save this Example of sudoku as example.suk. You can write a program sudoku1.py in python that using example.suk as imput, generates a formula example.cnf in DIMACS format. Then using a SAT solver, find a model of the formula. Implement another program sudoku2.py that, takeing the output of the SAT solver example.out, generates a solution of the sudoku: 

python sudoku1.py <example.suk >example.cnf
./built/cadical example.cnf >example.out
python sudoku2.py <example.out