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:29:38 UTC 2010 #Using input file /home/misc2010/data/2010/easy/rand7fec8c.cudf #Using ouput file /home/misc2010/tmp/201007050905/p2cudf-paranoid-1.6/rand7fec8c.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:2587 #Parsing done (2.587s). #Solving ... #Request size: 1665 #Number of packages after slice: 3073 #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@1bfc93a # 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 10410 32667 # Current objective function value: 81619(0.66s) # Current objective function value: 81616(0.91s) # Paranoid criteria value: -30, -76 # Proof: [AbstractVariable: cron, AbstractVariable: deluge, AbstractVariable: deluge-common, AbstractVariable: deluge-gtk, AbstractVariable: deskbar-applet, AbstractVariable: epiphany-browser, AbstractVariable: gammu, AbstractVariable: gir1.0-gstreamer-0.10, AbstractVariable: gstreamer0.10-plugins-bad, AbstractVariable: javascript-common, AbstractVariable: libmimic0, AbstractVariable: libofa0, AbstractVariable: libseed0, AbstractVariable: lmodern, AbstractVariable: miro, AbstractVariable: ntfsprogs, AbstractVariable: postr, AbstractVariable: prosper, AbstractVariable: python-twisted-core, AbstractVariable: python-twisted-web, AbstractVariable: python-wnck, AbstractVariable: wwwconfig-common, AbstractVariable: x-ttcidfont-conf, AbstractVariable: xfonts-100dpi, AbstractVariable: xfonts-75dpi, AbstractVariable: xfonts-base, AbstractVariable: xfonts-mathml, AbstractVariable: xfonts-scalable, AbstractVariable: xfonts-utils, AbstractVariable: xorg, AbstractVariable: aptitude-doc-ja, AbstractVariable: aspell, AbstractVariable: aspell-uz, AbstractVariable: bcron, AbstractVariable: bcron-run, AbstractVariable: bogofilter, AbstractVariable: bogofilter-common, AbstractVariable: bogofilter-tokyocabinet, AbstractVariable: cron, AbstractVariable: deluge, AbstractVariable: deluge-common, AbstractVariable: deluge-gtk, AbstractVariable: deroff, AbstractVariable: deskbar-applet, AbstractVariable: epiphany-browser, AbstractVariable: gammu, AbstractVariable: gir1.0-gstreamer-0.10, AbstractVariable: gnome-art, AbstractVariable: gnome-splashscreen-manager, AbstractVariable: gstreamer0.10-plugins-bad, AbstractVariable: icedove, AbstractVariable: icedove-l10n-tr, AbstractVariable: javascript-common, AbstractVariable: libart2-ruby1.8, AbstractVariable: libatk1-ruby1.8, AbstractVariable: libbg1, AbstractVariable: libcairo-ruby1.8, AbstractVariable: libcdk5, AbstractVariable: libcdk5-dev, AbstractVariable: libdcerpc0, AbstractVariable: libgconf2-ruby, AbstractVariable: libgconf2-ruby1.8, AbstractVariable: libgdk-pixbuf2-ruby1.8, AbstractVariable: libglade2-ruby, AbstractVariable: libglade2-ruby1.8, AbstractVariable: libglib2-ruby1.8, AbstractVariable: libgnome2-ruby, AbstractVariable: libgnome2-ruby1.8, AbstractVariable: libgnomecanvas2-ruby1.8, AbstractVariable: libgtk2-ruby1.8, AbstractVariable: libibverbs1, AbstractVariable: libldb0, AbstractVariable: libmapi0, AbstractVariable: libmapiproxy-dev, AbstractVariable: libmapiproxy0, AbstractVariable: libmimic0, AbstractVariable: libmlx4-1, AbstractVariable: libofa0, AbstractVariable: libpango1-ruby1.8, AbstractVariable: libpotrace-dev, AbstractVariable: libpotrace0, AbstractVariable: libseed0, AbstractVariable: libtevent0, AbstractVariable: lmodern, AbstractVariable: madbomber-data, AbstractVariable: miro, AbstractVariable: ntfsprogs, AbstractVariable: perlmagick, AbstractVariable: postr, AbstractVariable: prosper, AbstractVariable: python-twisted-core, AbstractVariable: python-twisted-web, AbstractVariable: python-wnck, AbstractVariable: runit, AbstractVariable: ucspi-unix, AbstractVariable: wwwconfig-common, AbstractVariable: x-ttcidfont-conf, AbstractVariable: xfonts-100dpi, AbstractVariable: xfonts-75dpi, AbstractVariable: xfonts-base, AbstractVariable: xfonts-mathml, AbstractVariable: xfonts-scalable, AbstractVariable: xfonts-utils, AbstractVariable: xmms2-core, AbstractVariable: xmms2-plugin-mad, AbstractVariable: xorg] # starts : 3 # conflicts : 72 # decisions : 15791 # propagations : 133074 # inspects : 322764 # learnt literals : 7 # learnt binary clauses : 4 # learnt ternary clauses : 2 # learnt clauses : 64 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 38 # 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) : 739300.0 # non guided choices 5315 # learnt constraints type #Solving done (4.074s). #Solution contains:1637