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:51:09 UTC 2010 #Using input file /home/misc2010/data/2010/easy/randea6106.cudf #Using ouput file /home/misc2010/tmp/201007050905/p2cudf-paranoid-1.6/randea6106.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:2222 #Parsing done (2.222s). #Solving ... #Request size: 1665 #Number of packages after slice: 3094 #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 10468 32871 # Current objective function value: 167337(0.54s) # Current objective function value: 167313(0.79s) # Current objective function value: 167312(1.221s) # Paranoid criteria value: -61, -111 # Proof: [AbstractVariable: apt-listbugs, AbstractVariable: apt-listchanges, AbstractVariable: apt-xapian-index, AbstractVariable: clisp, AbstractVariable: dasher, AbstractVariable: deskbar-applet, AbstractVariable: f-spot, AbstractVariable: gnome-about, AbstractVariable: gnome-accessibility, AbstractVariable: gnome-applets, AbstractVariable: gnome-core, AbstractVariable: gnome-keyring-manager, AbstractVariable: gnome-mag, AbstractVariable: gnome-orca, AbstractVariable: gnome-panel, AbstractVariable: gnome-screensaver, AbstractVariable: gnome-session, AbstractVariable: graphviz, AbstractVariable: gstreamer0.10-plugins-bad, AbstractVariable: gvfs-backends, AbstractVariable: krb5-multidev, AbstractVariable: libcurl-ocaml-dev, AbstractVariable: libcurl4-gnutls-dev, AbstractVariable: libdc1394-22, AbstractVariable: libdpkg-ruby1.8, AbstractVariable: libgettext-ruby1.8, AbstractVariable: libgnome2-perl, AbstractVariable: libgnome2.24-cil, AbstractVariable: libgnomeui-0, AbstractVariable: libgnomeui-common, AbstractVariable: libgvpr1, AbstractVariable: libhttp-access2-ruby1.8, AbstractVariable: libhttpclient-ruby1.8, AbstractVariable: libimobiledevice1, AbstractVariable: libkadm5clnt-mit7, AbstractVariable: libkrb5-dev, AbstractVariable: liblocale-ruby1.8, AbstractVariable: libneon27-gnutls-dev, AbstractVariable: libopenssl-ruby1.8, AbstractVariable: libplist1, AbstractVariable: libpostgresql-ocaml-dev, AbstractVariable: libpq-dev, AbstractVariable: librpm-dev, AbstractVariable: libruby, AbstractVariable: libruby1.8, AbstractVariable: libsigsegv0, AbstractVariable: libuconv-ruby1.8, AbstractVariable: libxml-parser-ruby1.8, AbstractVariable: locales, AbstractVariable: miro, AbstractVariable: python-apt, AbstractVariable: python-gnome2, AbstractVariable: python-gnomeapplet, AbstractVariable: python-pyatspi, AbstractVariable: rhythmbox, AbstractVariable: rhythmbox-plugins, AbstractVariable: ruby, AbstractVariable: ruby1.8, AbstractVariable: vim-addon-manager, AbstractVariable: xchat-gnome, AbstractVariable: xindy, AbstractVariable: apt-listbugs, AbstractVariable: apt-listchanges, AbstractVariable: apt-xapian-index, AbstractVariable: aptitude-doc-fr, AbstractVariable: aspell, AbstractVariable: aspell-am, AbstractVariable: bogofilter, AbstractVariable: bogofilter-common, AbstractVariable: bogofilter-tokyocabinet, AbstractVariable: bzr, AbstractVariable: bzr-upload, AbstractVariable: clisp, AbstractVariable: dasher, AbstractVariable: deskbar-applet, AbstractVariable: distcc, AbstractVariable: emacs22-bin-common, AbstractVariable: emacs22-common, AbstractVariable: emacs22-nox, AbstractVariable: emacsen-common, AbstractVariable: f-spot, AbstractVariable: gnome-about, AbstractVariable: gnome-accessibility, AbstractVariable: gnome-applets, AbstractVariable: gnome-core, AbstractVariable: gnome-keyring-manager, AbstractVariable: gnome-mag, AbstractVariable: gnome-orca, AbstractVariable: gnome-panel, AbstractVariable: gnome-screensaver, AbstractVariable: gnome-session, AbstractVariable: graphviz, AbstractVariable: gstreamer0.10-plugins-bad, AbstractVariable: gvfs-backends, AbstractVariable: hunspell-uz, AbstractVariable: ice33-slice, AbstractVariable: ice33-translators, AbstractVariable: krb5-multidev, AbstractVariable: kwwidgets-examples, AbstractVariable: libaqbanking-data, AbstractVariable: libaqbanking29, AbstractVariable: libaqofxconnect5, AbstractVariable: libcurl-ocaml-dev, AbstractVariable: libcurl4-gnutls-dev, AbstractVariable: libdc1394-22, AbstractVariable: libdpkg-ruby1.8, AbstractVariable: libgettext-ruby1.8, AbstractVariable: libgnome2-perl, AbstractVariable: libgnome2.24-cil, AbstractVariable: libgnomeui-0, AbstractVariable: libgnomeui-common, AbstractVariable: libgvpr1, AbstractVariable: libgwenhywfar47, AbstractVariable: libhttp-access2-ruby1.8, AbstractVariable: libhttpclient-ruby1.8, AbstractVariable: libiceutil33, AbstractVariable: libimobiledevice1, AbstractVariable: libkadm5clnt-mit7, AbstractVariable: libkrb5-dev, AbstractVariable: libllvm2.7, AbstractVariable: liblocale-ruby1.8, AbstractVariable: libmcpp0, AbstractVariable: libneon27-gnutls-dev, AbstractVariable: libopenssl-ruby1.8, AbstractVariable: libplist1, AbstractVariable: libpostgresql-ocaml-dev, AbstractVariable: libpq-dev, AbstractVariable: libqt4-dev, AbstractVariable: libqt4-help, AbstractVariable: libqt4-multimedia, AbstractVariable: libqt4-phonon, AbstractVariable: libqt4-scripttools, AbstractVariable: libqt4-webkit, AbstractVariable: libqt4-xmlpatterns, AbstractVariable: libqtscript4-core, AbstractVariable: libqtscript4-network, AbstractVariable: libqwtplot3d-qt4-0, AbstractVariable: libqwtplot3d-qt4-dev, AbstractVariable: librpm-dev, AbstractVariable: libruby, AbstractVariable: libruby1.8, AbstractVariable: libsigsegv0, AbstractVariable: libslice33, AbstractVariable: libuconv-ruby1.8, AbstractVariable: libxml-parser-ruby1.8, AbstractVariable: libzeroc-ice33, AbstractVariable: llvm-2.7, AbstractVariable: llvm-2.7-dev, AbstractVariable: llvm-2.7-examples, AbstractVariable: llvm-2.7-runtime, AbstractVariable: locales, AbstractVariable: locales-all, AbstractVariable: lxsession, AbstractVariable: miro, AbstractVariable: perlmagick, AbstractVariable: python-apt, AbstractVariable: python-configobj, AbstractVariable: python-django-mumble, AbstractVariable: python-gnome2, AbstractVariable: python-gnomeapplet, AbstractVariable: python-pyatspi, AbstractVariable: python-zeroc-ice, AbstractVariable: qt4-qmake, AbstractVariable: rhythmbox, AbstractVariable: rhythmbox-plugins, AbstractVariable: ruby, AbstractVariable: ruby1.8, AbstractVariable: sbcl, AbstractVariable: slime, AbstractVariable: vim-addon-manager, AbstractVariable: xchat-gnome, AbstractVariable: xindy] # starts : 8 # conflicts : 732 # decisions : 21350 # propagations : 974857 # inspects : 2458691 # learnt literals : 17 # learnt binary clauses : 27 # learnt ternary clauses : 44 # learnt clauses : 714 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 993 # 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) : 2321088.095238095 # non guided choices 7915 # learnt constraints type #Solving done (3.892s). #Solution contains:1610