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 Tue Jul 06 01:19:34 UTC 2010 #Using input file /home/misc2010/data/2010/difficult/randf17677.cudf #Using ouput file /home/misc2010/tmp/201007051419/p2cudf-paranoid-1.6/randf17677.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:1469 #Parsing done (1.47s). #Solving ... #Request size: 745 #Number of packages after slice: 5299 #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 11604 46786 # Current objective function value: 53799(0.754s) # Current objective function value: 53783(1.23s) # Current objective function value: 50934(1.363s) # Current objective function value: 50869(1.498s) # Current objective function value: 35969(1.574s) # Current objective function value: 35968(2.691s) # Current objective function value: 35966(2.74s) # Current objective function value: 35965(2.805s) # Current objective function value: 35964(2.885s) # Current objective function value: 35963(2.934s) # Current objective function value: 35962(2.996s) # cleaning 2472 clauses out of 4948 with flag 5001/5001 # cleaning 4238 clauses out of 8476 with flag 11001/11001 # cleaning 5618 clauses out of 11236 with flag 18001/18001 # cleaning 6809 clauses out of 13618 with flag 26001/26001 # cleaning 7903 clauses out of 15808 with flag 35001/35001 # cleaning 8952 clauses out of 17904 with flag 45000/45000 # cleaning 9972 clauses out of 19952 with flag 56000/56000 # Current objective function value: 35961(62.154s) # cleaning 10990 clauses out of 21981 with flag 68001/68001 # cleaning 11995 clauses out of 23989 with flag 81001/81001 # Current objective function value: 35960(99.701s) # cleaning 12995 clauses out of 25993 with flag 95003/95003 # Paranoid criteria value: -12, -224 # Proof: [AbstractVariable: bsd-mailx, AbstractVariable: dnsutils, AbstractVariable: etckeeper, AbstractVariable: gsfonts, AbstractVariable: libcurl3, AbstractVariable: libmagick10, AbstractVariable: libsasl2-modules-gssapi-mit, AbstractVariable: libssh2-1, AbstractVariable: libwmf0.2-7, AbstractVariable: mailx, AbstractVariable: ocaml-ulex08, AbstractVariable: resolvconf, AbstractVariable: ant-optional, AbstractVariable: ant-optional-gcj, AbstractVariable: apache2-mpm-prefork, AbstractVariable: apache2.2-bin, AbstractVariable: apache2.2-common, AbstractVariable: aptitude-doc-ja, AbstractVariable: bison, AbstractVariable: blt, AbstractVariable: bsd-mailx, AbstractVariable: camlp4, AbstractVariable: camlp5, AbstractVariable: cli-common, AbstractVariable: darcs, AbstractVariable: dictionaries-common, AbstractVariable: dnsutils, AbstractVariable: etckeeper, AbstractVariable: fetchmail, AbstractVariable: firedns, AbstractVariable: flex, AbstractVariable: fluxbox, AbstractVariable: fontconfig-config, AbstractVariable: gcc-4.4-base, AbstractVariable: gsfonts, AbstractVariable: heirloom-mailx, AbstractVariable: hicolor-icon-theme, AbstractVariable: icedove, AbstractVariable: icedove-l10n-pt-pt, AbstractVariable: imagemagick, AbstractVariable: install-info, AbstractVariable: ledit, AbstractVariable: lesstif2, AbstractVariable: libapr1, AbstractVariable: libaprutil1, AbstractVariable: libaprutil1-dbd-sqlite3, AbstractVariable: libaprutil1-ldap, AbstractVariable: libasyncns0, AbstractVariable: libaudio-mpd-common-perl, AbstractVariable: libaudio2, AbstractVariable: libbluetooth2, AbstractVariable: libbotan-1.8.2, AbstractVariable: libbreakpoint-ruby1.8, AbstractVariable: libbuilder-ruby1.8, AbstractVariable: libc-bin, AbstractVariable: libc-dev-bin, AbstractVariable: libc6, AbstractVariable: libc6-dev, AbstractVariable: libclass-inspector-perl, AbstractVariable: libcmdparse2-ruby1.8, AbstractVariable: libconfig-tiny-perl, AbstractVariable: libcryptgps-ocaml-dev, AbstractVariable: libcurl-ocaml, AbstractVariable: libcurl-ocaml-dev, AbstractVariable: libcurl3, AbstractVariable: libdaemons-ruby1.8, AbstractVariable: libdb4.8, AbstractVariable: libdbus-1-3, AbstractVariable: libdbus-glib-1-2, AbstractVariable: libecj-java, AbstractVariable: libexif12, AbstractVariable: libexpat-ocaml, AbstractVariable: libexpat-ocaml-dev, AbstractVariable: libfeedtools-ruby1.8, AbstractVariable: libffi5, AbstractVariable: libfindlib-ocaml, AbstractVariable: libfindlib-ocaml-dev, AbstractVariable: libfirestring0.9, AbstractVariable: libflute-1.3-jfree-java, AbstractVariable: libfontconfig1, AbstractVariable: libgammu-common, AbstractVariable: libgammu3, AbstractVariable: libgcrypt11, AbstractVariable: libgcrypt11-dev, AbstractVariable: libgdiplus, AbstractVariable: libgl1-mesa-swx11, AbstractVariable: libglib2.0-0, AbstractVariable: libglib2.0-dev, AbstractVariable: libglu1-mesa, AbstractVariable: libgnutls-dev, AbstractVariable: libgnutls26, AbstractVariable: libgoocanvas-common, AbstractVariable: libgpg-error-dev, AbstractVariable: libgpg-error0, AbstractVariable: libgssapi-krb5-2, AbstractVariable: libhpricot-ruby1.8, AbstractVariable: libhunspell-1.2-0, AbstractVariable: libk5crypto3, AbstractVariable: libkrb5-3, AbstractVariable: libkrb5support0, AbstractVariable: liblog4net1.2-cil, AbstractVariable: liblog4r-ruby1.8, AbstractVariable: libloudmouth1-0, AbstractVariable: liblqr-1-0, AbstractVariable: libltdl7, AbstractVariable: libmagick10, AbstractVariable: libmagickcore3, AbstractVariable: libmagickwand3, AbstractVariable: libmarkaby-ruby1.8, AbstractVariable: libmmap-ruby1.8, AbstractVariable: libmng1, AbstractVariable: libmono-accessibility1.0-cil, AbstractVariable: libmono-corlib1.0-cil, AbstractVariable: libmono-corlib2.0-cil, AbstractVariable: libmono-data-tds1.0-cil, AbstractVariable: libmono-data-tds2.0-cil, AbstractVariable: libmono-dev, AbstractVariable: libmono-posix1.0-cil, AbstractVariable: libmono-posix2.0-cil, AbstractVariable: libmono-security1.0-cil, AbstractVariable: libmono-security2.0-cil, AbstractVariable: libmono-sharpzip2.84-cil, AbstractVariable: libmono-sqlite2.0-cil, AbstractVariable: libmono-system-data1.0-cil, AbstractVariable: libmono-system-data2.0-cil, AbstractVariable: libmono-system-runtime2.0-cil, AbstractVariable: libmono-system-web1.0-cil, AbstractVariable: libmono-system-web2.0-cil, AbstractVariable: libmono-system1.0-cil, AbstractVariable: libmono-system2.0-cil, AbstractVariable: libmono-winforms1.0-cil, AbstractVariable: libmono0, AbstractVariable: libmono2.0-cil, AbstractVariable: libmysqlclient16, AbstractVariable: libncurses-ruby1.8, AbstractVariable: libncurses5, AbstractVariable: libncurses5-dev, AbstractVariable: libncursesw5, AbstractVariable: libndoc1.3-cil, AbstractVariable: libneon27-gnutls, AbstractVariable: libnspr4-0d, AbstractVariable: libnss3-1d, AbstractVariable: libnunit2.4-cil, AbstractVariable: libocamlnet-ocaml, AbstractVariable: libocamlnet-ocaml-dev, AbstractVariable: libosmesa6, AbstractVariable: libpcre-ocaml, AbstractVariable: libpcre-ocaml-dev, AbstractVariable: libpcre3, AbstractVariable: libpcre3-dev, AbstractVariable: libpcrecpp0, AbstractVariable: libpgsql-ruby1.8, AbstractVariable: libpq5, AbstractVariable: libpthread-stubs0, AbstractVariable: libpthread-stubs0-dev, AbstractVariable: libpulse0, AbstractVariable: libpxp-ocaml-dev, AbstractVariable: libqt3-mt, AbstractVariable: libreadline6, AbstractVariable: libreadonly-perl, AbstractVariable: libredcloth-ruby1.8, AbstractVariable: libruby, AbstractVariable: libruby1.8-extras, AbstractVariable: libruby1.9.1, AbstractVariable: libsasl2-modules-gssapi-mit, AbstractVariable: libserf-0-0, AbstractVariable: libsqlite0, AbstractVariable: libsqlite3-0, AbstractVariable: libss2-dbg, AbstractVariable: libssh2-1, AbstractVariable: libssl0.9.8, AbstractVariable: libstdc++6, AbstractVariable: libsvn1, AbstractVariable: libsys-syslog-perl, AbstractVariable: libtasn1-3, AbstractVariable: libtasn1-3-dev, AbstractVariable: libtelepathy-glib0, AbstractVariable: libtest-classapi-perl, AbstractVariable: libuuid1, AbstractVariable: libuuidtools-ruby1.8, AbstractVariable: libwmf0.2-7, AbstractVariable: libxau-dev, AbstractVariable: libxcb-reply1, AbstractVariable: libxcb-reply1-dev, AbstractVariable: libxcb1, AbstractVariable: libxcb1-dev, AbstractVariable: libxdmcp-dev, AbstractVariable: libxml-simple-ruby, AbstractVariable: libxml2, AbstractVariable: libxmu6, AbstractVariable: libxp6, AbstractVariable: locales, AbstractVariable: m4, AbstractVariable: mailx, AbstractVariable: menu, AbstractVariable: module-assistant, AbstractVariable: mono-2.0-gac, AbstractVariable: mono-gac, AbstractVariable: mono-gmcs, AbstractVariable: mono-runtime, AbstractVariable: myspell-pt-pt, AbstractVariable: mysql-common, AbstractVariable: nagios-plugins-standard, AbstractVariable: nant, AbstractVariable: ncurses-bin, 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: openafs-client, AbstractVariable: openafs-modules-source, AbstractVariable: php-file, AbstractVariable: php-pear, AbstractVariable: procps, AbstractVariable: pterm, AbstractVariable: python-central, AbstractVariable: python-gammu, AbstractVariable: python-pkg-resources, AbstractVariable: python-setuptools, AbstractVariable: python-tk, AbstractVariable: python2.6, AbstractVariable: python2.6-minimal, AbstractVariable: rails, AbstractVariable: rake, AbstractVariable: rdoc, AbstractVariable: resolvconf, AbstractVariable: ruby1.9.1, AbstractVariable: softhsm-common, AbstractVariable: subversion, AbstractVariable: tcl8.4, AbstractVariable: tk8.4, AbstractVariable: x11proto-core-dev] # starts : 102 # conflicts : 104437 # decisions : 590899 # propagations : 236725544 # inspects : 508633859 # learnt literals : 76 # learnt binary clauses : 274 # learnt ternary clauses : 206 # learnt clauses : 104360 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 834762 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 10 # 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) : 2.372237137989779E7 # non guided choices 34524 # learnt constraints type #Solving done (111.596s). #Solution contains:805