# Checking available version of Java # Java(TM) SE Runtime Environment (build 1.6.0_22-b04) # Running really p2cudf # Solver launched on Thu Aug 25 15:47:01 CEST 2011 # Using input file /home/misc2010/data/2011/incremental/s/rand298.cudf # Using ouput file /home/misc2010/tmp/201108251442/p2cudf-paranoid-1.13/rand298.cudf.s.result # Objective function -removed,-changed # Timeout 280s # java.runtime.name Java(TM) SE Runtime Environment # java.vm.name Java HotSpot(TM) Server VM # java.vm.version 17.1-b03 # java.vm.vendor Sun Microsystems Inc. # sun.arch.data.model 32 # java.version 1.6.0_22 # os.name Linux # os.version 2.6.18-6-xen-amd64 # os.arch i386 # Free memory 705643136 # Max memory 709558272 # Total memory 709558272 # Number of processors 1 # Parsing ... # Time to parse:1649 # Parsing done (1.651s). # Solving ... # Request size: 992 # Number of packages after slice: 1300 # Slice efficiency: 92% # --- Begin Solver configuration --- # org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@143c8b3 # 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 # Simple reason simplification # luby style (SATZ_rand, TiniSAT) restarts strategy with factor 512 # Glucose learned constraints deletion strategy # timeout=280s # DB Simplification allowed=false # --- End Solver configuration --- # Optimization function: User defined:-removed,-changed # criteria removed size is 950 using new vars 2251 to 3201 # criteria changed size is 1299 using new vars 3201 to 4500 # p cnf 4499 15527 # Current objective function value: 48(0.141s) # Found optimal criterion number 1 # Current objective function value: 90(0.183s) # Found optimal solution for the last criterion # -removed criteria value: 48 # Removed packages: [freeglut3, gnome, gnome-desktop-environment, gnome-gv, kaddressbook, kaddressbook-plugins, kalarm, kandy, kanjidic, karm, kbugbuster, kde, kde-amusements, kde-devel, kde-devel-extras, kdeaddons, kdebase-dev, kdeedu, kdelibs4-dev, kdelirc, kdepim, kdepim-wizards, kdesdk, kdeutils, kitchensync, kiten, kmail, kmailcvt, knode, knotes, konsolekalendar, kontact, korganizer, kpilot, kspy, ksync, ktnef, libglut3, libkcal2a, libkdepim1, libkonq4-dev, libkpimexchange1, libkpimidentities1, liblablgl-ocaml, liblablgl-ocaml-dev, liblablgtk2-ocaml-dev, libmlgtk-ocaml, libmlgtk-ocaml-dev] # -changed criteria value: 90 # Changed packages: [freeglut3, gnome, gnome-desktop-environment, gnome-gv, gnunet, gnunet-gtk, iiimf-htt-server, kaddressbook, kaddressbook-plugins, kalarm, kandy, kanjidic, karm, kbugbuster, kde, kde-amusements, kde-devel, kde-devel-extras, kdeaddons, kdebase-dev, kdeedu, kdelibs3-bin, kdelibs4-dev, kdelirc, kdepim, kdepim-wizards, kdesdk, kdeutils, kitchensync, kiten, kmail, kmailcvt, knode, knotes, konsolekalendar, kontact, korganizer, kpilot, kspy, ksync, ktnef, libatspi1.0-0, libauthen-pam-perl, libboost-dev, libboost-serialization-dev, libdb4.3, libdps-dev, libexif-dev, libextractor1, libgail-gnome-dbg, libgail-gnome-module, libglut3, libgmp3, libgnuift0, libgnuift0-dev, libiiimp0, libjasper-1.701-dev, libkcal2a, libkdepim1, libkonq4-dev, libkpimexchange1, libkpimidentities1, liblablgl-ocaml, liblablgl-ocaml-dev, liblablgtk2-ocaml-dev, libltdl3, libmagick6-dev, libmlgtk-ocaml, libmlgtk-ocaml-dev, libmrml0, libnet-ssleay-perl, libsqlite3-0, libtdb1, libtiff4-dev, libtiffxx0, libwmf-dev, libxmuu-dev, libxp-dev, libxpm-dev, libxtrap-dev, libxtst-dev, module-init-tools, openssl, pm-dev, python2.4, python2.4-logilab-common, rsh-redone-server, usermin, usermin-proc, xlibs-dev] # starts : 2 # conflicts : 18 # decisions : 6835 # propagations : 34553 # inspects : 103986 # shortcuts : 0 # learnt literals : 17 # learnt binary clauses : 0 # learnt ternary clauses : 0 # learnt constraints : 0 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 0 # 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) : 215956.25 # non guided choices 1108 # learnt constraints type # Solving done (2.022s). # The solution found IS optimal # Solution contains:944