HEAD is now at 5df24db 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:22:39 UTC 2010 #Using input file /home/misc2010/data/2010/easy/rand61b840.cudf #Using ouput file /home/misc2010/tmp/201007050905/p2cudf-paranoid-1.6/rand61b840.cudf.easy.result #Objective function paranoid #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 721951928 #Max memory 725876736 #Total memory 725876736 #Number of processors 1 #Parsing ... #Time to parse:2871 #Parsing done (2.871s). #Solving ... #Request size: 1665 #Number of packages after slice: 3192 #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 paranoid # p cnf 10638 33543 # Current objective function value: 391009(0.66s) # Current objective function value: 390992(1.11s) # Paranoid criteria value: -140, -252 # Proof: [AbstractVariable: at-spi, AbstractVariable: avidemux, AbstractVariable: avidemux-plugins, AbstractVariable: baobab, AbstractVariable: brasero, AbstractVariable: brasero-common, AbstractVariable: capplets-data, AbstractVariable: cheese, AbstractVariable: cheese-common, AbstractVariable: dasher, AbstractVariable: dasher-data, AbstractVariable: deskbar-applet, AbstractVariable: eog, AbstractVariable: epiphany-browser, AbstractVariable: epiphany-browser-data, AbstractVariable: evince, AbstractVariable: evolution, AbstractVariable: evolution-data-server, AbstractVariable: evolution-webcal, AbstractVariable: f-spot, AbstractVariable: file-roller, AbstractVariable: gconf-editor, AbstractVariable: gconf2, AbstractVariable: gdm3, AbstractVariable: gecko-mediaplayer, AbstractVariable: gedit, AbstractVariable: gksu, AbstractVariable: gnome-about, AbstractVariable: gnome-accessibility, AbstractVariable: gnome-applets, AbstractVariable: gnome-applets-data, AbstractVariable: gnome-bluetooth, AbstractVariable: gnome-control-center, AbstractVariable: gnome-core, AbstractVariable: gnome-dictionary, AbstractVariable: gnome-keyring, AbstractVariable: gnome-keyring-manager, AbstractVariable: gnome-mag, AbstractVariable: gnome-media, AbstractVariable: gnome-media-common, AbstractVariable: gnome-mplayer, AbstractVariable: gnome-netstatus-applet, AbstractVariable: gnome-orca, AbstractVariable: gnome-panel, AbstractVariable: gnome-panel-data, AbstractVariable: gnome-power-manager, AbstractVariable: gnome-screensaver, AbstractVariable: gnome-screenshot, AbstractVariable: gnome-search-tool, AbstractVariable: gnome-session, AbstractVariable: gnome-session-bin, AbstractVariable: gnome-settings-daemon, AbstractVariable: gnome-system-log, AbstractVariable: gnome-system-monitor, AbstractVariable: gnome-terminal, AbstractVariable: gnome-terminal-data, AbstractVariable: gnome-user-guide, AbstractVariable: gnome-utils, AbstractVariable: gok, AbstractVariable: gstreamer0.10-plugins-bad, AbstractVariable: gstreamer0.10-plugins-good, AbstractVariable: gthumb, AbstractVariable: gthumb-data, AbstractVariable: guake, AbstractVariable: imagemagick, AbstractVariable: inkscape, AbstractVariable: krb5-multidev, AbstractVariable: libbonoboui2-0, AbstractVariable: libbrasero-media0, AbstractVariable: libcurl-ocaml-dev, AbstractVariable: libcurl4-gnutls-dev, AbstractVariable: libflac8, AbstractVariable: libgail-gnome-module, AbstractVariable: libgksu2-0, AbstractVariable: libgnome-media0, AbstractVariable: libgnome-vfs2.0-cil, AbstractVariable: libgnome2-0, AbstractVariable: libgnome2-common, AbstractVariable: libgnome2-perl, AbstractVariable: libgnome2-vfs-perl, AbstractVariable: libgnome2.24-cil, AbstractVariable: libgnomekbd-common, AbstractVariable: libgnomekbd4, AbstractVariable: libgnomeui-0, AbstractVariable: libgnomevfs2-0, AbstractVariable: libgnomevfs2-common, AbstractVariable: libgnomevfs2-extra, AbstractVariable: libgweather-common, AbstractVariable: libgweather1, AbstractVariable: libkrb5-dev, AbstractVariable: libmagick++3, AbstractVariable: libmagickcore3, AbstractVariable: libmagickcore3-extra, AbstractVariable: libmagickwand3, AbstractVariable: libmetacity-private0, AbstractVariable: libmysqlclient16, AbstractVariable: libneon27-gnutls-dev, AbstractVariable: libpanel-applet2-0, AbstractVariable: libpostgresql-ocaml-dev, AbstractVariable: libpq-dev, AbstractVariable: libpstoedit0c2a, AbstractVariable: libpulse-mainloop-glib0, AbstractVariable: libpulse0, AbstractVariable: libqt4-sql-mysql, AbstractVariable: librpm-dev, AbstractVariable: libsndfile1, AbstractVariable: libsqlite3-ocaml, AbstractVariable: libsqlite3-ocaml-dev, AbstractVariable: liferea, AbstractVariable: metacity, AbstractVariable: metacity-common, AbstractVariable: metacity-themes, AbstractVariable: miro, AbstractVariable: mousetweaks, AbstractVariable: mplayer, AbstractVariable: mysql-common, AbstractVariable: nautilus, AbstractVariable: nautilus-data, AbstractVariable: notification-daemon, AbstractVariable: obex-data-server, AbstractVariable: openoffice.org-gnome, AbstractVariable: procmail, AbstractVariable: pstoedit, AbstractVariable: purifyeps, AbstractVariable: python-facebook, AbstractVariable: python-gnome2, AbstractVariable: python-gnomeapplet, AbstractVariable: python-pyatspi, AbstractVariable: reportbug, AbstractVariable: rhythmbox, AbstractVariable: rhythmbox-plugins, AbstractVariable: rss-glx, AbstractVariable: synaptic, AbstractVariable: twolame, AbstractVariable: vlc, AbstractVariable: vlc-nox, AbstractVariable: vlc-plugin-pulse, AbstractVariable: xchat-gnome, AbstractVariable: xchat-gnome-common, AbstractVariable: yelp, AbstractVariable: aptitude-doc-fr, AbstractVariable: aspell, AbstractVariable: aspell-am, AbstractVariable: at-spi, AbstractVariable: avidemux, AbstractVariable: avidemux-plugins, AbstractVariable: baobab, AbstractVariable: blt, AbstractVariable: brasero, AbstractVariable: brasero-common, AbstractVariable: capplets-data, AbstractVariable: cheese, AbstractVariable: cheese-common, AbstractVariable: crystalspace-doc, AbstractVariable: dasher, AbstractVariable: dasher-data, AbstractVariable: deskbar-applet, AbstractVariable: eog, AbstractVariable: epiphany-browser, AbstractVariable: epiphany-browser-data, AbstractVariable: erlang-appmon, AbstractVariable: erlang-asn1, AbstractVariable: erlang-base-hipe, AbstractVariable: erlang-common-test, AbstractVariable: erlang-corba, AbstractVariable: erlang-crypto, AbstractVariable: erlang-debugger, AbstractVariable: erlang-dialyzer, AbstractVariable: erlang-docbuilder, AbstractVariable: erlang-edoc, AbstractVariable: erlang-erl-docgen, AbstractVariable: erlang-et, AbstractVariable: erlang-eunit, AbstractVariable: erlang-gs, AbstractVariable: erlang-ic, AbstractVariable: erlang-inets, AbstractVariable: erlang-inviso, AbstractVariable: erlang-megaco, AbstractVariable: erlang-mnesia, AbstractVariable: erlang-nox, AbstractVariable: erlang-observer, AbstractVariable: erlang-odbc, AbstractVariable: erlang-os-mon, AbstractVariable: erlang-parsetools, AbstractVariable: erlang-percept, AbstractVariable: erlang-pman, AbstractVariable: erlang-public-key, AbstractVariable: erlang-reltool, AbstractVariable: erlang-runtime-tools, AbstractVariable: erlang-snmp, AbstractVariable: erlang-ssh, AbstractVariable: erlang-ssl, AbstractVariable: erlang-syntax-tools, AbstractVariable: erlang-test-server, AbstractVariable: erlang-toolbar, AbstractVariable: erlang-tools, AbstractVariable: erlang-tv, AbstractVariable: erlang-typer, AbstractVariable: erlang-webtool, AbstractVariable: erlang-wx, AbstractVariable: erlang-x11, AbstractVariable: erlang-xmerl, AbstractVariable: evince, AbstractVariable: evince-gtk, AbstractVariable: evolution, AbstractVariable: evolution-data-server, AbstractVariable: evolution-webcal, AbstractVariable: f-spot, AbstractVariable: file-roller, AbstractVariable: gconf-editor, AbstractVariable: gconf2, AbstractVariable: gdm3, AbstractVariable: gecko-mediaplayer, AbstractVariable: gedit, AbstractVariable: gksu, AbstractVariable: gnome-about, AbstractVariable: gnome-accessibility, AbstractVariable: gnome-applets, AbstractVariable: gnome-applets-data, AbstractVariable: gnome-bluetooth, AbstractVariable: gnome-control-center, AbstractVariable: gnome-core, AbstractVariable: gnome-dictionary, AbstractVariable: gnome-keyring, AbstractVariable: gnome-keyring-manager, AbstractVariable: gnome-mag, AbstractVariable: gnome-media, AbstractVariable: gnome-media-common, AbstractVariable: gnome-mplayer, AbstractVariable: gnome-netstatus-applet, AbstractVariable: gnome-orca, AbstractVariable: gnome-panel, AbstractVariable: gnome-panel-data, AbstractVariable: gnome-power-manager, AbstractVariable: gnome-screensaver, AbstractVariable: gnome-screenshot, AbstractVariable: gnome-search-tool, AbstractVariable: gnome-session, AbstractVariable: gnome-session-bin, AbstractVariable: gnome-settings-daemon, AbstractVariable: gnome-system-log, AbstractVariable: gnome-system-monitor, AbstractVariable: gnome-terminal, AbstractVariable: gnome-terminal-data, AbstractVariable: gnome-user-guide, AbstractVariable: gnome-utils, AbstractVariable: gnugo, AbstractVariable: gok, AbstractVariable: gstreamer0.10-plugins-bad, AbstractVariable: gstreamer0.10-plugins-good, AbstractVariable: gthumb, AbstractVariable: gthumb-data, AbstractVariable: guake, AbstractVariable: heimdal-dev, AbstractVariable: heimdal-multidev, AbstractVariable: idle-python2.5, AbstractVariable: imagemagick, AbstractVariable: inkscape, AbstractVariable: krb5-multidev, AbstractVariable: libasn1-8-heimdal, AbstractVariable: libaudio-dev, AbstractVariable: libbonoboui2-0, AbstractVariable: libbrasero-media0, AbstractVariable: libcups2-dev, AbstractVariable: libcurl-ocaml-dev, AbstractVariable: libcurl4-gnutls-dev, AbstractVariable: libflac8, AbstractVariable: libfontconfig1-dev, AbstractVariable: libfreetype6-dev, AbstractVariable: libgail-gnome-module, AbstractVariable: libgksu2-0, AbstractVariable: libgl1-mesa-dev, AbstractVariable: libglu1-mesa-dev, AbstractVariable: libgnome-media0, AbstractVariable: libgnome-vfs2.0-cil, AbstractVariable: libgnome2-0, AbstractVariable: libgnome2-common, AbstractVariable: libgnome2-perl, AbstractVariable: libgnome2-vfs-perl, AbstractVariable: libgnome2.24-cil, AbstractVariable: libgnomekbd-common, AbstractVariable: libgnomekbd4, AbstractVariable: libgnomeui-0, AbstractVariable: libgnomevfs2-0, AbstractVariable: libgnomevfs2-common, AbstractVariable: libgnomevfs2-extra, AbstractVariable: libgssapi2-heimdal, AbstractVariable: libgweather-common, AbstractVariable: libgweather1, AbstractVariable: libhdb9-heimdal, AbstractVariable: libheimntlm0-heimdal, AbstractVariable: libhx509-5-heimdal, AbstractVariable: libice-dev, AbstractVariable: libjpeg62-dev, AbstractVariable: libkadm5clnt7-heimdal, AbstractVariable: libkadm5srv8-heimdal, AbstractVariable: libkafs0-heimdal, AbstractVariable: libkrb5-26-heimdal, AbstractVariable: libkrb5-dev, AbstractVariable: liblcms1-dev, AbstractVariable: liblwt-ocaml-doc, AbstractVariable: libmagick++3, AbstractVariable: libmagickcore3, AbstractVariable: libmagickcore3-extra, AbstractVariable: libmagickwand3, AbstractVariable: libmath-calc-units-perl, AbstractVariable: libmetacity-private0, AbstractVariable: libmng-dev, AbstractVariable: libmysqlclient16, AbstractVariable: libneon27-gnutls-dev, AbstractVariable: libpanel-applet2-0, AbstractVariable: libpng12-dev, AbstractVariable: libpostgresql-ocaml-dev, AbstractVariable: libpq-dev, AbstractVariable: libpstoedit0c2a, AbstractVariable: libpulse-mainloop-glib0, AbstractVariable: libpulse0, AbstractVariable: libpyside0.3, AbstractVariable: libqglviewer-dev, AbstractVariable: libqglviewer-dev-common, AbstractVariable: libqglviewer-qt3-2, AbstractVariable: libqglviewer-qt3-dev, AbstractVariable: libqt3-headers, AbstractVariable: libqt3-mt, AbstractVariable: libqt3-mt-dev, AbstractVariable: libqt4-sql-mysql, AbstractVariable: libqt4-sql-odbc, AbstractVariable: libroken18-heimdal, AbstractVariable: librpm-dev, AbstractVariable: libset-infinite-perl, AbstractVariable: libshiboken0.3, AbstractVariable: libsm-dev, AbstractVariable: libsndfile1, AbstractVariable: libsqlite3-ocaml, AbstractVariable: libsqlite3-ocaml-dev, AbstractVariable: libwind0-heimdal, AbstractVariable: libxcursor-dev, AbstractVariable: libxext-dev, AbstractVariable: libxfixes-dev, AbstractVariable: libxft-dev, AbstractVariable: libxi-dev, AbstractVariable: libxinerama-dev, AbstractVariable: libxmu-dev, AbstractVariable: libxmu-headers, AbstractVariable: libxrandr-dev, AbstractVariable: libxrender-dev, AbstractVariable: libxt-dev, AbstractVariable: liferea, AbstractVariable: mesa-common-dev, AbstractVariable: metacity, AbstractVariable: metacity-common, AbstractVariable: metacity-themes, AbstractVariable: miro, AbstractVariable: mousetweaks, AbstractVariable: mplayer, AbstractVariable: mysql-common, AbstractVariable: nautilus, AbstractVariable: nautilus-data, AbstractVariable: notification-daemon, AbstractVariable: notify-osd, AbstractVariable: obex-data-server, AbstractVariable: odbcinst, AbstractVariable: odbcinst1debian2, AbstractVariable: openoffice.org-gnome, AbstractVariable: procmail, AbstractVariable: pstoedit, AbstractVariable: purifyeps, AbstractVariable: python-facebook, AbstractVariable: python-gnome2, AbstractVariable: python-gnomeapplet, AbstractVariable: python-pyatspi, AbstractVariable: python-pyside.qtopengl, AbstractVariable: python-tk, AbstractVariable: qt3-dev-tools, AbstractVariable: reportbug, AbstractVariable: rhythmbox, AbstractVariable: rhythmbox-plugins, AbstractVariable: rss-glx, AbstractVariable: synaptic, AbstractVariable: twolame, AbstractVariable: unixodbc, AbstractVariable: vlc, AbstractVariable: vlc-nox, AbstractVariable: vlc-plugin-pulse, AbstractVariable: x11proto-fixes-dev, AbstractVariable: x11proto-randr-dev, AbstractVariable: x11proto-render-dev, AbstractVariable: x11proto-xext-dev, AbstractVariable: x11proto-xinerama-dev, AbstractVariable: xchat-gnome, AbstractVariable: xchat-gnome-common, AbstractVariable: yelp] # starts : 5 # conflicts : 358 # decisions : 24092 # propagations : 467904 # inspects : 1178964 # learnt literals : 79 # learnt binary clauses : 52 # learnt ternary clauses : 22 # learnt clauses : 278 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 112 # 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) : 1114057.142857143 # non guided choices 5265 # learnt constraints type #Solving done (4.134s). #Solution contains:1593