Propositional logic and simple predicate assignments powerpoint (0)

Propositional logic and  simple  
predicate  assignments
Home assignment 2 : Margus Martsepp
Advanced  Course  of Applied Logics ( ITV0081 )
Overview
Setting up
• zChaff
• glucose
• BerkMin
Collecting problemset
• trivial problem
•  benchmark
Using problemset
zChaff
Installing compiler
$ sudo apt-get install build - essential
zchaff {download, unarhive, make executable}
$ wget  http://www.princeton.edu/~chaff/zchaff/zchaff.2008.10.12.zip
$ unzip zchaff.2008.10.12.zip
$ cd zchaff
/zchaff$ make
glucose
(Re)installing zlib
$ sudo apt-get install --reinstall zlibc zlib1g zlib1g-dev
glucose {download, unarhive, make executable}
$ wget  https://www.lri.fr/~simon/downloads/glucose2.1.tgz
$ tar -xvzf glucose2.1.tgz
$ cd glucose_2.1
/glucose_2.1$ sh build.sh
Note: glucose contains SatElite Preprocessing
BerkMin
installing shared libs
$ sudo apt-get install libstdc++6-4.5-dbg
berkmin {download, unarhive, set as executable}
$ wget  http://eigold.tripod.com/BerkMin561-linux.gz
$ gunzip BerkMin561- linux .gz
$ chmod +x BerkMin561-linux
BerkMin
Collecting problemset
cnf problems {download, unarhive}
$ mkdir problemset
$ cd problemset
/problemset$ wget  http://people.sc.fsu.edu/~jburkardt/data/cnf/
aim-100-1_6-no-1.cnf
/problemset$ wget  http://www.satlib.org/Benchmarks/SAT/New/
Competition -03/distrib-shuffled.tar.bz2
/problemset$ tar -xjvf distrib-shuffled.tar.bz2
zChaff : trivial problem
glucose : trivial problem
glucose : trivial problem
Benchmark : SAT
Total  Run Time
problemset/handmade/gomes/qwh/qwh.35.405.shuffled-
as.sat03- 1651 .cnf.gz 
• zChaff  : 32.586 s
• glucose  : 30.8779 s
problemset/ industrial / maris /CNF/hanoi5.shuffled-as.sat03-
400.cnf
• zChaff  : +100 s
• glucose  : 23.1614 s
problemset/handmade/markstrom/SATISFIABLE/mm-3x1-9-9-
sb.1.shuffled-as.sat03-1495.cnf
• zChaff  : 5.40834 s
• glucose  : 0.144009 s
Benchmark : UNSAT
Total Run Time
problemset/industrial/kukula/addm_bench/am_5_5.shuffled-
as.sat03-361.cnf.gz 
• zChaff  : 26.9017 s
• glucose  : 4.65229 s
problemset/industrial/maris/CNF/hanoi5u.shuffled-as.sat03-
401.cnf.gz
• zChaff  : +100 s
• glucose  : 10.6767 s
problemset/handmade/markstrom/UNSATISFIABLE/mm-2x2-6-6-
sb.1.shuffled-as.sat03-1500.cnf.g
• zChaff  : 8.84455 s
• glucose  : 4.50828 s

Document Outline

• Slide 1
• Overview
• zChaff
• glucose
• BerkMin
• BerkMin
• Collecting problemset
• zChaff : trivial problem
• glucose : trivial problem
• glucose : trivial problem
• Benchmark : SAT
• Benchmark : UNSAT