Problem Solving

Next Tutoring Sessions

On demand...

Slides

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

Recorded classes

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

Solutions to some proposed exercices

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