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:26:34 UTC 2010 #Using input file /home/misc2010/data/2010/easy/rand6d933e.cudf #Using ouput file /home/misc2010/tmp/201007050905/p2cudf-paranoid-1.6/rand6d933e.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:2582 #Parsing done (2.582s). #Solving ... #Request size: 1665 #Number of packages after slice: 3080 #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@763f5d # 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 10435 32667 # Current objective function value: 158450(0.88s) # Current objective function value: 158435(1.122s) # Paranoid criteria value: -58, -95 # Proof: [AbstractVariable: cheese, AbstractVariable: chromium-browser, AbstractVariable: dasher, AbstractVariable: deskbar-applet, AbstractVariable: epiphany-browser, AbstractVariable: equivs, AbstractVariable: evolution, AbstractVariable: evolution-data-server, AbstractVariable: f-spot, AbstractVariable: fakeroot, AbstractVariable: gecko-mediaplayer, AbstractVariable: gnome-about, AbstractVariable: gnome-accessibility, AbstractVariable: gnome-applets, AbstractVariable: gnome-core, AbstractVariable: gnome-keyring-manager, AbstractVariable: gnome-mag, AbstractVariable: gnome-media, AbstractVariable: gnome-mplayer, AbstractVariable: gnome-orca, AbstractVariable: gnome-panel, AbstractVariable: gnome-screensaver, AbstractVariable: gnome-session, AbstractVariable: gstreamer0.10-ffmpeg, AbstractVariable: gstreamer0.10-plugins-bad, AbstractVariable: gstreamer0.10-plugins-good, AbstractVariable: gthumb, AbstractVariable: gvfs-backends, AbstractVariable: hp-ppd, AbstractVariable: libavcodec52, AbstractVariable: libavformat52, AbstractVariable: libglade2.0-cil, AbstractVariable: libgnome2-perl, AbstractVariable: libgnome2.24-cil, AbstractVariable: libgnomeui-0, AbstractVariable: libgnomeui-common, AbstractVariable: libgtk2.0-cil, AbstractVariable: libgweather1, AbstractVariable: libmjpegtools-1.9, AbstractVariable: libmono-addins-gui0.2-cil, AbstractVariable: libquicktime1, AbstractVariable: libschroedinger-1.0-0, AbstractVariable: libsoup-gnome2.4-1, AbstractVariable: miro, AbstractVariable: mjpegtools, AbstractVariable: mplayer, AbstractVariable: netpbm, AbstractVariable: ntfs-3g, AbstractVariable: openoffice.org-gnome, AbstractVariable: python-gnome2, AbstractVariable: python-gnomeapplet, AbstractVariable: python-pyatspi, AbstractVariable: rhythmbox, AbstractVariable: rhythmbox-plugins, AbstractVariable: vlc, AbstractVariable: vlc-nox, AbstractVariable: vlc-plugin-pulse, AbstractVariable: xchat-gnome, AbstractVariable: ant-gcj, AbstractVariable: ant1.7, AbstractVariable: ant1.7-optional, AbstractVariable: ant1.7-optional-gcj, AbstractVariable: aptitude-doc-ja, AbstractVariable: aspell, AbstractVariable: aspell-uz, AbstractVariable: calendar-timezones, AbstractVariable: cheese, AbstractVariable: chromium-browser, AbstractVariable: dash, AbstractVariable: dasher, AbstractVariable: deskbar-applet, AbstractVariable: epiphany-browser, AbstractVariable: equivs, AbstractVariable: evolution, AbstractVariable: evolution-data-server, AbstractVariable: f-spot, AbstractVariable: fakeroot, AbstractVariable: freetds-common, AbstractVariable: gecko-mediaplayer, AbstractVariable: gnome-about, AbstractVariable: gnome-accessibility, AbstractVariable: gnome-applets, AbstractVariable: gnome-core, AbstractVariable: gnome-keyring-manager, AbstractVariable: gnome-mag, AbstractVariable: gnome-media, AbstractVariable: gnome-mplayer, AbstractVariable: gnome-orca, AbstractVariable: gnome-panel, AbstractVariable: gnome-screensaver, AbstractVariable: gnome-session, AbstractVariable: gstreamer0.10-ffmpeg, AbstractVariable: gstreamer0.10-plugins-bad, AbstractVariable: gstreamer0.10-plugins-good, AbstractVariable: gthumb, AbstractVariable: gvfs-backends, AbstractVariable: hp-ppd, AbstractVariable: iceowl, AbstractVariable: iceowl-l10n-sk, AbstractVariable: libaprutil1-dbd-freetds, AbstractVariable: libavcodec52, AbstractVariable: libavformat52, AbstractVariable: libcgi-extratags-perl, AbstractVariable: libcppunit-1.12-1, AbstractVariable: libglade2.0-cil, AbstractVariable: libgnome2-perl, AbstractVariable: libgnome2.24-cil, AbstractVariable: libgnomeui-0, AbstractVariable: libgnomeui-common, AbstractVariable: libgtk2.0-cil, AbstractVariable: libgweather1, AbstractVariable: libibverbs1, AbstractVariable: libldb0, AbstractVariable: liblwp2, AbstractVariable: libmath-random-oo-perl, AbstractVariable: libmjpegtools-1.9, AbstractVariable: libmono-addins-gui0.2-cil, AbstractVariable: libmusic-dev, AbstractVariable: libmusic1, AbstractVariable: libnuma1, AbstractVariable: libopenmpi1.3, AbstractVariable: libparams-validate-perl, AbstractVariable: libquicktime1, AbstractVariable: librvm-dev, AbstractVariable: librvm1, AbstractVariable: libschroedinger-1.0-0, AbstractVariable: libsoup-gnome2.4-1, AbstractVariable: libsp-gxmlcpp1, AbstractVariable: libsybdb5, AbstractVariable: libtest-mockrandom-perl, AbstractVariable: libtest-number-delta-perl, AbstractVariable: libtevent0, AbstractVariable: libxerces2-java, AbstractVariable: lxsession, AbstractVariable: miro, AbstractVariable: mjpegtools, AbstractVariable: mplayer, AbstractVariable: netpbm, AbstractVariable: ntfs-3g, AbstractVariable: openoffice.org-gnome, AbstractVariable: perlmagick, AbstractVariable: python-gnome2, AbstractVariable: python-gnomeapplet, AbstractVariable: python-pyatspi, AbstractVariable: rhythmbox, AbstractVariable: rhythmbox-plugins, AbstractVariable: samba4-common-bin, AbstractVariable: samba4-testsuite, AbstractVariable: vlc, AbstractVariable: vlc-nox, AbstractVariable: vlc-plugin-pulse, AbstractVariable: wide-dhcpv6-relay, AbstractVariable: xchat-gnome] # starts : 3 # conflicts : 102 # decisions : 11753 # propagations : 121085 # inspects : 271254 # learnt literals : 2 # learnt binary clauses : 3 # learnt ternary clauses : 5 # learnt clauses : 99 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 43 # 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) : 484340.0 # non guided choices 5264 # learnt constraints type #Solving done (3.616s). #Solution contains:1599