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:15:52 UTC 2010 #Using input file /home/misc2010/data/2010/easy/rand359ca0.cudf #Using ouput file /home/misc2010/tmp/201007050905/p2cudf-paranoid-1.6/rand359ca0.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:2641 #Parsing done (2.641s). #Solving ... #Request size: 1665 #Number of packages after slice: 3110 #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 10499 32964 # Current objective function value: 85386(0.66s) # Current objective function value: 85385(1.09s) # Paranoid criteria value: -31, -73 # Proof: [AbstractVariable: apt-listbugs, AbstractVariable: apt-listchanges, AbstractVariable: apt-utils, AbstractVariable: apt-xapian-index, AbstractVariable: avahi-daemon, AbstractVariable: cl-asdf, AbstractVariable: clisp, AbstractVariable: common-lisp-controller, AbstractVariable: gnome-accessibility, AbstractVariable: gnome-orca, AbstractVariable: libapt-pkg-dev, AbstractVariable: libexpat-ocaml-dev, AbstractVariable: libexpat1-dev, AbstractVariable: libfam0, AbstractVariable: libgail-gnome-module, AbstractVariable: libgettext-ruby1.8, AbstractVariable: liblocale-ruby1.8, AbstractVariable: libnss-mdns, AbstractVariable: libpthread-stubs0-dev, AbstractVariable: libqt4-designer, AbstractVariable: libqt4-gui, AbstractVariable: libqt4-qt3support, AbstractVariable: libx11-dev, AbstractVariable: libxcb1-dev, AbstractVariable: ocaml, AbstractVariable: openoffice.org-help-en-us, AbstractVariable: python-apt, AbstractVariable: qt4-qtconfig, AbstractVariable: realpath, AbstractVariable: skype, AbstractVariable: synaptic, AbstractVariable: apt-listbugs, AbstractVariable: apt-listchanges, AbstractVariable: apt-utils, AbstractVariable: apt-xapian-index, AbstractVariable: aptitude-doc-fr, AbstractVariable: aspell, AbstractVariable: aspell-ca, AbstractVariable: asterisk-prompt-fr-armelle, AbstractVariable: avahi-daemon, AbstractVariable: bogofilter, AbstractVariable: bogofilter-common, AbstractVariable: bogofilter-tokyocabinet, AbstractVariable: calamaris, AbstractVariable: cl-asdf, AbstractVariable: clisp, AbstractVariable: common-lisp-controller, AbstractVariable: gamin, AbstractVariable: gimp-resynthesizer, AbstractVariable: gnome-accessibility, AbstractVariable: gnome-orca, AbstractVariable: gnome-theme-gilouche, AbstractVariable: google-gadgets-common, AbstractVariable: google-gadgets-gst, AbstractVariable: libalgorithm-c3-perl, AbstractVariable: libapt-pkg-dev, AbstractVariable: libcapture-tiny-perl, AbstractVariable: libclass-c3-perl, AbstractVariable: libclass-mop-perl, AbstractVariable: libdata-optlist-perl, AbstractVariable: libdevel-globaldestruction-perl, AbstractVariable: libdevel-stacktrace-perl, AbstractVariable: libemail-abstract-perl, AbstractVariable: libemail-address-perl, AbstractVariable: libemail-date-format-perl, AbstractVariable: libemail-sender-perl, AbstractVariable: libemail-simple-perl, AbstractVariable: libethos-1.0-0, AbstractVariable: libexpat-ocaml-dev, AbstractVariable: libexpat1-dev, AbstractVariable: libfam0, AbstractVariable: libgail-gnome-module, AbstractVariable: libgamin0, AbstractVariable: libgettext-ruby1.8, AbstractVariable: libggadget-1.0-0b, AbstractVariable: liblocale-ruby1.8, AbstractVariable: libmoose-perl, AbstractVariable: libmro-compat-perl, AbstractVariable: libnss-mdns, AbstractVariable: libparams-util-perl, AbstractVariable: libpthread-stubs0-dev, AbstractVariable: libqt4-designer, AbstractVariable: libqt4-gui, AbstractVariable: libqt4-qt3support, AbstractVariable: librpc-xml-perl, AbstractVariable: libscope-guard-perl, AbstractVariable: libsub-exporter-perl, AbstractVariable: libsub-install-perl, AbstractVariable: libthrowable-perl, AbstractVariable: libtry-tiny-perl, AbstractVariable: libx11-dev, AbstractVariable: libxcb1-dev, AbstractVariable: ocaml, AbstractVariable: openoffice.org-help-en-us, AbstractVariable: perlmagick, AbstractVariable: php-simpletest, AbstractVariable: pktstat, AbstractVariable: python-apt, AbstractVariable: qt4-qtconfig, AbstractVariable: realpath, AbstractVariable: skype, AbstractVariable: synaptic, AbstractVariable: tango-icon-theme, AbstractVariable: xindy] # starts : 3 # conflicts : 99 # decisions : 14314 # propagations : 161590 # inspects : 376397 # learnt literals : 10 # learnt binary clauses : 8 # learnt ternary clauses : 10 # learnt clauses : 88 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 116 # 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) : 897722.2222222222 # non guided choices 5356 # learnt constraints type #Solving done (3.95s). #Solution contains:1631