Problem Solving

Next Tutoring Sessions

Slides

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
3. Course 2024/25
   1. Second Partial Proposed solution

   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