HEAD is now at 5df24db initial deployement # Checking available version of Java # Java(TM) SE Runtime Environment (build 1.6.0_20-b02) # Running really p2cudf #Solver launched on Mon Jul 05 18:56:49 UTC 2010 #Using input file /home/misc2010/data/2010/difficult/rand4d6b1c.cudf #Using ouput file /home/misc2010/tmp/201007051419/p2cudf-paranoid-1.6/rand4d6b1c.cudf.difficult.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 16.3-b01 #java.vm.vendor Sun Microsystems Inc. #sun.arch.data.model 32 #java.version 1.6.0_20 #os.name Linux #os.version 2.6.18-6-xen-amd64 #os.arch i386 #Free memory 699792080 #Max memory 703463424 #Total memory 703463424 #Number of processors 2 #Parsing ... #Time to parse:1669 #Parsing done (1.67s). #Solving ... #Request size: 743 #Number of packages after slice: 5213 #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@17d5d2a # 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 11484 46349 # Current objective function value: 88087(0.611s) # Current objective function value: 88071(0.901s) # Current objective function value: 79265(0.974s) # Current objective function value: 76427(1.715s) # Current objective function value: 76363(1.791s) # Current objective function value: 76362(1.841s) # Current objective function value: 76361(1.903s) # cleaning 2463 clauses out of 4929 with flag 5000/5000 # Paranoid criteria value: -26, -181 # Proof: [AbstractVariable: bsd-mailx, AbstractVariable: gij-4.1, AbstractVariable: gosa, AbstractVariable: gosa-help-fr, AbstractVariable: libclamav6, AbstractVariable: libcommons-beanutils-java, AbstractVariable: libcommons-collections3-java, AbstractVariable: libcommons-digester-java, AbstractVariable: libcommons-fileupload-java, AbstractVariable: libcommons-modeler-java, AbstractVariable: libgcj7-0, AbstractVariable: libgcj7-jar, AbstractVariable: libmx4j-java, AbstractVariable: librrd4, AbstractVariable: librrds-perl, AbstractVariable: libtomcat5-java, AbstractVariable: libtomcat5.5-java, AbstractVariable: libtommath0, AbstractVariable: mailx, AbstractVariable: munin, AbstractVariable: php5, AbstractVariable: php5-xdebug, AbstractVariable: rrdtool, AbstractVariable: tasksel, AbstractVariable: tasksel-data, AbstractVariable: tomcat5.5, AbstractVariable: ant-optional, AbstractVariable: ant-optional-gcj, AbstractVariable: aptitude-doc-ja, AbstractVariable: arc-dust, AbstractVariable: avahi-daemon, AbstractVariable: avahi-utils, AbstractVariable: bsd-mailx, AbstractVariable: checkpolicy, AbstractVariable: clamav, AbstractVariable: clamav-base, AbstractVariable: clamav-daemon, AbstractVariable: clamav-freshclam, AbstractVariable: dbus, AbstractVariable: dictionaries-common, AbstractVariable: dvbackup, AbstractVariable: freeglut3, AbstractVariable: g++-4.3, AbstractVariable: gcc-4.4-base, AbstractVariable: gconf2, AbstractVariable: gconf2-common, AbstractVariable: gdm, AbstractVariable: gij-4.1, AbstractVariable: gksu, AbstractVariable: gnome-keyring, AbstractVariable: gosa, AbstractVariable: gosa-help-fr, AbstractVariable: heirloom-mailx, AbstractVariable: libapache2-mod-auth-plain, AbstractVariable: libart-2.0-2, AbstractVariable: libaudio2, AbstractVariable: libavahi-client3, AbstractVariable: libavahi-common-data, AbstractVariable: libavahi-common3, AbstractVariable: libavahi-core6, AbstractVariable: libboost-dev, AbstractVariable: libboost-serialization-dev, AbstractVariable: libboost-serialization1.34.1, AbstractVariable: libc-bin, AbstractVariable: libc-dev-bin, AbstractVariable: libc6, AbstractVariable: libc6-dev, AbstractVariable: libcache-cache-perl, AbstractVariable: libclamav5, AbstractVariable: libclamav6, AbstractVariable: libclass-container-perl, AbstractVariable: libcommons-beanutils-java, AbstractVariable: libcommons-collections3-java, AbstractVariable: libcommons-digester-java, AbstractVariable: libcommons-fileupload-java, AbstractVariable: libcommons-modeler-java, AbstractVariable: libcompress-raw-zlib-perl, AbstractVariable: libcompress-zlib-perl, AbstractVariable: libdaemon0, AbstractVariable: libdb4.7, AbstractVariable: libdbus-1-3, AbstractVariable: libdbus-glib-1-2, AbstractVariable: libdevel-stacktrace-perl, AbstractVariable: libdmx1, AbstractVariable: libdv-bin, AbstractVariable: libdv4, AbstractVariable: libdw1, AbstractVariable: libdynamite0, AbstractVariable: libecj-java-gcj, AbstractVariable: libelf1, AbstractVariable: libexception-class-perl, AbstractVariable: libfontenc1, AbstractVariable: libfs6, AbstractVariable: libgail-common, AbstractVariable: libgail18, AbstractVariable: libgcj7-0, AbstractVariable: libgcj7-jar, AbstractVariable: libgconf2-4, AbstractVariable: libgksu2-0, AbstractVariable: libgksuui1.0-1, AbstractVariable: libgl1-mesa-swx11, AbstractVariable: libglade2-0, AbstractVariable: libglib1.2ldbl, AbstractVariable: libglibmm-2.4-1c2a, AbstractVariable: libglu1-mesa, AbstractVariable: libgnome-keyring0, AbstractVariable: libgnomecanvas2-0, AbstractVariable: libgnomecanvas2-common, AbstractVariable: libgtk1.2, AbstractVariable: libgtk1.2-common, AbstractVariable: libgtop2-7, AbstractVariable: libgtop2-common, AbstractVariable: libhal-storage1, AbstractVariable: libhal1, AbstractVariable: libhook-lexwrap-perl, AbstractVariable: libhtml-mason-perl, AbstractVariable: libhttp-server-simple-mason-perl, AbstractVariable: libhttp-server-simple-perl, AbstractVariable: libidl0, AbstractVariable: libio-compress-base-perl, AbstractVariable: libio-compress-zlib-perl, AbstractVariable: libipc-sharelite-perl, AbstractVariable: libltdl3, AbstractVariable: liblzma2, AbstractVariable: liblzo2-2, AbstractVariable: liblzo2-dev, AbstractVariable: libmagick++10, AbstractVariable: libmng1, AbstractVariable: libmx4j-java, AbstractVariable: libnspr4-0d, AbstractVariable: libnss3-1d, AbstractVariable: libnss3-tools, AbstractVariable: libnuclient3, AbstractVariable: liborange0, AbstractVariable: liborbit2, AbstractVariable: libosmesa6, AbstractVariable: libpam-nufw, AbstractVariable: libparams-util-perl, AbstractVariable: libpci3, AbstractVariable: libperl5.10, AbstractVariable: libqt3-mt, AbstractVariable: librrd4, AbstractVariable: librrds-perl, AbstractVariable: librsvg2-common, AbstractVariable: libsemanage1, AbstractVariable: libsqlite3-0, AbstractVariable: libstartup-notification0, AbstractVariable: libstdc++6, AbstractVariable: libstdc++6-4.3-dev, AbstractVariable: libsynce0, AbstractVariable: libsynfig0, AbstractVariable: libsynfigapp0, AbstractVariable: libtomcat5-java, AbstractVariable: libtomcat5.5-java, AbstractVariable: libtommath0, AbstractVariable: libunshield0, AbstractVariable: libustr-1.0-1, AbstractVariable: libxaw7, AbstractVariable: libxcb-event0, AbstractVariable: libxfont1, AbstractVariable: libxkbfile1, AbstractVariable: libxml++2.6-2, AbstractVariable: libxmu6, AbstractVariable: libxrandr2, AbstractVariable: libxv1, AbstractVariable: libxxf86dga1, AbstractVariable: libxxf86vm1, AbstractVariable: locales, AbstractVariable: m4, AbstractVariable: mailx, AbstractVariable: mtools, AbstractVariable: munin, AbstractVariable: museeq, AbstractVariable: nscd, AbstractVariable: orange, AbstractVariable: perl, AbstractVariable: perl-base, AbstractVariable: perl-modules, AbstractVariable: php5, AbstractVariable: php5-xdebug, AbstractVariable: policycoreutils, AbstractVariable: pterm, AbstractVariable: python-debian, AbstractVariable: python-semanage, AbstractVariable: python-sepolgen, AbstractVariable: rrdtool, AbstractVariable: selinux-policy-dev, AbstractVariable: systemtap, AbstractVariable: systemtap-client, AbstractVariable: systemtap-common, AbstractVariable: systemtap-runtime, AbstractVariable: tasksel, AbstractVariable: tasksel-data, AbstractVariable: tomcat5.5, AbstractVariable: x11-apps, AbstractVariable: x11-session-utils, AbstractVariable: x11-utils, AbstractVariable: x11-xfs-utils, AbstractVariable: x11-xkb-utils, AbstractVariable: x11-xserver-utils, AbstractVariable: xbase-clients, AbstractVariable: xinit, AbstractVariable: xmms2-core, AbstractVariable: xmms2-plugin-gme, AbstractVariable: xnest, AbstractVariable: xtux-levels, AbstractVariable: zip] # starts : 35 # conflicts : 10876 # decisions : 227048 # propagations : 17808069 # inspects : 36271827 # learnt literals : 86 # learnt binary clauses : 229 # learnt ternary clauses : 99 # learnt clauses : 10789 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 50460 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 1 # 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) : 1348891.7588244206 # non guided choices 18119 # learnt constraints type #Solving done (17.459s). #Solution contains:773