# 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 18:21:41 CEST 2011 # Using input file /home/misc2010/data/2011/dudf-real/e2f6303a-4fe9-11e0-aa4f-00163e1e087d.cudf # Using ouput file /home/misc2010/tmp/201108251442/p2cudf-paranoid-1.13/e2f6303a-4fe9-11e0-aa4f-00163e1e087d.cudf.dudf-real.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:2094 # Parsing done (2.097s). # Solving ... # Request size: 2362 # Number of packages after slice: 4305 # Slice efficiency: 90% # --- Begin Solver configuration --- # org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@6d084b # 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 2337 using new vars 6643 to 8980 # criteria changed size is 2935 using new vars 8980 to 11915 # p cnf 11914 45242 # Current objective function value: 4(0.258s) # Found optimal criterion number 1 # Current objective function value: 130(0.366s) # Current objective function value: 52(0.522s) # Found optimal solution for the last criterion # -removed criteria value: 4 # Removed packages: [openoffice.org-base-core, openoffice.org-core, openoffice.org-evolution, openoffice.org-report-builder-bin] # -changed criteria value: 52 # Changed packages: [libhyphen0, libraptor2-0, librasqal3, librdf0, libreoffice, libreoffice-base, libreoffice-base-core, libreoffice-calc, libreoffice-common, libreoffice-core, libreoffice-draw, libreoffice-filter-binfilter, libreoffice-filter-mobiledev, libreoffice-gcj, libreoffice-gnome, libreoffice-gtk, libreoffice-impress, libreoffice-java-common, libreoffice-math, libreoffice-officebean, libreoffice-report-builder-bin, libreoffice-style-galaxy, libreoffice-style-tango, libreoffice-writer, libwpd-0.9-9, libwpg-0.2-2, libwps-0.2-2, mythes-en-us, openoffice.org, openoffice.org-base, openoffice.org-base-core, openoffice.org-calc, openoffice.org-common, openoffice.org-core, openoffice.org-draw, openoffice.org-evolution, openoffice.org-filter-binfilter, openoffice.org-gcj, openoffice.org-gnome, openoffice.org-gtk, openoffice.org-impress, openoffice.org-math, openoffice.org-officebean, openoffice.org-report-builder-bin, openoffice.org-style-galaxy, openoffice.org-style-tango, openoffice.org-thesaurus-en-us, openoffice.org-writer, python-uno, ttf-opensymbol, uno-libs3, ure] # starts : 2 # conflicts : 2 # decisions : 8122 # propagations : 31256 # inspects : 103555 # shortcuts : 0 # learnt literals : 1 # learnt binary clauses : 1 # learnt ternary clauses : 0 # learnt constraints : 1 # 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) : 529762.7118644068 # non guided choices 5424 # learnt constraints type # Solving done (2.836s). # The solution found IS optimal # Solution contains:2359