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 09:42:09 UTC 2010 #Using input file /home/misc2010/data/2010/easy/randadea40.cudf #Using ouput file /home/misc2010/tmp/201007050905/p2cudf-trendy-1.6/randadea40.cudf.easy.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:2229 #Parsing done (2.229s). #Solving ... #Request size: 1665 #Number of packages after slice: 3056 #Slice efficiency: 91% ## 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 12347 37480 # Current objective function value: 1880293378812(1.03s) # Current objective function value: 1880293351783(1.41s) # Current objective function value: 1880293343674(1.66s) # Current objective function value: 1880293343673(1.91s) # Trendy criteria value: -95, -0, -52, -338 # Proof: [AbstractVariable: alsa-base, AbstractVariable: brasero, AbstractVariable: cheese, AbstractVariable: chromium-browser, AbstractVariable: cups, AbstractVariable: cups-bsd, AbstractVariable: cups-driver-gutenprint, AbstractVariable: cvs, AbstractVariable: dasher, AbstractVariable: deskbar-applet, AbstractVariable: eog, AbstractVariable: epiphany-browser, AbstractVariable: evince, AbstractVariable: evolution, AbstractVariable: f-spot, AbstractVariable: foomatic-db-gutenprint, AbstractVariable: foomatic-filters-ppds, AbstractVariable: gconf-editor, AbstractVariable: gdm3, AbstractVariable: gecko-mediaplayer, AbstractVariable: ghostscript, AbstractVariable: ghostscript-cups, AbstractVariable: gimp, AbstractVariable: gnome-about, AbstractVariable: gnome-accessibility, AbstractVariable: gnome-applets, AbstractVariable: gnome-control-center, AbstractVariable: gnome-core, AbstractVariable: gnome-dictionary, AbstractVariable: gnome-icon-theme, AbstractVariable: gnome-keyring-manager, AbstractVariable: gnome-mag, AbstractVariable: gnome-media, AbstractVariable: gnome-mplayer, AbstractVariable: gnome-netstatus-applet, AbstractVariable: gnome-orca, AbstractVariable: gnome-panel, AbstractVariable: gnome-power-manager, AbstractVariable: gnome-screensaver, AbstractVariable: gnome-session, AbstractVariable: gnome-utils, AbstractVariable: gs-common, AbstractVariable: gsfonts, AbstractVariable: gstreamer0.10-ffmpeg, AbstractVariable: gstreamer0.10-plugins-bad, AbstractVariable: gstreamer0.10-plugins-base, AbstractVariable: gstreamer0.10-plugins-good, AbstractVariable: hplip, AbstractVariable: hplip-cups, AbstractVariable: ijsgutenprint, AbstractVariable: latex-make, AbstractVariable: libavcodec52, AbstractVariable: libavformat52, AbstractVariable: libbonoboui2-0, AbstractVariable: libboost-program-options1.42.0, AbstractVariable: libfile-copy-recursive-perl, AbstractVariable: libgail-gnome-module, AbstractVariable: libgnome2-perl, AbstractVariable: libgnome2.24-cil, AbstractVariable: libgnomeui-0, AbstractVariable: libmagickcore3-extra, AbstractVariable: libmjpegtools-1.9, AbstractVariable: libpanel-applet2-0, AbstractVariable: libpolkit-agent-1-0, AbstractVariable: libpolkit-gtk-1-0, AbstractVariable: libquicktime1, AbstractVariable: librpcsecgss3, AbstractVariable: libshout3, AbstractVariable: libtheora0, AbstractVariable: libwmf0.2-7, AbstractVariable: miro, AbstractVariable: mjpegtools, AbstractVariable: mousetweaks, AbstractVariable: mplayer, AbstractVariable: nfs-common, AbstractVariable: openbsd-inetd, AbstractVariable: policykit-1-gnome, AbstractVariable: printconf, AbstractVariable: prosper, AbstractVariable: ps2eps, AbstractVariable: pstoedit, AbstractVariable: purifyeps, AbstractVariable: python-gnome2, AbstractVariable: python-gnomeapplet, AbstractVariable: python-pyatspi, AbstractVariable: rhythmbox, AbstractVariable: rhythmbox-plugins, AbstractVariable: sane-utils, AbstractVariable: schroot, AbstractVariable: update-inetd, AbstractVariable: vlc, AbstractVariable: vlc-nox, AbstractVariable: vlc-plugin-pulse, AbstractVariable: x-ttcidfont-conf, AbstractVariable: xchat-gnome, AbstractVariable: 31538514, AbstractVariable: 14800362, AbstractVariable: 21173056, AbstractVariable: 11587215, AbstractVariable: 28899428, AbstractVariable: 22048196, AbstractVariable: 2859291, AbstractVariable: 31952838, AbstractVariable: 3916375, AbstractVariable: 25919971, AbstractVariable: 31999426, AbstractVariable: 5924809, AbstractVariable: 22507120, AbstractVariable: 9030750, AbstractVariable: 849515, AbstractVariable: 9717476, AbstractVariable: 16837612, AbstractVariable: 8344960, AbstractVariable: 8702985, AbstractVariable: 20000831, AbstractVariable: 5670411, AbstractVariable: 28708894, AbstractVariable: 31212095, AbstractVariable: 4744654, AbstractVariable: 18071221, AbstractVariable: 25383640, AbstractVariable: 14298351, AbstractVariable: 18414151, AbstractVariable: 14111765, AbstractVariable: 25068634, AbstractVariable: 12518719, AbstractVariable: 28142411, AbstractVariable: 32200294, AbstractVariable: 8345839, AbstractVariable: 7549020, AbstractVariable: 24032956, AbstractVariable: 20453728, AbstractVariable: 21720045, AbstractVariable: 13044493, AbstractVariable: 30284778, AbstractVariable: 9936743, AbstractVariable: 5489653, AbstractVariable: 2062088, AbstractVariable: 19256862, AbstractVariable: 14456678, AbstractVariable: 5958617, AbstractVariable: 7437713, AbstractVariable: 1173553, AbstractVariable: 4347715, AbstractVariable: 31633330, AbstractVariable: 25232872, AbstractVariable: 16949413, AbstractVariable: 9menu, AbstractVariable: a2ps, AbstractVariable: amiwm, AbstractVariable: anthy-common, AbstractVariable: aptitude-doc-cs, AbstractVariable: aqsis-libs-dev, AbstractVariable: aqsis-libsc2a, AbstractVariable: aspell, AbstractVariable: aspell-he, AbstractVariable: aterm, AbstractVariable: aterm-ml, AbstractVariable: aumix-common, AbstractVariable: aumix-gtk, AbstractVariable: autopoint, AbstractVariable: awesome, AbstractVariable: bcc, AbstractVariable: bcron, AbstractVariable: bin86, AbstractVariable: bluez-alsa, AbstractVariable: bluez-gstreamer, AbstractVariable: bzr, AbstractVariable: bzrtools, AbstractVariable: ca-certificates-java, AbstractVariable: cabextract, AbstractVariable: cdcd, AbstractVariable: cddb, AbstractVariable: citadel-server, AbstractVariable: conkeror, AbstractVariable: conkeror-spawn-process-helper, AbstractVariable: cpp-4.1, AbstractVariable: cvsnt, AbstractVariable: db4.6-util, AbstractVariable: debian-el, AbstractVariable: debootstrap, AbstractVariable: dirac, AbstractVariable: dkms, AbstractVariable: dlocate, AbstractVariable: dmraid, AbstractVariable: dracut, AbstractVariable: dwm, AbstractVariable: dwm-tools, AbstractVariable: e16, AbstractVariable: e16-data, AbstractVariable: elinks, AbstractVariable: elinks-data, AbstractVariable: elks-libc, AbstractVariable: emacs23-bin-common, AbstractVariable: emacs23-common, AbstractVariable: emacs23-nox, AbstractVariable: emacsen-common, AbstractVariable: epdfview, AbstractVariable: exo-utils, AbstractVariable: fancontrol, AbstractVariable: festival, 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: fglrx-atieventsd, AbstractVariable: fglrx-driver, AbstractVariable: fglrx-glx, AbstractVariable: fglrx-glx-ia32, AbstractVariable: fglrx-modules-dkms, AbstractVariable: fluxbox, AbstractVariable: flwm, AbstractVariable: fortune-mod, AbstractVariable: fortunes, AbstractVariable: fortunes-debian-hints, AbstractVariable: fortunes-min, AbstractVariable: fortunes-off, AbstractVariable: fvwm, AbstractVariable: fvwm-crystal, AbstractVariable: fvwm-icons, AbstractVariable: gcc-4.1, AbstractVariable: gcc-4.1-base, 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-gnomevfs, AbstractVariable: gstreamer0.10-pulseaudio, AbstractVariable: hsetroot, AbstractVariable: i3-wm, AbstractVariable: ia32-sun-java6-bin, AbstractVariable: icedtea-6-jre-cacao, AbstractVariable: icewm-common, AbstractVariable: ipsvd, AbstractVariable: java-common, AbstractVariable: jed-common, AbstractVariable: jed-extra, AbstractVariable: kazehakase, AbstractVariable: kazehakase-gecko, AbstractVariable: kazehakase-webkit, AbstractVariable: kbuild, AbstractVariable: kdelibs5-data, AbstractVariable: kernel-package, AbstractVariable: kterm, AbstractVariable: libaccess-bridge-java, AbstractVariable: libaccess-bridge-java-jni, AbstractVariable: libafterimage0, AbstractVariable: libalgorithm-diff-perl, AbstractVariable: libalgorithm-merge-perl, AbstractVariable: libanthy0, AbstractVariable: libanyevent-i3-perl, AbstractVariable: libanyevent-perl, AbstractVariable: libarray-printcols-perl, AbstractVariable: libasync-interrupt-perl, AbstractVariable: libatk1-ruby1.8, AbstractVariable: libatm1, AbstractVariable: libattica0, AbstractVariable: libavahi-compat-libdnssd1, AbstractVariable: libbg1, AbstractVariable: libbg1-doc, AbstractVariable: libcairo-ruby1.8, AbstractVariable: libcitadel2, AbstractVariable: libclucene0ldbl, AbstractVariable: libcommon-sense-perl, AbstractVariable: libdigest-hmac-perl, AbstractVariable: libdmraid1.0.0.rc16, AbstractVariable: libestools1.2, AbstractVariable: libestraier8, AbstractVariable: libev3, AbstractVariable: libexo-0.3-0, AbstractVariable: libexo-common, AbstractVariable: libfltk1.1, AbstractVariable: libfont-afm-perl, AbstractVariable: libfsplib0, AbstractVariable: libgdk-pixbuf2-ruby1.8, AbstractVariable: libgjs0a, AbstractVariable: libglib2-ruby1.8, AbstractVariable: libgnustep-base1.19, AbstractVariable: libgpod-common, AbstractVariable: libgsasl7, AbstractVariable: libgtk2-ruby, AbstractVariable: libgtk2-ruby1.8, AbstractVariable: libhtml-format-perl, AbstractVariable: libhubbub0, AbstractVariable: libio-socket-inet6-perl, AbstractVariable: libiodbc2, AbstractVariable: libjs-mootools, AbstractVariable: libjson-perl, AbstractVariable: libjson-xs-perl, AbstractVariable: libkdecore5, AbstractVariable: libkdeui5, AbstractVariable: libkeybinder0, AbstractVariable: libkio5, AbstractVariable: libknewstuff2-4, AbstractVariable: libknewstuff3-4, AbstractVariable: libltdl-dev, AbstractVariable: libm17n-0, AbstractVariable: libmail-spf-perl, AbstractVariable: libmatrixssl1.8, AbstractVariable: libmpdclient2, AbstractVariable: libmutter-private0, AbstractVariable: libnet-dns-perl, AbstractVariable: libnet-ip-perl, AbstractVariable: libnetaddr-ip-perl, AbstractVariable: libnsbmp0, AbstractVariable: libnsgif0, AbstractVariable: libntlm0, AbstractVariable: libobjc2, AbstractVariable: libobparser21, AbstractVariable: libobrender21, AbstractVariable: libonig2, AbstractVariable: libotf0, AbstractVariable: libotp0-heimdal, AbstractVariable: libpacketdump3, AbstractVariable: libpango1-ruby1.8, AbstractVariable: libpaper-utils, AbstractVariable: libparserutils0, AbstractVariable: libpulse-browse0, AbstractVariable: libqca2, AbstractVariable: libqdbm14, AbstractVariable: libqpx-dev, AbstractVariable: libqpx0, AbstractVariable: librecode0, AbstractVariable: libroken18-heimdal, AbstractVariable: librplay3, AbstractVariable: libsieve2-1, AbstractVariable: libslang2-modules, AbstractVariable: libsocket6-perl, AbstractVariable: libsolid4, AbstractVariable: libsoprano4, AbstractVariable: libstreamanalyzer0, AbstractVariable: libstreams0, AbstractVariable: libstroke0, AbstractVariable: libthunar-vfs-1-2, AbstractVariable: libtool, AbstractVariable: libtrace-tools, AbstractVariable: libtrace3, AbstractVariable: libtre5, AbstractVariable: libvisual-0.4-plugins, AbstractVariable: libvncserver0, AbstractVariable: libx11-protocol-perl, AbstractVariable: libxcb-icccm1, AbstractVariable: libxcb-image0, AbstractVariable: libxcb-property1, AbstractVariable: libxcb-randr0, AbstractVariable: libxcb-shape0, AbstractVariable: libxcb-shm0, 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: libyajl1, AbstractVariable: linux-image-2.6.32-5-openvz-amd64, AbstractVariable: linux-image-2.6.32-5-vserver-amd64, AbstractVariable: linux-image-2.6.32-5-xen-amd64, AbstractVariable: lxsession, AbstractVariable: m17n-contrib, AbstractVariable: m17n-db, AbstractVariable: mdadm, AbstractVariable: mercurial, AbstractVariable: mercurial-common, AbstractVariable: mesa-utils, AbstractVariable: mlterm, AbstractVariable: mlterm-common, AbstractVariable: mlterm-tools, AbstractVariable: mpc, AbstractVariable: msmtp, AbstractVariable: mutter, AbstractVariable: mutter-common, AbstractVariable: navit-graphics-qt-qpainter, AbstractVariable: navit-gui-gtk, AbstractVariable: netsurf-framebuffer-common, AbstractVariable: netsurf-gtk, AbstractVariable: netsurf-linuxfb, AbstractVariable: netsurf-sdl, AbstractVariable: netsurf-vnc, AbstractVariable: odbcinst, AbstractVariable: odbcinst1debian2, AbstractVariable: openbox, AbstractVariable: openbox-themes, AbstractVariable: openjdk-6-jre-headless, AbstractVariable: openjdk-6-jre-lib, AbstractVariable: openoffice.org-emailmerge, AbstractVariable: openoffice.org-filter-binfilter, AbstractVariable: openoffice.org-l10n-ne, AbstractVariable: openssh-server, AbstractVariable: oss-compat, AbstractVariable: perl-tk, AbstractVariable: perlmagick, AbstractVariable: psutils, AbstractVariable: pulseaudio, AbstractVariable: pulseaudio-esound-compat, AbstractVariable: pulseaudio-module-x11, AbstractVariable: pulseaudio-utils, AbstractVariable: python-configobj, AbstractVariable: python-crypto, AbstractVariable: python-keybinder, AbstractVariable: python-paramiko, AbstractVariable: python-uno, AbstractVariable: ratpoison, AbstractVariable: re2c, AbstractVariable: rox-filer, AbstractVariable: roxterm, AbstractVariable: runit, AbstractVariable: rxvt, AbstractVariable: rxvt-ml, AbstractVariable: sbcl, AbstractVariable: scrotwm, AbstractVariable: slsh, AbstractVariable: socklog, AbstractVariable: soprano-daemon, AbstractVariable: spamassassin, AbstractVariable: spamc, AbstractVariable: sun-java6-bin, AbstractVariable: sun-java6-jre, AbstractVariable: tango-icon-theme, AbstractVariable: terminator, AbstractVariable: texlive-fonts-recommended-doc, AbstractVariable: texlive-humanities-doc, AbstractVariable: texlive-latex-extra-doc, AbstractVariable: texlive-latex-recommended-doc, AbstractVariable: texlive-pictures-doc, AbstractVariable: texlive-pstricks-doc, AbstractVariable: thunar, AbstractVariable: thunar-data, AbstractVariable: thunar-volman, AbstractVariable: tightvncserver, AbstractVariable: tipa, AbstractVariable: tla, AbstractVariable: tla-doc, AbstractVariable: trayer, AbstractVariable: ttf-bitstream-vera, AbstractVariable: ttf-devanagari-fonts, AbstractVariable: ttf-mscorefonts-installer, AbstractVariable: tzdata-java, AbstractVariable: ucspi-unix, AbstractVariable: ude, AbstractVariable: unixodbc, AbstractVariable: util-vserver, AbstractVariable: uwm, AbstractVariable: virtualbox-ose-guest-source, AbstractVariable: virtualbox-ose-guest-utils, AbstractVariable: virtualbox-ose-guest-x11, AbstractVariable: vnc4server, AbstractVariable: vzctl, AbstractVariable: vzquota, AbstractVariable: wmii, AbstractVariable: wmii-doc, AbstractVariable: wodim, AbstractVariable: xbill, 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: xinput, AbstractVariable: xjed, AbstractVariable: xlockmore, AbstractVariable: xnest, AbstractVariable: zeroinstall-injector] # starts : 24 # conflicts : 4526 # decisions : 237442 # propagations : 3492047 # inspects : 6915719 # learnt literals : 43 # learnt binary clauses : 96 # learnt ternary clauses : 122 # learnt clauses : 4482 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 1052872 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 0 # 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) : 109167.40652744779 # non guided choices 51907 # learnt constraints type #Solving done (36.2s). #Solution contains:1864