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 23:53:14 UTC 2010 #Using input file /home/misc2010/data/2010/difficult/randa651ed.cudf #Using ouput file /home/misc2010/tmp/201007051419/p2cudf-paranoid-1.6/randa651ed.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:1852 #Parsing done (1.853s). #Solving ... #Request size: 744 #Number of packages after slice: 5171 #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@1617189 # 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 11369 46494 # Current objective function value: 109470(0.601s) # Current objective function value: 109462(1.012s) # Current objective function value: 106594(1.09s) # Current objective function value: 106562(1.283s) # Current objective function value: 100807(1.391s) # Current objective function value: 95073(1.441s) # Current objective function value: 95072(1.494s) # Current objective function value: 95071(1.645s) # Current objective function value: 95068(1.922s) # Current objective function value: 95067(2.036s) # Current objective function value: 95066(2.212s) # Current objective function value: 95065(2.466s) # Current objective function value: 95064(5.775s) # cleaning 2463 clauses out of 4934 with flag 5000/5000 # cleaning 4234 clauses out of 8469 with flag 11001/11001 # cleaning 5619 clauses out of 11237 with flag 18003/18003 # cleaning 6803 clauses out of 13612 with flag 26000/26000 # Paranoid criteria value: -33, -189 # Proof: [AbstractVariable: binutils, AbstractVariable: camlp4, AbstractVariable: camlp5, AbstractVariable: debhelper, AbstractVariable: dpkg-dev, AbstractVariable: gcc, AbstractVariable: gcc-4.1, AbstractVariable: gcc-4.3, AbstractVariable: git-core, AbstractVariable: gitweb, AbstractVariable: jhead, AbstractVariable: libcryptgps-ocaml-dev, AbstractVariable: libcurl-ocaml-dev, AbstractVariable: libcurl4-gnutls-dev, AbstractVariable: libequeue-ocaml-dev, AbstractVariable: liberror-perl, AbstractVariable: libexpat-ocaml-dev, AbstractVariable: libio-compress-base-perl, AbstractVariable: libldap2-dev, AbstractVariable: liblog4j1.2-java-gcj, AbstractVariable: libmagick10, AbstractVariable: libocamlnet-ocaml-dev, AbstractVariable: libopenexr6, AbstractVariable: libpcre-ocaml-dev, AbstractVariable: libpxp-ocaml-dev, AbstractVariable: librrds-perl, AbstractVariable: libtbb2, AbstractVariable: munin, AbstractVariable: ocaml-compiler-libs, AbstractVariable: ocaml-findlib, AbstractVariable: ocaml-nox, AbstractVariable: ocaml-ulex, AbstractVariable: ocaml-ulex08, AbstractVariable: alsa-tools-gui, AbstractVariable: ant-optional, AbstractVariable: ant-optional-gcj, AbstractVariable: apt-watch-backend, AbstractVariable: apt-watch-gnome, AbstractVariable: aptitude-doc-en, AbstractVariable: bc, AbstractVariable: binutils, AbstractVariable: camlp4, AbstractVariable: camlp5, AbstractVariable: console-tools, AbstractVariable: curl, AbstractVariable: dbus, AbstractVariable: dctrl-tools, AbstractVariable: debhelper, AbstractVariable: debian-cd, AbstractVariable: debootstrap, AbstractVariable: debpartial-mirror, AbstractVariable: dictionaries-common, AbstractVariable: dpkg-dev, AbstractVariable: etckeeper, AbstractVariable: fnorb, AbstractVariable: fontconfig-config, AbstractVariable: gcc, AbstractVariable: gcc-4.1, AbstractVariable: gcc-4.3, AbstractVariable: gconf2, AbstractVariable: gconf2-common, AbstractVariable: genisoimage, AbstractVariable: git-core, AbstractVariable: gitweb, AbstractVariable: gnome-mime-data, AbstractVariable: hal, AbstractVariable: hal-info, AbstractVariable: icedove, AbstractVariable: icedove-l10n-tr, AbstractVariable: icedove-locale-tr, AbstractVariable: imagemagick, AbstractVariable: jhead, AbstractVariable: libabstract-ruby1.9, AbstractVariable: libart-2.0-2, AbstractVariable: libasound2, AbstractVariable: libatk1.0-0, AbstractVariable: libatlas3gf-sse2, AbstractVariable: libaudio2, AbstractVariable: libaudiofile0, AbstractVariable: libavahi-client3, AbstractVariable: libavahi-common-data, AbstractVariable: libavahi-common3, AbstractVariable: libavahi-glib1, AbstractVariable: libbinio1ldbl, AbstractVariable: libbonobo2-0, AbstractVariable: libbonobo2-common, AbstractVariable: libbonoboui2-0, AbstractVariable: libbonoboui2-common, AbstractVariable: libcompress-raw-zlib-perl, AbstractVariable: libcompress-zlib-perl, AbstractVariable: libconsole, AbstractVariable: libcryptgps-ocaml-dev, AbstractVariable: libcurl-ocaml-dev, AbstractVariable: libcurl4-gnutls-dev, AbstractVariable: libdb4.7, AbstractVariable: libdbus-1-3, AbstractVariable: libdbus-glib-1-2, AbstractVariable: libecj-java, AbstractVariable: libequeue-ocaml-dev, AbstractVariable: liberror-perl, AbstractVariable: libesd-alsa0, AbstractVariable: libexpat-ocaml-dev, AbstractVariable: libfam0, AbstractVariable: libffi5, AbstractVariable: libfftw3-3, AbstractVariable: libflac8, AbstractVariable: libfltk1.1, AbstractVariable: libfontconfig1, AbstractVariable: libfontenc1, AbstractVariable: libgail-common, AbstractVariable: libgail18, AbstractVariable: libgconf2-4, AbstractVariable: libgfortran3, AbstractVariable: libgl1-mesa-swx11, AbstractVariable: libglade2-0, AbstractVariable: libglu1-mesa, AbstractVariable: libgnome-keyring0, AbstractVariable: libgnome2-0, AbstractVariable: libgnome2-common, AbstractVariable: libgnomecanvas2-0, AbstractVariable: libgnomecanvas2-common, AbstractVariable: libgnomeui-0, AbstractVariable: libgnomeui-common, AbstractVariable: libgnomevfs2-0, AbstractVariable: libgnomevfs2-common, AbstractVariable: libgtkhtml2-0, AbstractVariable: libgutenprint2, AbstractVariable: libgutenprintui2-1, AbstractVariable: libgutenprintui2-dev, AbstractVariable: libhal-storage1, AbstractVariable: libhal1, AbstractVariable: libhunspell-1.2-0, AbstractVariable: libidl0, AbstractVariable: libio-compress-base-perl, AbstractVariable: libio-compress-zlib-perl, AbstractVariable: libiodbc2, AbstractVariable: libldap2-dev, AbstractVariable: liblog4j1.2-java-gcj, AbstractVariable: liblqr-1-0, AbstractVariable: libltdl7, AbstractVariable: libmagick10, AbstractVariable: libmagickcore3, AbstractVariable: libmagickwand3, AbstractVariable: libmng1, AbstractVariable: libnet6-1.3-0, AbstractVariable: libnet6-1.3-dev, AbstractVariable: libnetcdf4, AbstractVariable: libnspr4-0d, AbstractVariable: libnss3-1d, AbstractVariable: libocamlnet-ocaml-dev, AbstractVariable: liboil0.3, AbstractVariable: libopenexr6, AbstractVariable: liborbit2, AbstractVariable: libosmesa6, AbstractVariable: libpanel-applet2-0, AbstractVariable: libpci3, AbstractVariable: libpcre-ocaml-dev, AbstractVariable: libperl5.10, AbstractVariable: libpulsecore5, AbstractVariable: libpxp-ocaml-dev, AbstractVariable: libqt3-mt, AbstractVariable: librrds-perl, AbstractVariable: libruby1.9, AbstractVariable: libsamplerate0, AbstractVariable: libshhopt1, AbstractVariable: libshhopt1-dev, AbstractVariable: libsigc++-2.0-0c2a, AbstractVariable: libsigc++-2.0-dev, AbstractVariable: libsmbios2, AbstractVariable: libsndfile1, AbstractVariable: libtbb2, AbstractVariable: libtelepathy-glib0, AbstractVariable: libxaw7, AbstractVariable: libxml2, AbstractVariable: libxmu6, AbstractVariable: libxv1, AbstractVariable: libxxf86dga1, AbstractVariable: libxxf86vm1, AbstractVariable: lynx-cur, AbstractVariable: mpichpython, AbstractVariable: munin, AbstractVariable: nasm, AbstractVariable: ocaml-compiler-libs, AbstractVariable: ocaml-findlib, AbstractVariable: ocaml-nox, AbstractVariable: ocaml-ulex, AbstractVariable: ocaml-ulex08, AbstractVariable: pciutils, AbstractVariable: perl, AbstractVariable: perl-base, AbstractVariable: perl-modules, AbstractVariable: pm-utils, AbstractVariable: powermgmt-base, AbstractVariable: pulseaudio-module-hal, AbstractVariable: pulseaudio-module-hal-dbg, AbstractVariable: python-cairo, AbstractVariable: python-cdd, AbstractVariable: python-gobject, AbstractVariable: python-gtk2, AbstractVariable: python-gtkhtml2, AbstractVariable: python-jinja, AbstractVariable: python-mpi, AbstractVariable: python-netcdf, AbstractVariable: python-numeric, AbstractVariable: python-numeric-ext, AbstractVariable: python-pycurl, AbstractVariable: python-pygments, AbstractVariable: python-scientific, AbstractVariable: python-sphinx, AbstractVariable: rsync, AbstractVariable: ruby1.9, AbstractVariable: shared-mime-info, AbstractVariable: simple-cdd, AbstractVariable: tcc, AbstractVariable: tofrodos, AbstractVariable: udev, AbstractVariable: usbutils, AbstractVariable: x11-utils, AbstractVariable: xbitmaps, AbstractVariable: xpdf-common, AbstractVariable: xpdf-utils, AbstractVariable: xterm] # starts : 66 # conflicts : 28324 # decisions : 242279 # propagations : 38594242 # inspects : 97740570 # learnt literals : 82 # learnt binary clauses : 262 # learnt ternary clauses : 96 # learnt clauses : 28241 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 226080 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 4 # 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) : 2477006.738976959 # non guided choices 33546 # learnt constraints type #Solving done (23.247s). #Solution contains:773