Lab1 - SAT (1)

• Example DIMACS format

c comment lines start with character 'c'

c the next line says that this SAT instance has 3 variables and 2 clauses

p cnf 3 2

c the first clause contains "x_1" and "not x_3"

c "0" is a terminator that allows clauses to span multiple lines

1 -3 0

c the second clause contains "x_2", "x_3", and "not x_1"

2 3 -1 0

This can be fed to z3 as

cat example.cnf | z3 -in -dimacs

z3 -dimacs example.cnf

• How to verify a tautology?
• Pigeonhole, ordering formulas: Use cnfgen to generate sat instances for pigeonhole and ordering, and find for which parameters do these instances get hard.

cnfgen php 10 9 | z3 -dimacs -in (unsat; ends in reasonable time)

cnfgen php 11 10 | z3 -dimacs -in (unsat; does not)

cnfgen php 100 100 | z3 -dimacs -in (sat; takes way longer to generate the input than solving it)

cnfgen op 24 | z3 -in -dimacs (unsat; terminates but slow)

• Pebbling formulas: Write a python program that generates instances for the pebbling problem for the n*n grid.
• Counting assignments: Write a python program that counts all satisfying assignments. Hint: For each found assignment, add its negation as a new clause. Z3 tutorial.

python2 -m virtualenv env0

source ./env0/bin/activate

pip install z3-solver

# simple example of using Z3 from Python

from z3 import *

p = Bool('p')

q = Bool('q')

r = Bool('r')

solve(Or(p, q, r, q), Or(Not(p), q), Or(p, Not(q), r))

• Random 3-CNF: Consider random 3-CNF formulas with n = 100 variables and m clauses. Find empirically for which ratio m/n the random formula is unsatisfiable with high probability (for every m sample 100 times).

cnfgen randkcnf 3 100 200 | z3 -in -dimacs

LAB2 - SAT (2)

• Z3 python tutorial.
• Jupyter notebook.
• Instructions to install and run jupyter:

virtualenv-2 .venv

source .venv/bin/activate

pip install z3-solver jupyter numpy matplotlib

jupyter notebook

LAB5 - COQ (1)

• Webpage of the tool.
• To open a coq file type: coqide file.v.
• Coq source file for this lab.
• Additional material.

LAB6 - COQ (2)

• Coq source file for this lab: Lists, induction, inversion, induction on evidence.

LAB7 - COQ (3)

• (To compile Maps.v (and generate Maps.vo) type: coqc Maps.v.)
• (To add a directory to the path: Add LoadPath "/path/").
• Suggestion: Exercises 1*, 2*, 7, 8 in the Coq source file.