Lab 01


  1. Download a SAT solver. For instance lingeling, minisat, or  cryptominisat.
  2. Encode as SAT the N-queens problem in the CNF, using the DIMACS format. See example output for  6-queens.cnf 
  3. Use a solution converter to visual representation, e.g. lingeling 6-queens.cnf | ./model2board.py 6. The converter assumes that square (1,1) is represented by variable 1, square (2,1) by variable 2, etc.
  4. Instead of a SAT solver, you can also use a model enumerator.

Lab 02


Encode into CNF the k-graph coloring problem, where k is a parameter of the encoding. Resources to facilitate the exercise:.
  • See example graphs: triangle and rectangle.
  • Erdos-Rényi graph generator
  • Model to graph script. On command line use as follows:  ./your_formula_generator 3 triangle.txt | lingeling | python2 model2graph.py 3 triangle.txt, assuming that your_formula_generator prints on standard output.
  • Once you've used model2graph.py successfully, you can use the following online graphviz visualization.
  • Example how to read a graph in Java
  • The statement "Node N is colored by color C", when considering K colors is encoded as the variable number N*K+C+1, where both colors and nodes are indexed from 0
Advanced: encode the K-clique problem, i.e. does the input graph has a clique of size K. Hint use for instance Seq. counter encoding described in Sinz 05.

Lab 03


Install a MaxSAT solver. Various options but the input forma is uniform. 

Specification for "Weighted Partial Max-SAT input format",  here; sample file.
Problems: You can use this script to show vertices  selected by a SAT model. A vertex n is mapped to the variable n+1. Graphs are represented as in the previous lab.

Optional

  • Place a maximal number of knights on a chessboard so that no knight attacks another.
  • Place a minimal number of knights on a chessboard so that each square of the board is attacked.


Lab 04

1. Install a Pseudo-Boolean (PB) solver (e.g. bsolo, wbo, scip, minisatp).
  • wbo:         http://sat.inesc-id.pt/~vmm/wbo.gz        (Linux - 64 bits)
  • bsolo:       http://sat.inesc-id.pt/~vmm/bsolo.gz      (Linux - 32 bits)
  • sat4jPseudo: http://www.sat4j.org/products.php       (Java)
  • SCIP:        http://scip.zib.de/#download              (All platforms: Windows, MacOS, Linux)
  • minisatp:    http://sat.inesc-id.pt/?vmm/minisatp.gz   (Linux - 64 bits)

Use the opb format available at:http://www.cril.univ-artois.fr/PB11/format.pdf

2. Consider the minimum vertex cover problem (lecture 06, slide 14).a) Encode the problem using PB constraints.b) Run the PB solver to get an optimal solution assignment.

3. Consider the software upgradability problem (lecture 06, page 21).a) Encode the problem using pseudo-Boolean constraints.b) Run the PB solver to get an optimal solution assignment.c) Consider installation costs to each package and change the PB instance accordingly.d) Run the PB solver to get an optimal solution assignment.
4. Consider a 4x4 sudoku puzzle where you have the following placements:(1, 2) -> 1(1, 3) -> 3(2, 1) -> 2(3, 4) -> 3(4, 2) -> 2(4, 3) -> 1
where each line is of the format (line, column) -> value

a) Encode it using PB constraints.b) Run a PB solver to get a solution assignment.

5. Have more fun and develop your Sudoku solver for any K x K puzzle.