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 19:16:35 UTC 2010 #Using input file /home/misc2010/data/2010/debian-dudf/cb0e73b0-0ffd-11df-9e59-00163e2c8d72.cudf #Using ouput file /home/misc2010/tmp/201007051233/p2cudf-paranoid-1.6/cb0e73b0-0ffd-11df-9e59-00163e2c8d72.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:2874 #Parsing done (2.874s). #Solving ... #Request size: 2153 #Number of packages after slice: 4548 #Slice efficiency: 86% ## 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@ce5b1c # 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 14364 49188 # Current objective function value: 149928(0.81s) # Current objective function value: 149899(1.23s) # Current objective function value: 149898(2.49s) # Current objective function value: 146425(2.67s) # Current objective function value: 146424(2.91s) # Current objective function value: 146413(2.97s) # Current objective function value: 146412(3.15s) # Paranoid criteria value: -42, -84 # Proof: [AbstractVariable: empathy, AbstractVariable: epiphany-gecko, AbstractVariable: gimp-print, AbstractVariable: gnome-network-admin, AbstractVariable: gobject-introspection-repository, AbstractVariable: hugin-bin, AbstractVariable: kqemu-modules-2.6.18-5-686, AbstractVariable: kqemu-modules-2.6.18-6-686, AbstractVariable: lapack3, AbstractVariable: libavcodec51, AbstractVariable: libdiscover1, AbstractVariable: libdns50, AbstractVariable: libempathy-gtk19, AbstractVariable: libempathy23, AbstractVariable: libg2c0, AbstractVariable: libgdl-1-0, AbstractVariable: libgladeui-1-7, AbstractVariable: libglib1.2, AbstractVariable: libgmime-2.0-2, AbstractVariable: libgoffice-0-4, AbstractVariable: libgoffice-0-6, AbstractVariable: libgssapi2, AbstractVariable: libgtksourceview1.0-0, AbstractVariable: libgvfscommon0, AbstractVariable: libmetacity0, AbstractVariable: libnl1-pre6, AbstractVariable: libopal-2.2.0, AbstractVariable: liborbit0, AbstractVariable: libpci2, AbstractVariable: librpm4, AbstractVariable: librpm4.4, AbstractVariable: libslab0, AbstractVariable: libssp0, AbstractVariable: libstlport4.6c2, AbstractVariable: libufsparse, AbstractVariable: libvte4, AbstractVariable: mono-common, AbstractVariable: nautilus-cd-burner, AbstractVariable: openoffice.org-gcj, AbstractVariable: postfix, AbstractVariable: serpentine, AbstractVariable: update-manager, AbstractVariable: apache2-utils, AbstractVariable: apache2.2-bin, AbstractVariable: apache2.2-common, AbstractVariable: bogofilter, AbstractVariable: bogofilter-bdb, AbstractVariable: ekiga, AbstractVariable: empathy, AbstractVariable: epiphany-gecko, AbstractVariable: evolution-exchange, AbstractVariable: gimp-print, AbstractVariable: gnome-network-admin, AbstractVariable: gobject-introspection-repository, AbstractVariable: hamster-applet, AbstractVariable: hugin-bin, AbstractVariable: kqemu-modules-2.6.18-5-686, AbstractVariable: kqemu-modules-2.6.18-6-686, AbstractVariable: lapack3, AbstractVariable: libaprutil1-dbd-odbc, AbstractVariable: libaprutil1-ldap, AbstractVariable: libavcodec51, AbstractVariable: libdiscover1, AbstractVariable: libdns50, AbstractVariable: libebook1.2-9, AbstractVariable: libecal1.2-7, AbstractVariable: libedataserver1.2-11, AbstractVariable: libempathy-gtk19, AbstractVariable: libempathy23, AbstractVariable: libg2c0, AbstractVariable: libgdl-1-0, AbstractVariable: libggi-target-fbdev, AbstractVariable: libgladeui-1-7, AbstractVariable: libglib1.2, AbstractVariable: libgmime-2.0-2, AbstractVariable: libgmime2.2a-cil, AbstractVariable: libgnomepanel2.24-cil, AbstractVariable: libgoffice-0-4, AbstractVariable: libgoffice-0-6, AbstractVariable: libgssapi2, AbstractVariable: libgtksourceview1.0-0, AbstractVariable: libgvfscommon0, AbstractVariable: libmetacity0, AbstractVariable: libnl1-pre6, AbstractVariable: libopal-2.2.0, AbstractVariable: libopal3.6.6, AbstractVariable: liborbit0, AbstractVariable: libpci2, AbstractVariable: libpt-1.10.10-plugins-alsa, AbstractVariable: libpt-1.10.10-plugins-v4l, AbstractVariable: libpt2.6.5, AbstractVariable: libpt2.6.5-plugins, AbstractVariable: librpm4, AbstractVariable: librpm4.4, AbstractVariable: libslab0, AbstractVariable: libssp0, AbstractVariable: libstlport4.6c2, AbstractVariable: libufsparse, AbstractVariable: libvte4, AbstractVariable: libxml-xpath-perl, AbstractVariable: mono-common, AbstractVariable: nautilus-cd-burner, AbstractVariable: openoffice.org-gcj, AbstractVariable: policykit-gnome, AbstractVariable: pornview, AbstractVariable: postfix, AbstractVariable: python-cups, AbstractVariable: python-cupsutils, AbstractVariable: python-evolution, AbstractVariable: python-gdbm, AbstractVariable: python-sexy, AbstractVariable: scrollkeeper, AbstractVariable: serpentine, AbstractVariable: system-config-printer, AbstractVariable: tasksel-data, AbstractVariable: totem, AbstractVariable: totem-gstreamer, AbstractVariable: totem-xine, AbstractVariable: transmission-common, AbstractVariable: transmission-daemon, AbstractVariable: transmission-gtk, AbstractVariable: update-manager, AbstractVariable: update-notifier, AbstractVariable: xloadimage, AbstractVariable: xserver-common, AbstractVariable: xserver-xephyr] # starts : 26 # conflicts : 4632 # decisions : 73611 # propagations : 7516671 # inspects : 19668330 # learnt literals : 32 # learnt binary clauses : 79 # learnt ternary clauses : 75 # learnt clauses : 4599 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 76115 # 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) : 2122753.741880825 # non guided choices 25868 # learnt constraints type #Solving done (9.472s). #Solution contains:2136