Logic for Computer Scientists
(summer semester 2017-2018, moodle)
(summer semester 2017-2018, moodle)
Consistency is the playground of dull minds.
("Sapiens", Yuval Noah Harari)
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
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)
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))
cnfgen randkcnf 3 100 200 | z3 -in -dimacs
virtualenv-2 .venv
source .venv/bin/activate
pip install z3-solver jupyter numpy matplotlib
jupyter notebook
source .venv/bin/activate
jupyter notebook
coqide file.v
.Maps.v
(and generate Maps.vo
) type: coqc Maps.v
.)Add LoadPath "/path/")
.