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 16:23:30 UTC 2010 #Using input file /home/misc2010/data/2010/debian-dudf/412959c6-e965-11de-8ebf-00163e6585dd.cudf #Using ouput file /home/misc2010/tmp/201007051233/p2cudf-paranoid-1.6/412959c6-e965-11de-8ebf-00163e6585dd.cudf.debian-dudf.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:2873 #Parsing done (2.873s). #Solving ... #Request size: 1546 #Number of packages after slice: 3530 #Slice efficiency: 90% ## 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@105738 # 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 10965 37386 # Current objective function value: 39139(0.611s) # Current objective function value: 39133(0.921s) # Current objective function value: 39130(0.981s) # Current objective function value: 39129(1.161s) # Current objective function value: 39128(1.161s) # Current objective function value: 39127(1.221s) # Current objective function value: 39126(1.542s) # Paranoid criteria value: -14, -52 # Proof: [AbstractVariable: epiphany-gecko, AbstractVariable: gobject-introspection-repository, AbstractVariable: libbeecrypt6, AbstractVariable: libdatrie0, AbstractVariable: libdns50, AbstractVariable: libeel2-2.20, AbstractVariable: libgdl-1-0, AbstractVariable: libgnomekbd2, AbstractVariable: libgnomekbdui2, AbstractVariable: libmetacity0, AbstractVariable: libslab0, AbstractVariable: libuniconf4.4, AbstractVariable: serpentine, AbstractVariable: tp-smapi-modules-2.6.30-1-amd64, AbstractVariable: aptitude-doc-ja, AbstractVariable: aspell, AbstractVariable: aspell-ca, AbstractVariable: bluez-utils, AbstractVariable: bogofilter, AbstractVariable: bogofilter-bdb, AbstractVariable: bogofilter-common, AbstractVariable: epiphany-gecko, AbstractVariable: evolution-exchange, AbstractVariable: freeglut3, AbstractVariable: ggzcore-bin, AbstractVariable: gnome-cards-data, AbstractVariable: gnome-games, AbstractVariable: gnome-games-data, AbstractVariable: gobject-introspection-repository, AbstractVariable: gstreamer0.10-gnomevfs, AbstractVariable: gtk2-engines-pixbuf, AbstractVariable: jackd, AbstractVariable: libbeecrypt6, AbstractVariable: libclutter-1.0-0, AbstractVariable: libclutter-gtk-0.10-0, AbstractVariable: libcucul0, AbstractVariable: libdatrie0, AbstractVariable: libdns50, AbstractVariable: libeel2-2.20, AbstractVariable: libgdl-1-0, AbstractVariable: libgnomekbd2, AbstractVariable: libgnomekbdui2, AbstractVariable: libgtkglext1, AbstractVariable: libmetacity0, AbstractVariable: libslab0, AbstractVariable: libuniconf4.4, AbstractVariable: libxalan2-java, AbstractVariable: libxerces2-java, AbstractVariable: mesa-utils, AbstractVariable: p7zip-full, AbstractVariable: perlmagick, AbstractVariable: python-cups, AbstractVariable: python-cupsutils, AbstractVariable: python-gdbm, AbstractVariable: python-gtkglext1, AbstractVariable: python-gtkhtml2, AbstractVariable: python-gtkmozembed, AbstractVariable: python-opengl, AbstractVariable: python-sexy, AbstractVariable: python-xdg, AbstractVariable: serpentine, AbstractVariable: system-config-printer, AbstractVariable: tp-smapi-modules-2.6.30-1-amd64, AbstractVariable: transmission-common, AbstractVariable: transmission-gtk, AbstractVariable: xserver-xorg-video-openchrome] # starts : 9 # conflicts : 295 # decisions : 43957 # propagations : 819843 # inspects : 2276867 # learnt literals : 9 # learnt binary clauses : 21 # learnt ternary clauses : 12 # learnt clauses : 285 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 2228 # 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) : 4554683.333333334 # non guided choices 19443 # learnt constraints type #Solving done (4.252s). #Solution contains:1561