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:11:11 UTC 2010 #Using input file /home/misc2010/data/2010/easy/rand1bff33.cudf #Using ouput file /home/misc2010/tmp/201007050905/p2cudf-trendy-1.6/rand1bff33.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:2894 #Parsing done (2.894s). #Solving ... #Request size: 1665 #Number of packages after slice: 3071 #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@ce5b1c # 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 12378 37637 # Current objective function value: 477132269453(1.051s) # Current objective function value: 477132182786(1.357s) # Current objective function value: 477132182785(1.67s) # Trendy criteria value: -24, -0, -10, -433 # Proof: [AbstractVariable: acpi-support, AbstractVariable: avidemux, AbstractVariable: avidemux-plugins, AbstractVariable: foo2zjs, AbstractVariable: gij-4.3, AbstractVariable: gnome-accessibility, AbstractVariable: gnome-core, AbstractVariable: gnome-media, AbstractVariable: gnome-media-common, AbstractVariable: gnome-screensaver, AbstractVariable: gnome-session, AbstractVariable: libgcj9-0, AbstractVariable: libgcj9-jar, AbstractVariable: libgnome-media0, AbstractVariable: libmailtools-perl, AbstractVariable: libmime-tools-perl, AbstractVariable: libmp3lame0, AbstractVariable: libsoap-lite-perl, AbstractVariable: mktemp, AbstractVariable: nmap, AbstractVariable: rhythmbox, AbstractVariable: rhythmbox-plugins, AbstractVariable: vim, AbstractVariable: xscreensaver, AbstractVariable: 29959477, AbstractVariable: 27891041, AbstractVariable: 11688861, AbstractVariable: 9949215, AbstractVariable: 10175206, AbstractVariable: 30293957, AbstractVariable: 10481832, AbstractVariable: 27785692, AbstractVariable: 1801334, AbstractVariable: 25935701, AbstractVariable: 9menu, AbstractVariable: a2ps, AbstractVariable: amiwm, AbstractVariable: anthy-common, AbstractVariable: aptitude-doc-fr, AbstractVariable: aspell, AbstractVariable: aspell-uz, AbstractVariable: aterm, AbstractVariable: aterm-ml, AbstractVariable: audacious, AbstractVariable: audacious-plugins, AbstractVariable: aumix, AbstractVariable: aumix-common, AbstractVariable: autopoint, AbstractVariable: awesome, AbstractVariable: bcc, AbstractVariable: bcron, AbstractVariable: bin86, AbstractVariable: bluez-alsa, AbstractVariable: bluez-cups, AbstractVariable: bluez-gstreamer, AbstractVariable: bzr, AbstractVariable: bzrtools, AbstractVariable: ca-certificates-java, AbstractVariable: cabextract, AbstractVariable: cdparanoia, AbstractVariable: citadel-server, AbstractVariable: conkeror, AbstractVariable: conkeror-spawn-process-helper, AbstractVariable: cpp-4.1, AbstractVariable: db4.6-util, AbstractVariable: debootstrap, AbstractVariable: dkms, AbstractVariable: dmraid, AbstractVariable: dolphin, AbstractVariable: dracut, AbstractVariable: dwm, AbstractVariable: dwm-tools, AbstractVariable: e16, AbstractVariable: e16-data, AbstractVariable: elinks, AbstractVariable: elinks-data, AbstractVariable: elks-libc, AbstractVariable: emboss-doc, AbstractVariable: exfalso, 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-source, AbstractVariable: fluxbox, AbstractVariable: flwm, AbstractVariable: fortune-mod, AbstractVariable: fortunes, AbstractVariable: fortunes-debian-hints, AbstractVariable: fortunes-min, AbstractVariable: fortunes-off, AbstractVariable: fte, AbstractVariable: fte-xwindow, AbstractVariable: fvwm, AbstractVariable: fvwm-crystal, AbstractVariable: fvwm-icons, AbstractVariable: galeon, AbstractVariable: galeon-common, AbstractVariable: gcc-4.1, AbstractVariable: gcc-4.1-base, AbstractVariable: ghostscript-x, AbstractVariable: gir1.0-mutter-2.29, AbstractVariable: gnome-audio, AbstractVariable: gnome-shell, AbstractVariable: gnome3-session, AbstractVariable: gnubg, AbstractVariable: gnubg-data, AbstractVariable: gnustep-base-common, AbstractVariable: gnustep-base-runtime, AbstractVariable: gnustep-common, AbstractVariable: gregorio, AbstractVariable: gregoriotex, AbstractVariable: gsfonts-x11, AbstractVariable: gstreamer0.10-gnomevfs, AbstractVariable: gstreamer0.10-pulseaudio, AbstractVariable: gtk2-engines-pixbuf, AbstractVariable: gv, 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: k3b, AbstractVariable: k3b-data, AbstractVariable: kaboom, AbstractVariable: kazehakase, AbstractVariable: kazehakase-gecko, AbstractVariable: kazehakase-webkit, AbstractVariable: kbuild, AbstractVariable: kde-l10n-sl, AbstractVariable: kdebase-bin, AbstractVariable: kdebase-data, AbstractVariable: kdebase-runtime, AbstractVariable: kdebase-runtime-data, AbstractVariable: kdelibs-bin, AbstractVariable: kdelibs5-data, AbstractVariable: kdelibs5-plugins, AbstractVariable: kdoctools, AbstractVariable: kernel-package, AbstractVariable: kfind, AbstractVariable: konqueror, AbstractVariable: konqueror-nsplugins, 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: libasound2-plugins, AbstractVariable: libasync-interrupt-perl, AbstractVariable: libatk1-ruby1.8, AbstractVariable: libatm1, AbstractVariable: libattica0, AbstractVariable: libaudclient2, AbstractVariable: libaudcore1, AbstractVariable: libaudid3tag2, AbstractVariable: libavahi-compat-libdnssd1, AbstractVariable: libbeagle1, AbstractVariable: libbg1, AbstractVariable: libbg1-doc, AbstractVariable: libbinio1ldbl, AbstractVariable: libcairo-ruby1.8, AbstractVariable: libcitadel2, AbstractVariable: libclucene0ldbl, AbstractVariable: libcommon-sense-perl, AbstractVariable: libcue1, AbstractVariable: libdata-report-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: libflac++6, AbstractVariable: libfltk1.1, AbstractVariable: libfluidsynth1, 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: libgraphicsmagick3, AbstractVariable: libgsasl7, AbstractVariable: libgtk2-ruby, AbstractVariable: libgtk2-ruby1.8, AbstractVariable: libgtkglext1, AbstractVariable: libhtml-format-perl, AbstractVariable: libhubbub0, AbstractVariable: libio-socket-inet6-perl, AbstractVariable: libiodbc2, AbstractVariable: libjs-mootools, AbstractVariable: libjson-perl, AbstractVariable: libjson-xs-perl, AbstractVariable: libk3b6, AbstractVariable: libk3b6-extracodecs, AbstractVariable: libkcddb4, AbstractVariable: libkde3support4, AbstractVariable: libkdecore5, AbstractVariable: libkdesu5, AbstractVariable: libkdeui5, AbstractVariable: libkdnssd4, AbstractVariable: libkeybinder0, AbstractVariable: libkfile4, AbstractVariable: libkhtml5, AbstractVariable: libkio5, AbstractVariable: libkjsapi4, AbstractVariable: libkjsembed4, AbstractVariable: libkmediaplayer4, AbstractVariable: libknewstuff2-4, AbstractVariable: libknewstuff3-4, AbstractVariable: libknotifyconfig4, AbstractVariable: libkntlm4, AbstractVariable: libkonq5, AbstractVariable: libkonq5-templates, AbstractVariable: libkonqsidebarplugin4a, AbstractVariable: libkparts4, AbstractVariable: libkpty4, AbstractVariable: libkrosscore4, AbstractVariable: libktexteditor4, AbstractVariable: libkutils4, AbstractVariable: liblash2, AbstractVariable: libltdl-dev, AbstractVariable: libm17n-0, AbstractVariable: libmail-spf-perl, AbstractVariable: libmatrixssl1.8, AbstractVariable: libmcs1, AbstractVariable: libmowgli1, AbstractVariable: libmpdclient2, AbstractVariable: libmutter-private0, AbstractVariable: libnepomuk4, AbstractVariable: libnepomukquery4a, 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: libpango1-ruby1.8, AbstractVariable: libpaper-utils, AbstractVariable: libparserutils0, AbstractVariable: libphonon4, AbstractVariable: libplasma3, AbstractVariable: libpolkit-qt-1-0, AbstractVariable: libpulse-browse0, AbstractVariable: libqca2, AbstractVariable: libqdbm14, AbstractVariable: libqt4-webkit, AbstractVariable: libqt4-xmlpatterns, AbstractVariable: librecode0, AbstractVariable: libresid-builder0c2a, AbstractVariable: librplay3, AbstractVariable: libsidplay2, AbstractVariable: libsieve2-1, AbstractVariable: libslang2-modules, AbstractVariable: libsocket6-perl, AbstractVariable: libsolid4, AbstractVariable: libsoprano4, AbstractVariable: libssh-4, AbstractVariable: libstreamanalyzer0, AbstractVariable: libstreams0, AbstractVariable: libstroke0, AbstractVariable: libtext-csv-perl, AbstractVariable: libtext-csv-xs-perl, AbstractVariable: libthreadweaver4, AbstractVariable: libthunar-vfs-1-2, AbstractVariable: libtime-y2038-perl, AbstractVariable: libtool, AbstractVariable: libtre5, AbstractVariable: libuno-cli-basetypes1.0-cil, AbstractVariable: libuno-cli-ure1.0-cil, AbstractVariable: libuno-cli-uretypes1.0-cil, AbstractVariable: libvirtodbc0, AbstractVariable: libvisual-0.4-plugins, AbstractVariable: libvncserver0, AbstractVariable: libwmf-bin, 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: libxcb-xv0, AbstractVariable: libxdg-basedir1, AbstractVariable: libxfce4menu-0.1-0, AbstractVariable: libxfce4util-bin, AbstractVariable: libxfce4util-common, AbstractVariable: libxfce4util4, AbstractVariable: libxfcegui4-4, AbstractVariable: libxfconf-0-2, AbstractVariable: libxine1, AbstractVariable: libxine1-bin, AbstractVariable: libxine1-console, AbstractVariable: libxine1-ffmpeg, AbstractVariable: libxine1-misc-plugins, AbstractVariable: libxine1-x, 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: midori, 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: openssh-server, AbstractVariable: oss-compat, AbstractVariable: oxygen-icon-theme, AbstractVariable: perl-tk, AbstractVariable: perlmagick, AbstractVariable: phonon, AbstractVariable: phonon-backend-gstreamer, AbstractVariable: plasma-scriptengine-javascript, AbstractVariable: psutils, AbstractVariable: pulseaudio, AbstractVariable: pulseaudio-esound-compat, AbstractVariable: pulseaudio-module-x11, AbstractVariable: pulseaudio-utils, AbstractVariable: python-beagle, AbstractVariable: python-cddb, AbstractVariable: python-configobj, AbstractVariable: python-crypto, AbstractVariable: python-gpod, AbstractVariable: python-keybinder, AbstractVariable: python-musicbrainz2, AbstractVariable: python-mutagen, AbstractVariable: python-paramiko, AbstractVariable: python-uno, AbstractVariable: quodlibet, AbstractVariable: quodlibet-ext, AbstractVariable: quodlibet-plugins, AbstractVariable: ratpoison, AbstractVariable: re2c, AbstractVariable: rox-filer, AbstractVariable: roxterm, AbstractVariable: runit, AbstractVariable: rxvt, AbstractVariable: rxvt-ml, AbstractVariable: sbcl, AbstractVariable: scrotwm, AbstractVariable: shared-desktop-ontologies, AbstractVariable: slsh, AbstractVariable: socklog, AbstractVariable: soprano-daemon, AbstractVariable: spamassassin, AbstractVariable: spamc, AbstractVariable: sun-java6-bin, AbstractVariable: sun-java6-jre, AbstractVariable: swordfish-doc, 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-omega, 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-mscorefonts-installer, AbstractVariable: tzdata-java, AbstractVariable: ucspi-unix, AbstractVariable: ude, AbstractVariable: unixodbc, AbstractVariable: util-vserver, AbstractVariable: uwm, AbstractVariable: vcdimager, AbstractVariable: vim-nox, AbstractVariable: virtualbox-ose-guest-source, AbstractVariable: virtualbox-ose-guest-utils, AbstractVariable: virtualbox-ose-guest-x11, AbstractVariable: virtuoso-minimal, AbstractVariable: virtuoso-opensource-6.1-bin, AbstractVariable: virtuoso-opensource-6.1-common, AbstractVariable: vnc4server, AbstractVariable: vzctl, AbstractVariable: vzquota, AbstractVariable: wmii, AbstractVariable: wmii-doc, AbstractVariable: wodim, AbstractVariable: xaw3dg, 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-gl, AbstractVariable: xnest, AbstractVariable: xpdf-common, AbstractVariable: zeroinstall-injector] # starts : 11 # conflicts : 1195 # decisions : 189686 # propagations : 1336086 # inspects : 2726649 # learnt literals : 19 # learnt binary clauses : 104 # learnt ternary clauses : 154 # learnt clauses : 1175 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 275906 # 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) : 195305.65706768015 # non guided choices 33506 # learnt constraints type #Solving done (11.21s). #Solution contains:2030