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:20:34 UTC 2010 #Using input file /home/misc2010/data/2010/easy/rand5c1800.cudf #Using ouput file /home/misc2010/tmp/201007050905/p2cudf-paranoid-1.6/rand5c1800.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:2377 #Parsing done (2.377s). #Solving ... #Request size: 1665 #Number of packages after slice: 3064 #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 paranoid # p cnf 10404 32596 # Current objective function value: 138411(0.6s) # Current objective function value: 138393(0.84s) # Current objective function value: 138387(0.9s) # Paranoid criteria value: -51, -75 # Proof: [AbstractVariable: avidemux, AbstractVariable: avidemux-plugins, AbstractVariable: brasero, AbstractVariable: cheese, AbstractVariable: chromium-browser, AbstractVariable: deskbar-applet, AbstractVariable: evolution, AbstractVariable: evolution-data-server, AbstractVariable: evolution-plugins, AbstractVariable: gecko-mediaplayer, AbstractVariable: gitk, AbstractVariable: gnome-accessibility, AbstractVariable: gnome-applets, AbstractVariable: gnome-control-center, AbstractVariable: gnome-core, AbstractVariable: gnome-media, AbstractVariable: gnome-mplayer, AbstractVariable: gnome-panel, AbstractVariable: gnome-screensaver, AbstractVariable: gnome-session, AbstractVariable: gstreamer0.10-ffmpeg, AbstractVariable: gstreamer0.10-plugins-bad, AbstractVariable: gstreamer0.10-plugins-base, AbstractVariable: gstreamer0.10-plugins-good, AbstractVariable: libavcodec52, AbstractVariable: libavformat52, AbstractVariable: libebook1.2-9, AbstractVariable: libedata-book1.2-2, AbstractVariable: libedataserverui1.2-8, AbstractVariable: libevolution, AbstractVariable: libjack0, AbstractVariable: libmjpegtools-1.9, AbstractVariable: libquicktime1, AbstractVariable: libshout3, AbstractVariable: libtheora0, AbstractVariable: liferea, AbstractVariable: liferea-data, AbstractVariable: media-player-info, AbstractVariable: miro, AbstractVariable: mjpegtools, AbstractVariable: mplayer, AbstractVariable: openoffice.org-evolution, AbstractVariable: patchutils, AbstractVariable: rhythmbox, AbstractVariable: rhythmbox-plugins, AbstractVariable: tasksel, AbstractVariable: tasksel-data, AbstractVariable: vlc, AbstractVariable: vlc-nox, AbstractVariable: vlc-plugin-pulse, AbstractVariable: xserver-xorg-input-kbd, AbstractVariable: aptitude-doc-ja, AbstractVariable: aspell, AbstractVariable: aspell-uz, AbstractVariable: avidemux, AbstractVariable: avidemux-plugins, AbstractVariable: brasero, AbstractVariable: cheese, AbstractVariable: chromium-browser, AbstractVariable: colorcode, AbstractVariable: compiz-core, AbstractVariable: debian-reference-common, AbstractVariable: debian-reference-de, AbstractVariable: deskbar-applet, AbstractVariable: evolution, AbstractVariable: evolution-data-server, AbstractVariable: evolution-plugins, AbstractVariable: gearman-tools, AbstractVariable: gecko-mediaplayer, AbstractVariable: gitk, AbstractVariable: gnome-accessibility, AbstractVariable: gnome-applets, AbstractVariable: gnome-control-center, AbstractVariable: gnome-core, AbstractVariable: gnome-media, AbstractVariable: gnome-mplayer, AbstractVariable: gnome-panel, AbstractVariable: gnome-screensaver, AbstractVariable: gnome-session, AbstractVariable: gstreamer0.10-ffmpeg, AbstractVariable: gstreamer0.10-plugins-bad, AbstractVariable: gstreamer0.10-plugins-base, AbstractVariable: gstreamer0.10-plugins-good, AbstractVariable: irssi, AbstractVariable: irssi-dev, AbstractVariable: libavcodec52, AbstractVariable: libavformat52, AbstractVariable: libcompizconfig0, AbstractVariable: libebook1.2-9, AbstractVariable: libedata-book1.2-2, AbstractVariable: libedataserverui1.2-8, AbstractVariable: libevolution, AbstractVariable: libgearman4, AbstractVariable: libjack0, AbstractVariable: libmjpegtools-1.9, AbstractVariable: libnjb-cil, AbstractVariable: libnjb5, AbstractVariable: libproc-dev, AbstractVariable: libquicktime1, AbstractVariable: libshout3, AbstractVariable: libtheora0, AbstractVariable: libxfontp1, AbstractVariable: liferea, AbstractVariable: liferea-data, AbstractVariable: loadmeter, AbstractVariable: lxsession, AbstractVariable: media-player-info, AbstractVariable: mesa-utils, AbstractVariable: miro, AbstractVariable: mjpegtools, AbstractVariable: mplayer, AbstractVariable: openoffice.org-evolution, AbstractVariable: os-prober, AbstractVariable: patchutils, AbstractVariable: perlmagick, AbstractVariable: rhythmbox, AbstractVariable: rhythmbox-plugins, AbstractVariable: tasksel, AbstractVariable: tasksel-data, AbstractVariable: vlc, AbstractVariable: vlc-nox, AbstractVariable: vlc-plugin-pulse, AbstractVariable: wmanx, AbstractVariable: xprint, AbstractVariable: xprint-common, AbstractVariable: xserver-xorg-input-kbd] # starts : 4 # conflicts : 52 # decisions : 17864 # propagations : 86702 # inspects : 197650 # learnt literals : 3 # learnt binary clauses : 7 # learnt ternary clauses : 15 # learnt clauses : 48 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 36 # 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) : 722516.6666666667 # non guided choices 7968 # learnt constraints type #Solving done (3.314s). #Solution contains:1593