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:05:25 UTC 2010 #Using input file /home/misc2010/data/2010/easy/rand08759d.cudf #Using ouput file /home/misc2010/tmp/201007050905/p2cudf-paranoid-1.6/rand08759d.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:2228 #Parsing done (2.228s). #Solving ... #Request size: 1665 #Number of packages after slice: 3074 #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 10424 32632 # Current objective function value: 73664(0.541s) # Paranoid criteria value: -27, -116 # Proof: [AbstractVariable: apt-file, AbstractVariable: dasher, AbstractVariable: debtree, AbstractVariable: espeak, AbstractVariable: freepats, AbstractVariable: gnome-accessibility, AbstractVariable: gnome-orca, AbstractVariable: gok, AbstractVariable: libapt-pkg-perl, AbstractVariable: libespeak1, AbstractVariable: libgnome-speech7, AbstractVariable: libportaudio2, AbstractVariable: lintian, AbstractVariable: linux-base, AbstractVariable: linux-image-2.6.32-4-amd64, AbstractVariable: linux-image-2.6.32-5-amd64, AbstractVariable: linux-image-amd64, AbstractVariable: locales, AbstractVariable: metacity, AbstractVariable: metacity-themes, AbstractVariable: openoffice.org, AbstractVariable: openssh-blacklist-extra, AbstractVariable: openssl-blacklist, AbstractVariable: openvpn, AbstractVariable: smbfs, AbstractVariable: tp-smapi-modules-2.6.32-4-amd64, AbstractVariable: tp-smapi-modules-2.6.32-5-amd64, AbstractVariable: apt-file, AbstractVariable: aptitude-doc-en, AbstractVariable: aspell, AbstractVariable: aspell-eo, AbstractVariable: bogofilter, AbstractVariable: bogofilter-common, AbstractVariable: bogofilter-tokyocabinet, AbstractVariable: cdd-doc, AbstractVariable: dasher, AbstractVariable: debtree, AbstractVariable: espeak, AbstractVariable: famfamfam-flag-png, AbstractVariable: freedm, AbstractVariable: freepats, AbstractVariable: gnome-accessibility, AbstractVariable: gnome-orca, AbstractVariable: gok, AbstractVariable: kbattleship, AbstractVariable: kdebase-runtime, AbstractVariable: kdebase-runtime-data, AbstractVariable: kdelibs-bin, AbstractVariable: kdelibs5-data, AbstractVariable: kdelibs5-plugins, AbstractVariable: kdoctools, AbstractVariable: libalgorithm-c3-perl, AbstractVariable: libapt-pkg-perl, AbstractVariable: libattica0, AbstractVariable: libclass-c3-perl, AbstractVariable: libclucene0ldbl, AbstractVariable: libdata-optlist-perl, AbstractVariable: libdata-section-perl, AbstractVariable: libespeak1, AbstractVariable: libgcj-doc, AbstractVariable: libgnome-speech7, AbstractVariable: libiodbc2, AbstractVariable: libkde3support4, AbstractVariable: libkdecore5, AbstractVariable: libkdegames5, AbstractVariable: libkdesu5, AbstractVariable: libkdeui5, AbstractVariable: libkdnssd4, AbstractVariable: libkfile4, AbstractVariable: libkhtml5, AbstractVariable: libkio5, AbstractVariable: libkjsapi4, AbstractVariable: libkjsembed4, AbstractVariable: libkmediaplayer4, AbstractVariable: libknewstuff2-4, AbstractVariable: libknewstuff3-4, AbstractVariable: libknotifyconfig4, AbstractVariable: libkntlm4, AbstractVariable: libkparts4, AbstractVariable: libkpty4, AbstractVariable: libkrosscore4, AbstractVariable: libktexteditor4, AbstractVariable: libkutils4, AbstractVariable: libladr4, AbstractVariable: libmro-compat-perl, AbstractVariable: libmutter-private0, AbstractVariable: libnepomuk4, AbstractVariable: libnepomukquery4a, AbstractVariable: libparams-util-perl, AbstractVariable: libphonon4, AbstractVariable: libplasma3, AbstractVariable: libpolkit-qt-1-0, AbstractVariable: libportaudio2, AbstractVariable: libqca2, AbstractVariable: libqt4-webkit, AbstractVariable: libqt4-xmlpatterns, AbstractVariable: libsdl-net1.2, AbstractVariable: libsoftware-license-perl, AbstractVariable: libsolid4, AbstractVariable: libsoprano4, AbstractVariable: libssh-4, AbstractVariable: libstreamanalyzer0, AbstractVariable: libstreams0, AbstractVariable: libsub-exporter-perl, AbstractVariable: libsub-install-perl, AbstractVariable: libtext-template-perl, AbstractVariable: libthreadweaver4, AbstractVariable: libwxbase2.6-0, AbstractVariable: libwxgtk2.6-0, AbstractVariable: libxmlunit-java-doc, AbstractVariable: lintian, AbstractVariable: linux-base, AbstractVariable: linux-image-2.6.32-4-amd64, AbstractVariable: linux-image-2.6.32-5-amd64, AbstractVariable: linux-image-amd64, AbstractVariable: locales, AbstractVariable: locales-all, AbstractVariable: metacity, AbstractVariable: metacity-themes, AbstractVariable: mutter, AbstractVariable: mutter-common, AbstractVariable: nano-tiny, AbstractVariable: openoffice.org, AbstractVariable: openssh-blacklist-extra, AbstractVariable: openssl-blacklist, AbstractVariable: openvpn, AbstractVariable: oxygen-icon-theme, AbstractVariable: perlmagick, AbstractVariable: phonon, AbstractVariable: phonon-backend-gstreamer, AbstractVariable: plasma-scriptengine-javascript, AbstractVariable: prboom, AbstractVariable: prover9, AbstractVariable: prover9-mace4, AbstractVariable: python-django-countries, AbstractVariable: python-wxgtk2.6, AbstractVariable: python-wxversion, AbstractVariable: shared-desktop-ontologies, AbstractVariable: smbfs, AbstractVariable: soprano-daemon, AbstractVariable: tp-smapi-modules-2.6.32-4-amd64, AbstractVariable: tp-smapi-modules-2.6.32-5-amd64, AbstractVariable: wcanadian-large] # starts : 2 # conflicts : 263 # decisions : 9078 # propagations : 369105 # inspects : 995212 # learnt literals : 37 # learnt binary clauses : 17 # learnt ternary clauses : 31 # learnt clauses : 225 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 366 # 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) : 605090.1639344263 # non guided choices 2663 # learnt constraints type #Solving done (3.541s). #Solution contains:1683