HEAD is now at 0e68ffa initial deployement # Checking available version of Java # Java(TM) SE Runtime Environment (build 1.6.0_12-b04) # Running really p2cudf #Solver launched on Mon Jul 05 19:29:25 UTC 2010 #Using input file /home/misc2010/data/2010/debian-dudf/e0bd67a6-56d0-11df-b11f-00163e7a6f5e.cudf #Using ouput file /home/misc2010/tmp/201007051233/p2cudf-trendy-1.6/e0bd67a6-56d0-11df-b11f-00163e7a6f5e.cudf.debian-dudf.result #Objective function trendy #Timeout 280s #java.runtime.name Java(TM) SE Runtime Environment #java.vm.name Java HotSpot(TM) Server VM #java.vm.version 11.2-b01 #java.vm.vendor Sun Microsystems Inc. #sun.arch.data.model 32 #java.version 1.6.0_12 #os.name Linux #os.version 2.6.18-6-xen-amd64 #os.arch i386 #Free memory 721951896 #Max memory 725876736 #Total memory 725876736 #Number of processors 1 #Parsing ... #Time to parse:2283 #Parsing done (2.283s). #Solving ... #Request size: 1582 #Number of packages after slice: 2937 #Slice efficiency: 90% ## Optimization to Pseudo Boolean adapter # Pseudo Boolean Optimization # --- Begin Solver configuration --- # Stops conflict analysis at the first Unique Implication Point # org.sat4j.pb.constraints.CompetResolutionPBMixedWLClauseCardConstrDataStructure@1aa57fb # Learn all clauses as in MiniSAT # claDecay=0.999 varDecay=0.95 conflictBoundIncFactor=1.5 initConflictBound=100 # VSIDS like heuristics from MiniSAT using a heap lightweight component caching from RSAT taking into account the objective function # Expensive reason simplification # Armin Biere (Picosat) restarts strategy # Glucose learned constraints deletion strategy # timeout=280s # DB Simplification allowed=false # --- End Solver configuration --- # Optimization function: misc 2010, trendy # p cnf 11521 36245 # Current objective function value: 243628941869(1.44s) # Current objective function value: 242642592568(1.74s) # Current objective function value: 242642587617(2.04s) # Current objective function value: 242636457047(2.22s) # Current objective function value: 242636457046(19.503s) # cleaning 2494 clauses out of 4994 with flag 5000/5000 # cleaning 4208 clauses out of 8468 with flag 11000/11000 # cleaning 5629 clauses out of 11259 with flag 18000/18000 # cleaning 6811 clauses out of 13628 with flag 26001/26001 # Current objective function value: 242636454578(234.384s) # Current objective function value: 242636454577(234.504s) # cleaning 7906 clauses out of 15816 with flag 35001/35001 # Trendy criteria value: -16, -10, -6, -352 # Proof: [AbstractVariable: epiphany-gecko, AbstractVariable: gdeb, AbstractVariable: gir1.0-clutter-0.8, AbstractVariable: gnome-apt, AbstractVariable: gnome-network-admin, AbstractVariable: libdatrie0, AbstractVariable: libeel2-2.20, AbstractVariable: libgd2-noxpm, AbstractVariable: libgnomekbd2, AbstractVariable: libgnomekbdui2, AbstractVariable: libgtksourceview1.0-0, AbstractVariable: libmetacity0, AbstractVariable: libslab0, AbstractVariable: libxcb-xlib0, AbstractVariable: nautilus-cd-burner, AbstractVariable: openoffice.org-debian-menus, AbstractVariable: gnome-power-manager, AbstractVariable: gnome-session, AbstractVariable: gnome-session-bin, AbstractVariable: gnome-session-common, AbstractVariable: libcairo2, AbstractVariable: libcairo2-dev, AbstractVariable: libdevkit-power-gobject1, AbstractVariable: libpango1.0-0, AbstractVariable: libpango1.0-dev, AbstractVariable: xulrunner-1.9.1, AbstractVariable: 29418586, AbstractVariable: 10038190, AbstractVariable: 20453728, AbstractVariable: 6620348, AbstractVariable: 13137563, AbstractVariable: 32623606, AbstractVariable: 9menu, AbstractVariable: a2ps, AbstractVariable: amiwm, AbstractVariable: apt-xapian-index, AbstractVariable: aptitude-doc-ja, AbstractVariable: aspell, AbstractVariable: aspell-cy, AbstractVariable: aterm, AbstractVariable: aterm-ml, AbstractVariable: audacious, AbstractVariable: audacious-plugins, AbstractVariable: audacious-plugins-extra, AbstractVariable: aumix, AbstractVariable: aumix-common, AbstractVariable: autopoint, AbstractVariable: autotools-dev, AbstractVariable: awesome, AbstractVariable: bcc, AbstractVariable: bcron, AbstractVariable: bin86, AbstractVariable: citadel-server, AbstractVariable: compiz-core, AbstractVariable: compiz-plugins, AbstractVariable: conkeror, AbstractVariable: conkeror-spawn-process-helper, AbstractVariable: cpp-4.1, AbstractVariable: crafty, AbstractVariable: crafty-books-small, AbstractVariable: db4.6-util, AbstractVariable: debian-edu-artwork-usplash, AbstractVariable: device3dfx-source, AbstractVariable: dkms, AbstractVariable: dolphin, AbstractVariable: dwm, AbstractVariable: dwm-tools, AbstractVariable: e16, AbstractVariable: e16-data, AbstractVariable: elinks, AbstractVariable: elinks-data, AbstractVariable: elks-libc, AbstractVariable: exfalso, AbstractVariable: exo-utils, AbstractVariable: fairymax, AbstractVariable: festival-hi, AbstractVariable: festival-mr, AbstractVariable: festival-te, AbstractVariable: festlex-ifd, AbstractVariable: festvox-hi-nsk, AbstractVariable: festvox-italp16k, AbstractVariable: festvox-itapc16k, AbstractVariable: festvox-mr-nsk, AbstractVariable: festvox-suopuhe-common, AbstractVariable: festvox-suopuhe-lj, AbstractVariable: festvox-suopuhe-mv, AbstractVariable: festvox-te-nsk, AbstractVariable: fetchmail, AbstractVariable: fgetty, AbstractVariable: fluxbox, AbstractVariable: flwm, AbstractVariable: foomatic-db, AbstractVariable: foomatic-db-engine, AbstractVariable: foomatic-filters, AbstractVariable: fortune-mod, AbstractVariable: fortunes, AbstractVariable: fortunes-debian-hints, AbstractVariable: fortunes-min, AbstractVariable: fortunes-off, AbstractVariable: fvwm, AbstractVariable: fvwm-crystal, AbstractVariable: fvwm-icons, AbstractVariable: galeon, AbstractVariable: galeon-common, AbstractVariable: gcc-4.1, AbstractVariable: gcc-4.1-base, AbstractVariable: geeqie-gps, AbstractVariable: gir1.0-mutter-2.29, AbstractVariable: gnome-audio, AbstractVariable: gnome-shell, AbstractVariable: gnustep-base-common, AbstractVariable: gnustep-base-runtime, AbstractVariable: gnustep-common, AbstractVariable: gstreamer0.10-pulseaudio, AbstractVariable: gthumb, AbstractVariable: gthumb-data, AbstractVariable: hsetroot, AbstractVariable: i3-wm, AbstractVariable: icewm-common, AbstractVariable: ipsvd, AbstractVariable: irb1.8, AbstractVariable: jed-common, AbstractVariable: jed-extra, AbstractVariable: kazehakase, AbstractVariable: kazehakase-gecko, AbstractVariable: kazehakase-webkit, AbstractVariable: kbuild, AbstractVariable: kdebase-bin, AbstractVariable: kdebase-data, AbstractVariable: kfind, AbstractVariable: knm-runtime, AbstractVariable: konqueror, AbstractVariable: konqueror-nsplugins, AbstractVariable: kterm, AbstractVariable: kwalletmanager, AbstractVariable: libafterimage0, AbstractVariable: libanthy0, AbstractVariable: libasound2-plugins, AbstractVariable: libatm1, AbstractVariable: libaudclient2, AbstractVariable: libaudcore1, AbstractVariable: libaudid3tag2, AbstractVariable: libaudutil1, AbstractVariable: libbg1, AbstractVariable: libbg1-doc, AbstractVariable: libbind9-60, AbstractVariable: libbinio1ldbl, AbstractVariable: libboost-iostreams1.40.0, AbstractVariable: libcitadel2, AbstractVariable: libclass-accessor-perl, AbstractVariable: libcurl3, AbstractVariable: libdecoration0, AbstractVariable: libdiscid0, AbstractVariable: libdns64, AbstractVariable: libdrm-radeon1, AbstractVariable: liberror-perl, AbstractVariable: libestraier8, AbstractVariable: libev3, AbstractVariable: libexo-0.3-0, AbstractVariable: libexo-common, AbstractVariable: libfluidsynth1, AbstractVariable: libfont-afm-perl, AbstractVariable: libfsplib0, AbstractVariable: libgettext-ruby1.8, AbstractVariable: libgjs0, AbstractVariable: libglide2, AbstractVariable: libgnomeprint2.2-data, AbstractVariable: libgnomeprintui2.2-common, AbstractVariable: libgnustep-base1.19, AbstractVariable: libgpod-common, AbstractVariable: libgpod4, AbstractVariable: libgraphicsmagick3, AbstractVariable: libgraphite3, AbstractVariable: libgsasl7, AbstractVariable: libgtk2-ruby, AbstractVariable: libhtml-format-perl, AbstractVariable: libhtml-template-perl, AbstractVariable: libimlib2, AbstractVariable: libio-socket-inet6-perl, AbstractVariable: libio-string-perl, AbstractVariable: libiodbc2, AbstractVariable: libisc60, AbstractVariable: libisccc60, AbstractVariable: libisccfg60, AbstractVariable: libjpeg-progs, AbstractVariable: libjpeg8, AbstractVariable: libk3b6, AbstractVariable: libk3b6-extracodecs, AbstractVariable: libkcddb4, AbstractVariable: libkonq5, AbstractVariable: libkonq5-templates, AbstractVariable: libkonqsidebarplugin4, AbstractVariable: liblash2, AbstractVariable: liblocale-ruby1.8, AbstractVariable: liblog4cxx10, AbstractVariable: liblouis2, AbstractVariable: libltdl-dev, AbstractVariable: liblwres60, AbstractVariable: liblzma2, AbstractVariable: liblzo2-2, AbstractVariable: libm17n-0, AbstractVariable: libmagick++3, AbstractVariable: libmagickcore3, AbstractVariable: libmagickwand3, AbstractVariable: libmail-spf-perl, AbstractVariable: libmailtools-perl, AbstractVariable: libmatrixssl1.8, AbstractVariable: libmcs1, AbstractVariable: libmowgli1, AbstractVariable: libmpdclient2, AbstractVariable: libmtp8, AbstractVariable: libmutter-private0, AbstractVariable: libnetaddr-ip-perl, AbstractVariable: libntfs-3g75, AbstractVariable: libntlm0, AbstractVariable: libobjc2, AbstractVariable: libobparser21, AbstractVariable: libobrender21, AbstractVariable: libonig2, AbstractVariable: libopenraw1, AbstractVariable: libopenrawgnome1, AbstractVariable: liborc-0.4-0, AbstractVariable: libotf0, AbstractVariable: libpaper-utils, AbstractVariable: libparse-debianchangelog-perl, AbstractVariable: libpkcs11-helper1, AbstractVariable: libprojectm-data, AbstractVariable: libprojectm2, AbstractVariable: libpt-1.10.10-plugins-alsa, AbstractVariable: libpt-1.10.10-plugins-v4l2, AbstractVariable: libpulse-browse0, AbstractVariable: libqdbm14, AbstractVariable: libreadline-ruby1.8, AbstractVariable: librecode0, AbstractVariable: libresid-builder0c2a, AbstractVariable: librplay3, AbstractVariable: librpmbuild0, AbstractVariable: libruby, AbstractVariable: libsad2, AbstractVariable: libsidplay2, AbstractVariable: libsieve2-1, AbstractVariable: libslang2-modules, AbstractVariable: libsocket6-perl, AbstractVariable: libsolidcontrol4, AbstractVariable: libsolidcontrolifaces4, AbstractVariable: libssh2-1, AbstractVariable: libstroke0, AbstractVariable: libsub-name-perl, AbstractVariable: libthunar-vfs-1-2, AbstractVariable: libtie-ixhash-perl, AbstractVariable: libtool, AbstractVariable: libtre5, AbstractVariable: libvisual-0.4-plugins, AbstractVariable: libx11-protocol-perl, AbstractVariable: libxcb-icccm1, AbstractVariable: libxcb-image0, AbstractVariable: libxcb-property1, AbstractVariable: libxcb-randr0, AbstractVariable: libxcb-xinerama0, AbstractVariable: libxcb-xtest0, AbstractVariable: libxdg-basedir1, AbstractVariable: libxfce4menu-0.1-0, AbstractVariable: libxfce4util-bin, AbstractVariable: libxfce4util-common, AbstractVariable: libxfce4util4, AbstractVariable: libxfcegui4-4, AbstractVariable: libxfconf-0-2, AbstractVariable: linux-headers-2.6.32-3-common-vserver, AbstractVariable: linux-headers-2.6.32-3-vserver-686-bigmem, AbstractVariable: linux-image-2.6.30-2-686, AbstractVariable: linux-image-2.6.30-2-686-bigmem, AbstractVariable: linux-image-2.6.32-3-486, AbstractVariable: linux-image-2.6.32-3-686, AbstractVariable: linux-image-2.6.32-3-686-bigmem, AbstractVariable: linux-image-2.6.32-3-amd64, AbstractVariable: linux-image-2.6.32-3-vserver-686, AbstractVariable: linux-image-2.6.32-3-vserver-686-bigmem, AbstractVariable: linux-kbuild-2.6.32, AbstractVariable: lxsession, AbstractVariable: lynx-cur, AbstractVariable: m17n-contrib, AbstractVariable: m17n-db, AbstractVariable: midori, AbstractVariable: mlterm, AbstractVariable: mlterm-common, AbstractVariable: mlterm-tools, AbstractVariable: module-assistant, AbstractVariable: mpc, AbstractVariable: msmtp, AbstractVariable: mutter, AbstractVariable: mutter-common, AbstractVariable: netsurf, AbstractVariable: network-manager-kde, AbstractVariable: network-manager-openvpn, AbstractVariable: network-manager-pptp, AbstractVariable: network-manager-vpnc, AbstractVariable: openbox, AbstractVariable: openbox-themes, AbstractVariable: openoffice.org-common, AbstractVariable: openoffice.org-core, AbstractVariable: openoffice.org-style-galaxy, AbstractVariable: openssl-blacklist, AbstractVariable: openvpn, AbstractVariable: openvpn-blacklist, AbstractVariable: perl-tk, AbstractVariable: phonon-backend-gstreamer, AbstractVariable: pptp-linux, AbstractVariable: psfontmgr, AbstractVariable: pulseaudio, AbstractVariable: pulseaudio-esound-compat, AbstractVariable: pulseaudio-module-x11, AbstractVariable: pulseaudio-utils, AbstractVariable: python-beagle, AbstractVariable: python-cddb, AbstractVariable: python-gpod, AbstractVariable: python-gtkhtml2, AbstractVariable: python-musicbrainz2, AbstractVariable: python-mutagen, AbstractVariable: python-simplejson, AbstractVariable: python-xapian, AbstractVariable: quodlibet, AbstractVariable: quodlibet-ext, AbstractVariable: quodlibet-plugins, AbstractVariable: ratpoison, AbstractVariable: re2c, AbstractVariable: rlwrap, AbstractVariable: rox-filer, AbstractVariable: rpm, AbstractVariable: runit, AbstractVariable: rxvt, AbstractVariable: rxvt-ml, AbstractVariable: scid, AbstractVariable: scrotwm, AbstractVariable: slsh, AbstractVariable: socklog, AbstractVariable: spamassassin, AbstractVariable: spamc, AbstractVariable: stalonetray, AbstractVariable: tdom, AbstractVariable: terminator, AbstractVariable: texlive-games, AbstractVariable: thunar, AbstractVariable: thunar-data, AbstractVariable: thunar-volman, AbstractVariable: tightvncserver, AbstractVariable: ttf-opensymbol, AbstractVariable: ucspi-unix, AbstractVariable: ude, AbstractVariable: udisks, AbstractVariable: ure, AbstractVariable: usb-modeswitch, AbstractVariable: usb-modeswitch-data, AbstractVariable: uuid-runtime, AbstractVariable: uwm, AbstractVariable: virtualbox-ose-guest-source, AbstractVariable: virtualbox-ose-guest-utils, AbstractVariable: virtualbox-ose-guest-x11, AbstractVariable: vnc4server, AbstractVariable: vpnc, AbstractVariable: wdiff, AbstractVariable: wmii, AbstractVariable: wmii-doc, AbstractVariable: xboard, AbstractVariable: xdg-user-dirs, AbstractVariable: xfce-keyboard-shortcuts, AbstractVariable: xfce4-panel, AbstractVariable: xfce4-session, AbstractVariable: xfce4-settings, AbstractVariable: xfce4-terminal, AbstractVariable: xfce4-utils, AbstractVariable: xfconf, AbstractVariable: xfdesktop4, AbstractVariable: xfdesktop4-data, AbstractVariable: xfonts-terminus, AbstractVariable: xfwm4, AbstractVariable: xfwm4-themes, AbstractVariable: xjed, AbstractVariable: xli, AbstractVariable: xnest, AbstractVariable: xscreensaver, AbstractVariable: xscreensaver-data, AbstractVariable: xserver-xorg-input-tslib, AbstractVariable: xserver-xorg-video-glide, AbstractVariable: zeroinstall-injector] # starts : 69 # conflicts : 37726 # decisions : 534315 # propagations : 31517769 # inspects : 52397633 # learnt literals : 43 # learnt binary clauses : 197 # learnt ternary clauses : 323 # learnt clauses : 37683 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 11392611 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 5 # number of reductions to clauses (during analyze) : 0 # number of learned constraints concerned by reduction : 0 # number of learning phase by resolution : 0 # number of learning phase by cutting planes : 0 # speed (assignments/second) : 684781.8406987354 # non guided choices 66092 # learnt constraints type #Solving done (282.993s). #Solution contains:1903