ABORT HEAD is now at 0e68ffa 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 00:13:05 UTC 2010 #Using input file /home/misc2010/data/2010/impossible/randfa4522.cudf #Using ouput file /home/misc2010/tmp/201007051419/p2cudf-trendy-1.6/randfa4522.cudf.impossible.result #Objective function trendy #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:3139 #Parsing done (3.14s). #Solving ... #Request size: 2938 #Number of packages after slice: 15416 #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@20be79 # 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, trendy # p cnf 36124 183675 # Current objective function value: 13594285337(2.419s) # Current objective function value: 10923839538(4.507s) # Current objective function value: 10116015230(5.836s) # Current objective function value: 9801734295(6.941s) # Current objective function value: 9756855943(7.558s) # Current objective function value: 9577380483(8.153s) # Current objective function value: 9554889233(8.671s) # cleaning 2401 clauses out of 4801 with flag 5000/5000 # cleaning 4199 clauses out of 8398 with flag 11001/11001 # cleaning 5591 clauses out of 11196 with flag 18000/18000 # cleaning 6801 clauses out of 13605 with flag 26000/26000 # cleaning 7903 clauses out of 15805 with flag 35001/35001 # cleaning 8941 clauses out of 17900 with flag 45000/45000 # cleaning 9969 clauses out of 19959 with flag 56000/56000 # cleaning 10989 clauses out of 21991 with flag 68001/68001 # cleaning 11995 clauses out of 24002 with flag 81001/81001 # cleaning 12991 clauses out of 26007 with flag 95001/95001 # cleaning 14009 clauses out of 28017 with flag 110002/110002 # cleaning 14988 clauses out of 30007 with flag 126001/126001 # cleaning 16008 clauses out of 32019 with flag 143001/143001 # cleaning 17003 clauses out of 34011 with flag 161001/161001 # cleaning 18000 clauses out of 36007 with flag 180000/180000 # cleaning 18995 clauses out of 38006 with flag 200000/200000 # cleaning 20001 clauses out of 40011 with flag 221000/221000 # cleaning 20983 clauses out of 42013 with flag 243003/243003 # cleaning 21999 clauses out of 44027 with flag 266000/266000 # cleaning 22995 clauses out of 46029 with flag 290001/290001 # cleaning 24003 clauses out of 48032 with flag 315000/315000