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 19:12:50 UTC 2010 #Using input file /home/misc2010/data/2010/impossible/rand81406f.cudf #Using ouput file /home/misc2010/tmp/201007051419/p2cudf-paranoid-1.6/rand81406f.cudf.impossible.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:3438 #Parsing done (3.439s). #Solving ... #Request size: 801 #Number of packages after slice: 15464 #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@2f1921 # 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 28106 153341 # Current objective function value: 190200(1.326s) # Current objective function value: 161670(1.604s) # Current objective function value: 76145(1.866s) # Current objective function value: 76144(2.623s) # Current objective function value: 76143(2.766s) # Current objective function value: 76142(2.922s) # Current objective function value: 76141(3.065s) # Current objective function value: 76140(4.08s) # Paranoid criteria value: -16, -108 # Proof: [AbstractVariable: apache2-common, AbstractVariable: base-config, AbstractVariable: ethereal-common, AbstractVariable: gcc-doc, AbstractVariable: gnome-terminal, AbstractVariable: gnome-themes, AbstractVariable: gtk2-engines-redmond95, AbstractVariable: libdigest-hmac-perl, AbstractVariable: libgtk2.0-dev, AbstractVariable: libmail-spf-query-perl, AbstractVariable: libnet-dns-perl, AbstractVariable: librsvg2-common, AbstractVariable: razor, AbstractVariable: ssl-cert, AbstractVariable: tasksel, AbstractVariable: xfonts-base, AbstractVariable: apache2-common, AbstractVariable: apache2-mpm-prefork, AbstractVariable: apache2.2-common, AbstractVariable: aptitude-doc-es, AbstractVariable: aspell-pl, AbstractVariable: base-config, AbstractVariable: dbconfig-common, AbstractVariable: ethereal, AbstractVariable: ethereal-common, AbstractVariable: fontconfig, AbstractVariable: fontconfig-config, AbstractVariable: gcc-doc, AbstractVariable: gnome-terminal, AbstractVariable: gnome-themes, AbstractVariable: gtk2-engines-redmond95, AbstractVariable: initrd-tools, AbstractVariable: iswedish, AbstractVariable: libapache2-mod-php4, AbstractVariable: libapr1, AbstractVariable: libaprutil1, AbstractVariable: libatk1.0-0, AbstractVariable: libatk1.0-dev, AbstractVariable: libc6, AbstractVariable: libc6-dev, AbstractVariable: libcairo2, AbstractVariable: libcairo2-dev, AbstractVariable: libcroco3, AbstractVariable: libdb4.4, AbstractVariable: libdevmapper1.02, AbstractVariable: libdigest-hmac-perl, AbstractVariable: libfontconfig1, AbstractVariable: libfontconfig1-dev, AbstractVariable: libfreetype6, AbstractVariable: libfreetype6-dev, AbstractVariable: libgcrypt11, AbstractVariable: libgd2-xpm, AbstractVariable: libglib2.0-0, AbstractVariable: libglib2.0-data, AbstractVariable: libglib2.0-dev, AbstractVariable: libgpg-error0, AbstractVariable: libgsf-1-114, AbstractVariable: libgsf-1-common, AbstractVariable: libgtk2.0-0, AbstractVariable: libgtk2.0-common, AbstractVariable: libgtk2.0-dev, AbstractVariable: libice-dev, AbstractVariable: libjs-yui, AbstractVariable: libkrb53, AbstractVariable: libmail-spf-query-perl, AbstractVariable: libncurses5, AbstractVariable: libncurses5-dev, AbstractVariable: libnet-dns-perl, AbstractVariable: libpango1.0-0, AbstractVariable: libpango1.0-common, AbstractVariable: libpango1.0-dev, AbstractVariable: libpng12-0, AbstractVariable: libpng12-dev, AbstractVariable: libpq4, AbstractVariable: librsvg2-2, AbstractVariable: librsvg2-common, AbstractVariable: libselinux1, AbstractVariable: libsepol1, AbstractVariable: libsm-dev, AbstractVariable: libsqlite0, AbstractVariable: libsqlite3-0, AbstractVariable: libssl0.9.8, AbstractVariable: libtool, AbstractVariable: libwbclient0, AbstractVariable: libxfixes3, AbstractVariable: libxinerama1, AbstractVariable: libxml++1.0, AbstractVariable: libxml2, AbstractVariable: libxslt1.1, AbstractVariable: locales, AbstractVariable: lsb-base, AbstractVariable: org-mode, AbstractVariable: php-cache-lite, AbstractVariable: php-http-request, AbstractVariable: php-net-checkip, AbstractVariable: php-net-socket, AbstractVariable: php-net-url, AbstractVariable: php-pear, AbstractVariable: php4-common, AbstractVariable: php5-cgi, AbstractVariable: php5-cli, AbstractVariable: php5-common, AbstractVariable: php5-gd, AbstractVariable: php5-sqlite, AbstractVariable: python-celementtree, AbstractVariable: python2.3-celementtree, AbstractVariable: python2.3-elementtree, AbstractVariable: razor, AbstractVariable: serendipity, AbstractVariable: skkdic-cdb, AbstractVariable: smarty, AbstractVariable: sqlite, AbstractVariable: ssh, AbstractVariable: ssl-cert, AbstractVariable: tasksel, AbstractVariable: tcl8.4, AbstractVariable: tk8.4, AbstractVariable: ttf-aenigma, AbstractVariable: ttf-dejavu-core, AbstractVariable: tzdata, AbstractVariable: vigor, AbstractVariable: wireshark, AbstractVariable: wireshark-common, AbstractVariable: xfonts-base] # starts : 17 # conflicts : 1758 # decisions : 187685 # propagations : 4622660 # inspects : 17136506 # learnt literals : 34 # learnt binary clauses : 98 # learnt ternary clauses : 77 # learnt clauses : 1723 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 4158 # 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) : 3335252.5252525257 # non guided choices 56582 # learnt constraints type #Solving done (8.106s). #Solution contains:768