HEAD is now at 5df24db initial deployement # Checking available version of Java # Java(TM) SE Runtime Environment (build 1.6.0_12-b04) # Running really p2cudf #Solver launched on Mon Jul 05 09:53:24 UTC 2010 #Using input file /home/misc2010/data/2010/easy/randeb343c.cudf #Using ouput file /home/misc2010/tmp/201007050905/p2cudf-paranoid-1.6/randeb343c.cudf.easy.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 11.2-b01 #java.vm.vendor Sun Microsystems Inc. #sun.arch.data.model 32 #java.version 1.6.0_12 #os.name Linux #os.version 2.6.18-6-xen-amd64 #os.arch i386 #Free memory 721951928 #Max memory 725876736 #Total memory 725876736 #Number of processors 1 #Parsing ... #Time to parse:2222 #Parsing done (2.222s). #Solving ... #Request size: 1665 #Number of packages after slice: 3085 #Slice efficiency: 91% ## 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@1aa57fb # 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 10450 32781 # Current objective function value: 147581(0.6s) # Current objective function value: 147580(0.843s) # Current objective function value: 147578(0.96s) # Paranoid criteria value: -54, -104 # Proof: [AbstractVariable: acpi-support, AbstractVariable: arno-iptables-firewall, AbstractVariable: avidemux, AbstractVariable: avidemux-plugins, AbstractVariable: deskbar-applet, AbstractVariable: f-spot, AbstractVariable: gecko-mediaplayer, AbstractVariable: gnome-about, AbstractVariable: gnome-accessibility, AbstractVariable: gnome-applets, AbstractVariable: gnome-core, AbstractVariable: gnome-mag, AbstractVariable: gnome-mplayer, AbstractVariable: gnome-orca, AbstractVariable: gnome-panel, AbstractVariable: gnome-screensaver, AbstractVariable: gnome-session, AbstractVariable: guake, AbstractVariable: gvfs-backends, AbstractVariable: gwibber, AbstractVariable: hplip, AbstractVariable: iptables, AbstractVariable: libgphoto2-2, AbstractVariable: libgphoto2-port0, AbstractVariable: libmjpegtools-1.9, AbstractVariable: liboobs-1-4, AbstractVariable: libsane, AbstractVariable: libsdl-image1.2, AbstractVariable: libsdl-mixer1.2, AbstractVariable: libsdl-ttf2.0-0, AbstractVariable: libsdl1.2debian, AbstractVariable: libsdl1.2debian-alsa, AbstractVariable: libsmpeg0, AbstractVariable: libsvga1, AbstractVariable: libx86-1, AbstractVariable: miro, AbstractVariable: mjpegtools, AbstractVariable: mplayer, AbstractVariable: openoffice.org-gnome, AbstractVariable: openvpn, AbstractVariable: openvpn-blacklist, AbstractVariable: postr, AbstractVariable: python-gconf, AbstractVariable: python-gnome2, AbstractVariable: python-nautilus, AbstractVariable: python-pyatspi, AbstractVariable: python-pygame, AbstractVariable: rhythmbox, AbstractVariable: rhythmbox-plugins, AbstractVariable: sane-utils, AbstractVariable: skype, AbstractVariable: vbetool, AbstractVariable: vlc, AbstractVariable: xsane, AbstractVariable: acpi-support, AbstractVariable: aptitude-doc-fr, AbstractVariable: arno-iptables-firewall, AbstractVariable: aspell, AbstractVariable: aspell-uk, AbstractVariable: avidemux, AbstractVariable: avidemux-plugins, AbstractVariable: bogofilter, AbstractVariable: bogofilter-common, AbstractVariable: bogofilter-sqlite, AbstractVariable: csound, AbstractVariable: csound-gui, AbstractVariable: deskbar-applet, AbstractVariable: edos-rpmcheck, AbstractVariable: f-spot, AbstractVariable: gambas2-gb-form, AbstractVariable: gambas2-gb-form-dialog, AbstractVariable: gambas2-gb-gtk, AbstractVariable: gambas2-gb-gui, AbstractVariable: gambas2-gb-qt, AbstractVariable: gambas2-gb-settings, AbstractVariable: gambas2-runtime, AbstractVariable: gecko-mediaplayer, AbstractVariable: gnat-4.4-base, AbstractVariable: gnome-about, AbstractVariable: gnome-accessibility, AbstractVariable: gnome-applets, AbstractVariable: gnome-core, AbstractVariable: gnome-mag, AbstractVariable: gnome-mplayer, AbstractVariable: gnome-orca, AbstractVariable: gnome-panel, AbstractVariable: gnome-screensaver, AbstractVariable: gnome-session, AbstractVariable: guake, AbstractVariable: gvfs-backends, AbstractVariable: gwibber, AbstractVariable: hplip, AbstractVariable: iptables, AbstractVariable: lesstif2, AbstractVariable: libboost-date-time1.39.0, AbstractVariable: libboost-filesystem1.39-dev, AbstractVariable: libboost-filesystem1.39.0, AbstractVariable: libboost-serialization1.39-dev, AbstractVariable: libboost-serialization1.39.0, AbstractVariable: libboost-system1.39-dev, AbstractVariable: libboost-system1.39.0, AbstractVariable: libboost-thread1.39.0, AbstractVariable: libboost-wave1.39-dev, AbstractVariable: libboost-wave1.39.0, AbstractVariable: libboost1.39-dev, AbstractVariable: libcsound64-5.2, AbstractVariable: libfltk1.1, AbstractVariable: libfluidsynth1, AbstractVariable: libgnat-4.4, AbstractVariable: libgphoto2-2, AbstractVariable: libgphoto2-port0, AbstractVariable: libgsf-gnome-1-114, AbstractVariable: libidzebra-2.0-0, AbstractVariable: libidzebra-2.0-mod-grs-regx, AbstractVariable: liblash2, AbstractVariable: liblo7, AbstractVariable: libmjpegtools-1.9, AbstractVariable: liboobs-1-4, AbstractVariable: libportmidi0, AbstractVariable: libqt3-mt, AbstractVariable: libsane, AbstractVariable: libsdl-image1.2, AbstractVariable: libsdl-mixer1.2, AbstractVariable: libsdl-ttf2.0-0, AbstractVariable: libsdl1.2debian, AbstractVariable: libsdl1.2debian-alsa, AbstractVariable: libsmpeg0, AbstractVariable: libstk0c2a, AbstractVariable: libsvga1, AbstractVariable: libx86-1, AbstractVariable: libxbae-dev, AbstractVariable: libxbae4, AbstractVariable: libxp6, AbstractVariable: libyaz3, AbstractVariable: lxsession, AbstractVariable: miro, AbstractVariable: mjpegtools, AbstractVariable: mpg321, AbstractVariable: mplayer, AbstractVariable: music123, AbstractVariable: openoffice.org-gnome, AbstractVariable: openvpn, AbstractVariable: openvpn-blacklist, AbstractVariable: perlmagick, AbstractVariable: postr, AbstractVariable: python-gconf, AbstractVariable: python-gnome2, AbstractVariable: python-nautilus, AbstractVariable: python-nmap, AbstractVariable: python-pyatspi, AbstractVariable: python-pygame, AbstractVariable: rhythmbox, AbstractVariable: rhythmbox-plugins, AbstractVariable: sane-utils, AbstractVariable: skype, AbstractVariable: vbetool, AbstractVariable: vlc, AbstractVariable: xsane] # starts : 4 # conflicts : 85 # decisions : 19201 # propagations : 137571 # inspects : 319892 # learnt literals : 11 # learnt binary clauses : 4 # learnt ternary clauses : 3 # learnt clauses : 73 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 46 # 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) : 1146425.0 # non guided choices 7982 # learnt constraints type #Solving done (3.38s). #Solution contains:1617