HEAD is now at 2b6ae8b initial deployement # 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:03:51 CEST 2011 # Using input file /home/misc2010/data/2011/dudf-random/rand733.cudf # Using ouput file /home/misc2010/tmp/201108251442/p2cudf-paranoid-1.13/rand733.cudf.dudf-random.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:2255 # Parsing done (2.258s). # Solving ... # Request size: 1621 # Number of packages after slice: 2075 # Slice efficiency: 95% # --- Begin Solver configuration --- # org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@1feca64 # 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 1572 using new vars 3648 to 5220 # criteria changed size is 1746 using new vars 5220 to 6966 # p cnf 6965 17811 # Current objective function value: 31(0.142s) # Found optimal criterion number 1 # Current objective function value: 84(0.252s) # Current objective function value: 61(0.391s) # Current objective function value: 60(0.482s) # Found optimal solution for the last criterion # -removed criteria value: 31 # Removed packages: [gnome-mime-data, libbuddy-ocaml-dev, libgnomevfs2-0, libgnomevfs2-common, libgnomevfs2-dev, libgnomevfs2-extra, libmaven-archiver-java, libmaven-clean-plugin-java, libmaven-compiler-plugin-java, libmaven-dependency-tree-java, libmaven-doxia-tools-java, libmaven-enforcer-plugin-java, libmaven-file-management-java, libmaven-filtering-java, libmaven-install-plugin-java, libmaven-jar-plugin-java, libmaven-plugin-tools-java, libmaven-reporting-impl-java, libmaven-resources-plugin-java, libmaven-shade-plugin-java, libmaven-shared-io-java, libmaven-site-plugin-java, libmaven2-core-java, libplexus-ant-factory-java, libplexus-bsh-factory-java, libplexus-cipher-java, libplexus-container-default-java, libplexus-sec-dispatcher-java, maven-debian-helper, maven2, ssh] # -changed criteria value: 60 # Changed packages: [gnome-mime-data, kio-ftps, libbuddy-ocaml-dev, libclucene0ldbl, libgnomevfs2-0, libgnomevfs2-common, libgnomevfs2-dev, libgnomevfs2-extra, libkdecore5, libkdeui5, libkio5, libmaven-archiver-java, libmaven-clean-plugin-java, libmaven-compiler-plugin-java, libmaven-dependency-tree-java, libmaven-doxia-tools-java, libmaven-enforcer-plugin-java, libmaven-file-management-java, libmaven-filtering-java, libmaven-install-plugin-java, libmaven-jar-plugin-java, libmaven-plugin-tools-java, libmaven-reporting-impl-java, libmaven-resources-plugin-java, libmaven-shade-plugin-java, libmaven-shared-io-java, libmaven-site-plugin-java, libmaven2-core-java, libplexus-ant-factory-java, libplexus-bsh-factory-java, libplexus-cipher-java, libplexus-container-default-java, libplexus-sec-dispatcher-java, libqt4-core, libqt4-gui, libsolid4, libstreamanalyzer0, libstreams0, maven-debian-helper, maven2, mercurial, mercurial-common, python-setuptools, python-zope.component, python-zope.configuration, python-zope.copy, python-zope.event, python-zope.exceptions, python-zope.hookable, python-zope.i18nmessageid, python-zope.location, python-zope.proxy, python-zope.schema, python-zope.security, python-zope.testing, rlplot, ssh, trac, trac-mercurial, ttf-gujarati-fonts] # starts : 4 # conflicts : 14 # decisions : 12014 # propagations : 56543 # inspects : 138484 # shortcuts : 0 # learnt literals : 13 # 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) : 911983.8709677419 # non guided choices 4762 # learnt constraints type # Solving done (2.253s). # The solution found IS optimal # Solution contains:1570