Optimising generated rules for SAT solving (5/12 are duplicates)
Hans Petter Selasky
hps at selasky.org
Thu Nov 24 13:05:44 UTC 2016
On 11/24/16 13:13, Vsevolod Stakhov wrote:
> On 23/11/2016 16:27, Ed Schouten wrote:
>> Hi Hans,
>>
>> 2016-11-23 15:27 GMT+01:00 Hans Petter Selasky <hps at selasky.org>:
>>> I've made a patch to hopefully optimise SAT solving in our pkg utility.
>>
>> Nice! Do you by any chance have any numbers that show the performance
>> improvements made by this change? Assuming that the SAT solver of
>> pkg(1) uses an algorithm similar to DPLL[1], a change like this would
>> affect performance linearly. My guess is therefore that the running
>> time is reduced by approximately 5/12. Is this correct?
>
> There won't be any improvement if you just remove duplicates from SAT
> formula. This situation is handled by picosat internally and even for
> naive DPLL there is no significant influence of duplicate KNF clauses:
> once you've assumed all vars in some clause, you automatically resolve
> all duplicates.
>
> Is there any real improvement of SAT solver speed with this patch? From
> my experiences, SAT solving is negligible in terms of CPU time comparing
> to other tasks performed by pkg.
Hi,
I added some code to measure the time for SAT solving. During my test
run I'm seeing values in the range 8-10ms for both versions, so I
consider that neglible. However, the unpatched version wants to
reinstall 185 packages while the non-patched version wants to reinstall
1 package. That has a huge time influential. I'm not that familar with
PKG that I can draw any conclusions from this.
# Test1:
echo "n" | /xxx/pkg/src/pkg-static upgrade --no-repo-update > b.txt
# Test2:
echo "n" | env PKG_NO_SORT=YES /xxx/pkg/src/pkg-static upgrade
--no-repo-update > a.txt
Please find the material attached including a debug version patch you
can play with.
--HPS
-------------- next part --------------
Checking for upgrades (748 candidates): .......... done
Processing candidates (748 candidates): . done
Skipped 3702 identical rules
Reiterate
SAT solving took 0s and 7370 usecs
The following 52 package(s) will be affected (of 0 checked):
Installed packages to be UPGRADED:
xapian-core: 1.2.23,1 -> 1.2.24,1
webp: 0.5.0 -> 0.5.1_1
webkit2-gtk3: 2.8.5_6 -> 2.8.5_7
webkit-gtk2: 2.4.11_4 -> 2.4.11_5
vlc: 2.2.4_3,4 -> 2.2.4_4,4
trousers: 0.3.13_1 -> 0.3.14
tiff: 4.0.6_2 -> 4.0.7
thunderbird: 45.4.0_2 -> 45.5.0_1
sqlite3: 3.15.1 -> 3.15.1_1
spidermonkey170: 17.0.0_2 -> 17.0.0_3
soundtouch: 1.9.2 -> 1.9.2_1
raptor2: 2.0.15_4 -> 2.0.15_5
qt5-core: 5.6.2 -> 5.6.2_1
qt4-corelib: 4.8.7_5 -> 4.8.7_6
polkit: 0.113_1 -> 0.113_2
pciids: 20161029 -> 20161119
openimageio: 1.6.12_2 -> 1.6.12_3
openblas: 0.2.18_1,1 -> 0.2.18_2,1
openal-soft: 1.17.2 -> 1.17.2_1
libx264: 0.148.2708 -> 0.148.2708_1
libvpx: 1.6.0 -> 1.6.0_1
libvisio01: 0.1.5_3 -> 0.1.5_4
libreoffice: 5.2.3_2 -> 5.2.3_3
libpci: 3.5.1 -> 3.5.2
libmspub01: 0.1.2_4 -> 0.1.2_5
libfreehand: 0.1.1_3 -> 0.1.1_4
libe-book: 0.1.2_5 -> 0.1.2_6
libcdr01: 0.1.3_1 -> 0.1.3_2
lcms2: 2.7_2 -> 2.8
inkscape: 0.91_8 -> 0.91_9
icu: 57.1,1 -> 58.1,1
harfbuzz: 1.3.3 -> 1.3.3_1
gstreamer1-plugins: 1.8.0 -> 1.8.0_1
gstreamer-plugins: 0.10.36_6,3 -> 0.10.36_7,3
gstreamer: 0.10.36_4 -> 0.10.36_5
gnupg: 2.1.15 -> 2.1.16
glib: 2.46.2_3 -> 2.46.2_4
gcc: 4.8.5_2 -> 4.9.4
firefox: 50.0_2,1 -> 50.0_4,1
firebird25-client: 2.5.6_1 -> 2.5.6_2
ffmpeg: 2.8.8_5,1 -> 2.8.8_8,1
dejavu: 2.35 -> 2.37
chromium: 52.0.2743.116_2 -> 52.0.2743.116_4
boost-libs: 1.55.0_13 -> 1.55.0_14
blender: 2.77a -> 2.77a_1
belle-sip: 1.5.0 -> 1.5.0_1
bash: 4.4 -> 4.4.5
argyllcms: 1.7.0_1 -> 1.7.0_2
OpenEXR: 2.2.0_5 -> 2.2.0_6
ImageMagick: 6.9.5.10,1 -> 6.9.5.10_1,1
GraphicsMagick: 1.3.24,1 -> 1.3.24_1,1
Installed packages to be REINSTALLED:
baresip-0.4.19 (options changed)
Number of packages to be upgraded: 51
Number of packages to be reinstalled: 1
The process will require 19 MiB more space.
446 MiB to be downloaded.
Proceed with this action? [y/N]:
-------------- next part --------------
Checking for upgrades (748 candidates): .......... done
Processing candidates (748 candidates): . done
Reiterate
SAT solving took 0s and 5790 usecs
The following 236 package(s) will be affected (of 0 checked):
Installed packages to be UPGRADED:
xapian-core: 1.2.23,1 -> 1.2.24,1
webp: 0.5.0 -> 0.5.1_1
webkit2-gtk3: 2.8.5_6 -> 2.8.5_7
webkit-gtk2: 2.4.11_4 -> 2.4.11_5
vlc: 2.2.4_3,4 -> 2.2.4_4,4
trousers: 0.3.13_1 -> 0.3.14
tiff: 4.0.6_2 -> 4.0.7
thunderbird: 45.4.0_2 -> 45.5.0_1
sqlite3: 3.15.1 -> 3.15.1_1
spidermonkey170: 17.0.0_2 -> 17.0.0_3
soundtouch: 1.9.2 -> 1.9.2_1
raptor2: 2.0.15_4 -> 2.0.15_5
qt5-core: 5.6.2 -> 5.6.2_1
qt4-corelib: 4.8.7_5 -> 4.8.7_6
polkit: 0.113_1 -> 0.113_2
pciids: 20161029 -> 20161119
openimageio: 1.6.12_2 -> 1.6.12_3
openblas: 0.2.18_1,1 -> 0.2.18_2,1
openal-soft: 1.17.2 -> 1.17.2_1
libx264: 0.148.2708 -> 0.148.2708_1
libvpx: 1.6.0 -> 1.6.0_1
libvisio01: 0.1.5_3 -> 0.1.5_4
libreoffice: 5.2.3_2 -> 5.2.3_3
libpci: 3.5.1 -> 3.5.2
libmspub01: 0.1.2_4 -> 0.1.2_5
libfreehand: 0.1.1_3 -> 0.1.1_4
libe-book: 0.1.2_5 -> 0.1.2_6
libcdr01: 0.1.3_1 -> 0.1.3_2
lcms2: 2.7_2 -> 2.8
inkscape: 0.91_8 -> 0.91_9
icu: 57.1,1 -> 58.1,1
harfbuzz: 1.3.3 -> 1.3.3_1
gstreamer1-plugins: 1.8.0 -> 1.8.0_1
gstreamer-plugins: 0.10.36_6,3 -> 0.10.36_7,3
gstreamer: 0.10.36_4 -> 0.10.36_5
gnupg: 2.1.15 -> 2.1.16
glib: 2.46.2_3 -> 2.46.2_4
gcc: 4.8.5_2 -> 4.9.4
firefox: 50.0_2,1 -> 50.0_4,1
firebird25-client: 2.5.6_1 -> 2.5.6_2
ffmpeg: 2.8.8_5,1 -> 2.8.8_8,1
dejavu: 2.35 -> 2.37
chromium: 52.0.2743.116_2 -> 52.0.2743.116_4
boost-libs: 1.55.0_13 -> 1.55.0_14
blender: 2.77a -> 2.77a_1
belle-sip: 1.5.0 -> 1.5.0_1
bash: 4.4 -> 4.4.5
argyllcms: 1.7.0_1 -> 1.7.0_2
OpenEXR: 2.2.0_5 -> 2.2.0_6
ImageMagick: 6.9.5.10,1 -> 6.9.5.10_1,1
GraphicsMagick: 1.3.24,1 -> 1.3.24_1,1
Installed packages to be REINSTALLED:
yaml-cpp03-0.3.0
yajl-2.1.0
xvid-1.3.4,1
xcb-util-renderutil-0.3.9_1
xcb-util-keysyms-0.4.0_1
xcb-util-0.4.0_1,1
twolame-0.3.13_4
tpm-emulator-0.7.4_1
tinyxml-2.6.2_1
taglib-1.10
startup-notification-0.12_4
speexdsp-1.2.r3_1
speex-1.2.r2,1
speech-dispatcher-0.8.3_1
spandsp-0.0.6
snappy-1.1.3
serf-1.3.9_1
schroedinger-1.0.11_4
redland-1.0.17_4
readline-6.3.8
re2-20151101
rasqal-0.9.33
qt5-x11extras-5.6.2
qt5-widgets-5.6.2
python35-3.5.2
python27-2.7.12
popt-1.16_1
poppler-glib-0.46.0
poppler-0.46.0_2
pixman-0.34.0
perl5-5.24.1.r4
pcre-8.39
pangomm-2.36.0
pango-1.38.0_1
p11-kit-0.23.2
orc-0.4.25
opus-1.1.3
opensubdiv-3.0.5_2
openldap-client-2.4.44
openjpeg15-1.5.2_1
openjpeg-2.1.2_1
opencv2-core-2.4.13.1_1
opencolorio-1.0.9
opencollada-1.6.25
nss-3.27.1_1
nspr-4.13.1
npth-1.2
nettle-3.2
mythes-1.2.4
mpfr-3.1.5
mpc-1.0.3
lua52-5.2.4
libxslt-1.1.29
libxml2-2.9.4
libxcb-1.12
libwps-0.4.4
libwpg03-0.3.1
libwpd010-0.10.1
libwmf-0.2.8.4_15
libvorbis-1.3.5,3
libvdpau-1.1.1
libva-1.7.2
libv4l-1.6.3_2
libtheora-1.1.1_6
libtasn1-4.9
libsoup-2.52.2
libsndfile-1.0.27
libsigc++-2.4.1
libsecret-0.18.4
libsamplerate-0.1.9
librsvg2-2.40.16
librevenge-0.0.4_1
libpthread-stubs-0.3_6
libpciaccess-0.13.4
libpaper-1.1.24.4
libpagemaker-0.0.3
libogg-1.3.2_1,4
libodfgen01-0.1.6
libmwaw03-0.3.8
libmpeg2-0.5.1_6
libmatroska-1.4.5
libmad-0.15.1b_6
libltdl-2.4.6
liblqr-1-0.4.2
libidn-1.33_1
libiconv-1.14_9
libgltf-0.0.2_1
libglapi-11.2.2
libgcrypt-1.7.3
libfpx-1.3.1.4_1
libffi-3.2.1
libexttextcat-3.4.4
libevent2-2.0.22_1
libetonyek01-0.1.6,1
libepoxy-1.3.1
libedit-3.1.20150325_2,1
libdvdread-5.0.3
libdvdnav-5.0.3
libdvbpsi-1.3.0
libdrm-2.4.66,1
libdca-0.0.5_1
libcroco-0.6.11
libcmis-0.5.1
libcddb-1.3.2_4
libassuan-2.4.3
libantlr3c-3.4_1
libabw-0.1.1_1
liba52-0.7.4_3
libXxf86vm-1.1.4_1
libXvMC-1.0.10
libXv-1.0.11,1
libXtst-1.2.3
libXt-1.1.5,1
libXrender-0.9.10
libXrandr-1.5.1
libXmu-1.1.2_3,1
libXinerama-1.1.3_3,1
libXi-1.7.8,1
libXft-2.3.2_1
libXfixes-5.0.3
libXext-1.3.3_1,1
libXdmcp-1.1.2
libXdamage-1.1.4_3
libXcursor-1.1.14_3
libXcomposite-0.4.4_3,1
libXaw-1.0.13,2
libXau-1.0.8_3
libXScrnSaver-1.2.2_3
libX11-1.6.4,1
libSM-1.2.2_3,1
libIDL-0.8.14_2
libICE-1.0.9_1,1
libGLU-9.0.0_2
libGL-11.2.2
libEGL-11.2.2
jpeg-turbo-1.5.1
jbigkit-2.1_1
jasper-1.900.1_16
ilmbase-2.2.0
hyphen-2.8.8
hunspell-1.3.3
gtkspell-2.0.16_5
gtkmm24-2.24.4_2
gtk3-3.18.8_3
gtk2-2.24.29_2
gstreamer1-1.8.0
gsl-1.16_2
gnutls-3.4.16
gmp-5.1.3_3
glibmm-2.44.0,1
glew-1.13.0
giflib-5.1.4
gettext-runtime-0.19.8.1
gdk-pixbuf2-2.32.3_1
gconf2-3.2.6_4
gbm-11.2.2
freetype2-2.6.3
fontconfig-2.12.1,1
flac-1.3.1_2
fftw3-3.3.5
faad2-2.7_6,1
expat-2.2.0
espeak-1.48.04_1
enchant-1.6.0_5
dotconf-1.3_1
dbus-glib-0.104
dbus-1.8.20
db5-5.3.28_6
curl-7.51.0_1
cups-2.2.1
colord-1.2.11_1
clucene-2.3.3.4_7
cairomm-1.10.0_3
cairo-1.14.6_1,2
boehm-gc-7.6.0
bctoolbox-0.2.0
baresip-0.4.19 (options changed)
avahi-app-0.6.31_5
atkmm-2.22.7
atk-2.18.0
at-spi2-atk-2.18.1
apr-1.5.2.1.5.4_2
alsa-lib-1.1.2
ORBit2-2.14.19_1
CoinMP-1.8.3
Number of packages to be upgraded: 51
Number of packages to be reinstalled: 185
The process will require 19 MiB more space.
491 MiB to be downloaded.
Proceed with this action? [y/N]:
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 0001-Optimise-SAT-solving.patch
Type: text/x-patch
Size: 8744 bytes
Desc: not available
URL: <http://lists.freebsd.org/pipermail/freebsd-current/attachments/20161124/fb1bf1c5/attachment.bin>
More information about the freebsd-current
mailing list