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:14:45 UTC 2010 #Using input file /home/misc2010/data/2010/difficult/rand49d73b.cudf #Using ouput file /home/misc2010/tmp/201007051419/p2cudf-paranoid-1.6/rand49d73b.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:1424 #Parsing done (1.425s). #Solving ... #Request size: 744 #Number of packages after slice: 5263 #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@64f6cd # 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 11542 46600 # Current objective function value: 138817(0.683s) # Current objective function value: 138800(1.027s) # Current objective function value: 138757(1.109s) # Current objective function value: 135867(1.298s) # Current objective function value: 132921(1.404s) # Current objective function value: 132918(1.487s) # Current objective function value: 127123(1.566s) # Current objective function value: 127117(1.677s) # Current objective function value: 127068(1.785s) # Current objective function value: 127050(1.847s) # cleaning 2473 clauses out of 4946 with flag 5001/5001 # cleaning 4236 clauses out of 8473 with flag 11001/11001 # cleaning 5617 clauses out of 11237 with flag 18001/18001 # cleaning 6804 clauses out of 13621 with flag 26002/26002 # Current objective function value: 127049(20.934s) # cleaning 7908 clauses out of 15816 with flag 35001/35001 # cleaning 8954 clauses out of 17907 with flag 45000/45000 # cleaning 9973 clauses out of 19952 with flag 56000/56000 # cleaning 10984 clauses out of 21979 with flag 68000/68000 # cleaning 11995 clauses out of 23995 with flag 81000/81000 # cleaning 12993 clauses out of 26000 with flag 95000/95000 # Current objective function value: 127048(63.318s) # cleaning 13986 clauses out of 28007 with flag 110000/110000 # cleaning 15008 clauses out of 30021 with flag 126000/126000 # cleaning 16000 clauses out of 32014 with flag 143001/143001 # cleaning 17001 clauses out of 34010 with flag 161000/161000 # cleaning 17997 clauses out of 36009 with flag 180000/180000 # Current objective function value: 127047(119.412s) # cleaning 18996 clauses out of 38012 with flag 200000/200000 # cleaning 19990 clauses out of 40016 with flag 221000/221000 # cleaning 21008 clauses out of 42028 with flag 243002/243002 # cleaning 22005 clauses out of 44019 with flag 266001/266001 # cleaning 23001 clauses out of 46013 with flag 290001/290001 # cleaning 24004 clauses out of 48012 with flag 315001/315001 # cleaning 24999 clauses out of 50007 with flag 341000/341000 # cleaning 25991 clauses out of 52008 with flag 368000/368000 # cleaning 27003 clauses out of 54017 with flag 396000/396000 # cleaning 28005 clauses out of 56014 with flag 425000/425000 # Paranoid criteria value: -43, -240 # Proof: [AbstractVariable: ant, AbstractVariable: ant-gcj, AbstractVariable: camlp4, AbstractVariable: camlp5, AbstractVariable: hsqldb-server, AbstractVariable: less, AbstractVariable: libcommons-modeler-java, AbstractVariable: libcryptgps-ocaml-dev, AbstractVariable: libcurl-ocaml, AbstractVariable: libcurl-ocaml-dev, AbstractVariable: libcurl4-gnutls-dev, AbstractVariable: libequeue-ocaml-dev, AbstractVariable: libexpat-ocaml, AbstractVariable: libexpat-ocaml-dev, AbstractVariable: libgcj7-jar, AbstractVariable: libidn11-dev, AbstractVariable: libjaxp1.3-java, AbstractVariable: libjaxp1.3-java-gcj, AbstractVariable: libocamlnet-ocaml, AbstractVariable: libocamlnet-ocaml-dev, AbstractVariable: libpcap-ruby1.8, AbstractVariable: libpcre-ocaml, AbstractVariable: libpcre-ocaml-dev, AbstractVariable: libpxp-ocaml-dev, AbstractVariable: libsnmp15, AbstractVariable: libtomcat5-java, AbstractVariable: libtomcat5.5-java, AbstractVariable: libxerces2-java, AbstractVariable: ocaml-base-nox, AbstractVariable: ocaml-compiler-libs, AbstractVariable: ocaml-findlib, AbstractVariable: ocaml-interp, AbstractVariable: ocaml-nox, AbstractVariable: ocaml-ulex, AbstractVariable: ocaml-ulex08, AbstractVariable: pkg-config, AbstractVariable: snmp, AbstractVariable: sun-java5-bin, AbstractVariable: sun-java5-demo, AbstractVariable: sun-java5-jdk, AbstractVariable: sun-java5-jre, AbstractVariable: tomcat5.5, AbstractVariable: zabbix-frontend-php, AbstractVariable: ant, AbstractVariable: ant-gcj, AbstractVariable: aptitude-doc-fr, AbstractVariable: aspell, AbstractVariable: aspell-cs, AbstractVariable: camlp4, AbstractVariable: camlp5, AbstractVariable: cernlib-base, AbstractVariable: cernlib-base-dev, AbstractVariable: cfortran, AbstractVariable: dictionaries-common, AbstractVariable: ejabberd, AbstractVariable: elinks-lite, AbstractVariable: erlang-base-hipe, AbstractVariable: erlang-nox, AbstractVariable: fontconfig-config, AbstractVariable: g++-4.1, AbstractVariable: gcc-4.4-base, AbstractVariable: gfortran, AbstractVariable: gfortran-4.3, AbstractVariable: gij-4.3, AbstractVariable: gnuplot-mode, AbstractVariable: gnuplot-nox, AbstractVariable: graphdefang, AbstractVariable: gstreamer0.10-ffmpeg, AbstractVariable: gstreamer0.10-plugins-bad, AbstractVariable: gstreamer0.10-x, AbstractVariable: hicolor-icon-theme, AbstractVariable: hsqldb-server, AbstractVariable: kdelibs-data, AbstractVariable: kdelibs4c2a, AbstractVariable: less, AbstractVariable: libakonadi-dev, AbstractVariable: libakonadiprivate1, AbstractVariable: libalgorithm-c3-perl, AbstractVariable: libart-2.0-2, AbstractVariable: libarts1c2a, AbstractVariable: libartsc0, AbstractVariable: libasound2, AbstractVariable: libaspell15, AbstractVariable: libatk1.0-0, AbstractVariable: libaudio2, AbstractVariable: libaudiofile0, AbstractVariable: libavahi-client3, AbstractVariable: libavahi-common-data, AbstractVariable: libavahi-common3, AbstractVariable: libavahi-qt3-1, AbstractVariable: libavalon-framework-java-doc, AbstractVariable: libb-hooks-endofscope-perl, AbstractVariable: libblas-dev, AbstractVariable: libblas3gf, 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: libcapi20-3, AbstractVariable: libcdaudio1, AbstractVariable: libcelt0-0, AbstractVariable: libclass-c3-perl, AbstractVariable: libclass-mop-perl, AbstractVariable: libcommons-modeler-java, AbstractVariable: libcompress-raw-zlib-perl, AbstractVariable: libcompress-zlib-perl, AbstractVariable: libcryptgps-ocaml-dev, AbstractVariable: libcurl-ocaml, AbstractVariable: libcurl-ocaml-dev, AbstractVariable: libcurl4-gnutls-dev, AbstractVariable: libdap-bin, AbstractVariable: libdap10, AbstractVariable: libdata-optlist-perl, AbstractVariable: libdb4.7, AbstractVariable: libdbus-1-3, AbstractVariable: libdevel-globaldestruction-perl, AbstractVariable: libecj-java-gcj, AbstractVariable: libequeue-ocaml-dev, AbstractVariable: libesd-alsa0, AbstractVariable: libexempi3, AbstractVariable: libexif12, AbstractVariable: libexpat-ocaml, AbstractVariable: libexpat-ocaml-dev, AbstractVariable: libextractor1c2a, AbstractVariable: libfam0, AbstractVariable: libfftw3-3, AbstractVariable: libfile-readbackwards-perl, AbstractVariable: libflac8, AbstractVariable: libflickcurl0, AbstractVariable: libflickcurl0-dbg, AbstractVariable: libfontconfig1, AbstractVariable: libfontenc1, AbstractVariable: libgcj7-jar, AbstractVariable: libgd-gd2-perl, AbstractVariable: libgd-graph-perl, AbstractVariable: libgd-text-perl, AbstractVariable: libgetfem++-dev, AbstractVariable: libgetfem4++, AbstractVariable: libgfortran3, AbstractVariable: libgl1-mesa-swx11, AbstractVariable: libglu1-mesa, AbstractVariable: libgmp3-dev, AbstractVariable: libgmpxx4ldbl, AbstractVariable: libgmyth0, AbstractVariable: libgrib-api-0d-0, AbstractVariable: libgrib-api-data, AbstractVariable: libgssapi-krb5-2, AbstractVariable: libgstreamer-plugins-base0.10-0, AbstractVariable: libgstreamer0.10-0, AbstractVariable: libhal1, AbstractVariable: libicu38, AbstractVariable: libidn11-dev, AbstractVariable: libidzebra-2.0-0, AbstractVariable: libidzebra-2.0-mod-grs-regx, AbstractVariable: libio-compress-base-perl, AbstractVariable: libio-compress-zlib-perl, AbstractVariable: libiptcdata0, AbstractVariable: libjack0, AbstractVariable: libjaxp1.3-java, AbstractVariable: libjaxp1.3-java-gcj, AbstractVariable: libk5crypto3, AbstractVariable: libkdegames1, AbstractVariable: libkernlib1-dev, AbstractVariable: libkernlib1-gfortran, AbstractVariable: libkrb5-3, AbstractVariable: libkrb5support0, AbstractVariable: liblapack-dev, AbstractVariable: liblapack3gf, AbstractVariable: liblist-moreutils-perl, AbstractVariable: liblog4cpp5, AbstractVariable: liblua50, AbstractVariable: liblualib50, AbstractVariable: libmad0, AbstractVariable: libmathlib2-gfortran, AbstractVariable: libmldbm-perl, AbstractVariable: libmms0, AbstractVariable: libmng1, AbstractVariable: libmoose-perl, AbstractVariable: libmoosex-traits-perl, AbstractVariable: libmpcdec3, AbstractVariable: libmro-compat-perl, AbstractVariable: libmusicbrainz4c2a, AbstractVariable: libmysqlclient16, AbstractVariable: libnamespace-autoclean-perl, AbstractVariable: libnamespace-clean-perl, AbstractVariable: libocamlnet-ocaml, AbstractVariable: libocamlnet-ocaml-dev, AbstractVariable: libofa0, AbstractVariable: liboil0.3, AbstractVariable: libopenspc0, AbstractVariable: libosmesa6, AbstractVariable: libpacklib1-dev, AbstractVariable: libpacklib1-gfortran, AbstractVariable: libparams-util-perl, AbstractVariable: libpcap-ruby1.8, AbstractVariable: libpcre-ocaml, AbstractVariable: libpcre-ocaml-dev, AbstractVariable: libperl5.10, AbstractVariable: libphonon4, AbstractVariable: libpostproc51, AbstractVariable: libpq5, AbstractVariable: libpxp-ocaml-dev, AbstractVariable: libqhull5, AbstractVariable: libqt3-mt, AbstractVariable: libqt4-dbus, AbstractVariable: libqt4-network, AbstractVariable: libqt4-opengl, AbstractVariable: libqt4-sql, AbstractVariable: libqt4-sql-psql, AbstractVariable: libqt4-xml, AbstractVariable: libqtcore4, AbstractVariable: libqtgui4, AbstractVariable: libresid-builder0c2a, AbstractVariable: libsamplerate0, AbstractVariable: libscope-guard-perl, AbstractVariable: libsctp1, AbstractVariable: libsndfile1, AbstractVariable: libsnmp15, AbstractVariable: libsoundtouch1c2, AbstractVariable: libssl0.9.8, AbstractVariable: libstdc++6, AbstractVariable: libstdc++6-4.1-dev, AbstractVariable: libsub-exporter-perl, AbstractVariable: libsub-identify-perl, AbstractVariable: libsub-install-perl, AbstractVariable: libsub-name-perl, AbstractVariable: libsuperlu3, AbstractVariable: libtask-weaken-perl, AbstractVariable: libtomcat5-java, AbstractVariable: libtomcat5.5-java, AbstractVariable: libtry-tiny-perl, AbstractVariable: libvariable-magic-perl, AbstractVariable: libvorbisfile3, AbstractVariable: libvte-common, AbstractVariable: libvte-ruby1.8, AbstractVariable: libvte9, AbstractVariable: libwildmidi0, AbstractVariable: libwine, AbstractVariable: libxalan110, AbstractVariable: libxaw7, AbstractVariable: libxerces-c28, AbstractVariable: libxerces2-java, AbstractVariable: libxfont1, AbstractVariable: libxml-security-c14, AbstractVariable: libxml2, AbstractVariable: libxmu6, AbstractVariable: libxrandr2, AbstractVariable: libxslt1.1, AbstractVariable: libxv1, AbstractVariable: libxxf86vm1, AbstractVariable: libyaz3, AbstractVariable: locales, AbstractVariable: menu-xdg, AbstractVariable: mysql-common, AbstractVariable: nagios-plugins-standard, AbstractVariable: nscd, AbstractVariable: ocaml-base-nox, AbstractVariable: ocaml-compiler-libs, AbstractVariable: ocaml-findlib, AbstractVariable: ocaml-interp, AbstractVariable: ocaml-nox, AbstractVariable: ocaml-ulex, AbstractVariable: ocaml-ulex08, AbstractVariable: oss-compat, AbstractVariable: perl, AbstractVariable: perl-base, AbstractVariable: perl-modules, AbstractVariable: phonon, AbstractVariable: phonon-backend-gstreamer, AbstractVariable: pkg-config, AbstractVariable: snmp, AbstractVariable: sun-java5-bin, AbstractVariable: sun-java5-demo, AbstractVariable: sun-java5-jdk, AbstractVariable: sun-java5-jre, AbstractVariable: tcl8.4, AbstractVariable: tomcat5.5, AbstractVariable: x11-xserver-utils, AbstractVariable: xdmx, AbstractVariable: zabbix-frontend-php] # starts : 162 # conflicts : 431866 # decisions : 2575686 # propagations : 516216262 # inspects : 1180767242 # learnt literals : 60 # learnt binary clauses : 357 # learnt ternary clauses : 93 # learnt clauses : 431806 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 1098566 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 25 # 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) : 3206969.5154907526 # non guided choices 34825 # learnt constraints type #Solving done (282.373s). #Solution contains:799