Decision procedures and SAT/SMT solvers

This repository contains solutions to various NAIL094 homework assignments.

Please, do not copy

---

Programming assignments - Build your own SAT solver, and related tasks

Root: CPP

1. Tseitin Encoding and DIMACS Format: formula2cnf
2. DPLL Algorithm: bin/main -a
3. Watched Literals: bin/main -w
4. CDCL: bin/main

Old (Haskell)

Root: Haskell

Remarkable for its brevity, not so much for its speed

1. Tseitin Encoding and DIMACS Format: cabal run formula2cnf
2. DPLL Algorithm: cabal run dpll

---

Programming assignments - Using a SAT solver

Root: sat-use

• N Queens Puzzle
• Backbones
• Testing Equivalence
• Cryptarithms
• Cryptarithms with SMT-LIB 2

---

Theoretical assignments

Root: lecture-hw

• hw1.pdf
• hw2.pdf
• hw3.pdf
• hw4.pdf
• hw5.pdf
• hw6.pdf
• hw7.pdf
• hw8.pdf
• hw9.pdf
• hw10.pdf