From 98e1e8fdd1936f266314aa2aa652b46d27611b0f Mon Sep 17 00:00:00 2001
From: Carlo Baldassi <carlobaldassi@gmail.com>
Date: Fri, 5 Jan 2018 02:36:09 +0100
Subject: [PATCH] Add backtracking to max-sum, improve greedy solver

With this change, the solver is now exact, i.e. it should always
find a solution if it exists, and fail only when it
doesn't, producing a reasonable log trace in that case.
(Optimality is still based on a heuristic, unless the solution
is found by the greedy solver, which is quite improved as well
anyway.)
---
 bin/Pkg2/types.jl          |   1 -
 src/GraphType.jl           | 295 ++++++++++++++++++-----
 src/Resolve.jl             | 171 +++++++------
 src/resolve/FieldValues.jl |  24 +-
 src/resolve/MaxSum.jl      | 477 ++++++++++++++++++++++---------------
 test/NastyGenerator.jl     |  96 ++++++++
 test/resolve.jl            |  43 ++--
 7 files changed, 747 insertions(+), 360 deletions(-)
 create mode 100644 test/NastyGenerator.jl

diff --git a/bin/Pkg2/types.jl b/bin/Pkg2/types.jl
index 390d358bb9048..4a52b2940542b 100644
--- a/bin/Pkg2/types.jl
+++ b/bin/Pkg2/types.jl
@@ -5,7 +5,6 @@ module Types
 export VersionInterval, VersionSet
 import Base: show, isempty, in, intersect, union!, union, ==, hash, copy, deepcopy_internal
 
-import Pkg3.equalto
 import Pkg3.iswindows
 
 struct VersionInterval
diff --git a/src/GraphType.jl b/src/GraphType.jl
index 53d8c810cbf0e..d526548ec9ddc 100644
--- a/src/GraphType.jl
+++ b/src/GraphType.jl
@@ -6,7 +6,8 @@ using ..Types
 import ..Types.uuid_julia
 import Pkg3.equalto
 
-export Graph, ResolveLog, add_reqs!, add_fixed!, simplify_graph!, get_resolve_log, showlog
+export Graph, ResolveLog, add_reqs!, add_fixed!, simplify_graph!, simplify_graph_soft!,
+       get_resolve_log, showlog, push_snapshot!, pop_snapshot!, wipe_snapshots!
 
 # The ResolveLog is used to keep track of events that take place during the
 # resolution process. We use one ResolveLogEntry per package, and record all events
@@ -58,14 +59,17 @@ mutable struct ResolveLog
     #        heuristics have been employed
     exact::Bool
 
+    # verbose: print global events messages on screen
+    verbose::Bool
+
     # UUID to names
     uuid_to_name::Dict{UUID,String}
 
-    function ResolveLog(uuid_to_name::Dict{UUID,String})
+    function ResolveLog(uuid_to_name::Dict{UUID,String}, verbose::Bool = false)
         journal = ResolveJournal()
         init = ResolveLogEntry(journal, UUID0, "")
         globals = ResolveLogEntry(journal, UUID0, "Global events:")
-        return new(init, globals, Dict(), journal, true, uuid_to_name)
+        return new(init, globals, Dict(), journal, true, verbose, uuid_to_name)
     end
 end
 
@@ -121,7 +125,8 @@ mutable struct GraphData
             versions::Dict{UUID,Set{VersionNumber}},
             deps::Dict{UUID,Dict{VersionRange,Dict{String,UUID}}},
             compat::Dict{UUID,Dict{VersionRange,Dict{String,VersionSpec}}},
-            uuid_to_name::Dict{UUID,String}
+            uuid_to_name::Dict{UUID,String};
+            verbose::Bool = false
         )
         # generate pkgs
         pkgs = sort!(collect(keys(versions)))
@@ -145,7 +150,7 @@ mutable struct GraphData
         eq_classes = Dict(pkgs[p0] => Dict(eq_vn(v0,p0) => Set([eq_vn(v0,p0)]) for v0 = 1:spp[p0]) for p0 = 1:np)
 
         # the resolution log is actually initialized below
-        rlog = ResolveLog(uuid_to_name)
+        rlog = ResolveLog(uuid_to_name, verbose)
 
         data = new(pkgs, np, spp, pdict, pvers, vdict, uuid_to_name, pruned, eq_classes, rlog)
 
@@ -170,16 +175,6 @@ mutable struct GraphData
     end
 end
 
-
-@enum DepDir FORWARD BACKWARDS BIDIR NONE
-
-function update_depdir(dd0::DepDir, dd1::DepDir)
-    dd0 == dd1 && return dd0
-    dd0 == NONE && return dd1
-    dd1 == NONE && return dd0
-    return BIDIR
-end
-
 mutable struct Graph
     # data:
     #   stores all the structures required to map between
@@ -202,10 +197,6 @@ mutable struct Graph
     #   spp1 is the number of states of p1.
     gmsk::Vector{Vector{BitMatrix}}
 
-    # dependency direction:
-    #   keeps track of which direction the dependency goes.
-    gdir::Vector{Vector{DepDir}}
-
     # constraints:
     #   a mask of allowed states for each package (e.g. to express
     #   requirements)
@@ -225,6 +216,13 @@ mutable struct Graph
     #   used to avoid returning them in the solution
     fix_inds::Set{Int}
 
+    ignored::BitVector
+
+    # stack of constraints/ignored packages:
+    #   allows to keep a sort of "versioning" of the constraints
+    #   such that the solver can implement tentative solutions
+    solve_stack::Vector{Tuple{Vector{BitVector},BitVector}}
+
     # states per package: same as in GraphData
     spp::Vector{Int}
 
@@ -237,13 +235,14 @@ mutable struct Graph
             compat::Dict{UUID,Dict{VersionRange,Dict{String,VersionSpec}}},
             uuid_to_name::Dict{UUID,String},
             reqs::Requires = Requires(),
-            fixed::Dict{UUID,Fixed} = Dict{UUID,Fixed}(uuid_julia=>Fixed(VERSION))
+            fixed::Dict{UUID,Fixed} = Dict{UUID,Fixed}(uuid_julia=>Fixed(VERSION));
+            verbose::Bool = false
         )
 
         extra_uuids = union(keys(reqs), keys(fixed), map(fx->keys(fx.requires), values(fixed))...)
         extra_uuids ⊆ keys(versions) || error("unknown UUID found in reqs/fixed") # TODO?
 
-        data = GraphData(versions, deps, compat, uuid_to_name)
+        data = GraphData(versions, deps, compat, uuid_to_name, verbose = verbose)
         pkgs, np, spp, pdict, pvers, vdict, rlog = data.pkgs, data.np, data.spp, data.pdict, data.pvers, data.vdict, data.rlog
 
         extended_deps = [[Dict{Int,BitVector}() for v0 = 1:(spp[p0]-1)] for p0 = 1:np]
@@ -264,6 +263,7 @@ mutable struct Graph
                     haskey(n2u, name) || error("Unknown package $name found in the compatibility requirements of $(pkgID(pkgs[p0], uuid_to_name))")
                     uuid = n2u[name]
                     p1 = pdict[uuid]
+                    p1 == p0 && error("Package $(pkgID(pkgs[p0], uuid_to_name)) version $vn has a dependency with itself")
                     # check conflicts instead of intersecting?
                     # (intersecting is used by fixed packages though...)
                     req_p1 = get!(req, p1) do; VersionSpec() end
@@ -275,14 +275,12 @@ mutable struct Graph
                 get!(req, pdict[uuid]) do; VersionSpec() end
             end
             # Translate the requirements into bit masks
-            # req_msk = Dict(p1 => BitArray(pvers[p1][v1] ∈ vs for v1 = 0:(spp[p1]-1)) for (p1,vs) in req)
             req_msk = Dict(p1 => (pvers[p1][1:(spp[p1]-1)] .∈ vs) for (p1,vs) in req)
             extended_deps[p0][v0] = req_msk
         end
 
         gadj = [Int[] for p0 = 1:np]
         gmsk = [BitMatrix[] for p0 = 1:np]
-        gdir = [DepDir[] for p0 = 1:np]
         gconstr = [trues(spp[p0]) for p0 = 1:np]
         adjdict = [Dict{Int,Int}() for p0 = 1:np]
 
@@ -307,14 +305,9 @@ mutable struct Graph
 
                 push!(gmsk[p0], bm)
                 push!(gmsk[p1], bmt)
-
-                push!(gdir[p0], FORWARD)
-                push!(gdir[p1], BACKWARDS)
             else
                 bm = gmsk[p0][j0]
                 bmt = gmsk[p1][j1]
-                gdir[p0][j0] = update_depdir(gdir[p0][j0], FORWARD)
-                gdir[p1][j1] = update_depdir(gdir[p1][j1], BACKWARDS)
             end
 
             for v1 = 1:(spp[p1]-1)
@@ -329,7 +322,10 @@ mutable struct Graph
         req_inds = Set{Int}()
         fix_inds = Set{Int}()
 
-        graph = new(data, gadj, gmsk, gdir, gconstr, adjdict, req_inds, fix_inds, spp, np)
+        ignored = falses(np)
+        solve_stack = Tuple{Vector{BitVector},BitVector}[]
+
+        graph = new(data, gadj, gmsk, gconstr, adjdict, req_inds, fix_inds, ignored, solve_stack, spp, np)
 
         _add_fixed!(graph, fixed)
         _add_reqs!(graph, reqs, :explicit_requirement)
@@ -346,13 +342,14 @@ mutable struct Graph
         spp = data.spp
         gadj = [copy(graph.gadj[p0]) for p0 = 1:np]
         gmsk = [[copy(graph.gmsk[p0][j0]) for j0 = 1:length(gadj[p0])] for p0 = 1:np]
-        gdir = [copy(graph.gdir[p0]) for p0 = 1:np]
         gconstr = [copy(graph.gconstr[p0]) for p0 = 1:np]
         adjdict = [copy(graph.adjdict[p0]) for p0 = 1:np]
         req_inds = copy(graph.req_inds)
         fix_inds = copy(graph.fix_inds)
+        ignored = copy(graph.ignored)
+        solve_stack = [([copy(gc0) for gc0 in sav_gconstr],copy(sav_ignored)) for (sav_gconstr,sav_ignored) in graph.solve_stack]
 
-        return new(data, gadj, gmsk, gdir, gconstr, adjdict, req_inds, fix_inds, spp, np)
+        return new(data, gadj, gmsk, gconstr, adjdict, req_inds, fix_inds, ignored, solve_stack, spp, np)
     end
 end
 
@@ -430,11 +427,12 @@ function check_consistency(graph::Graph)
     spp = graph.spp
     gadj = graph.gadj
     gmsk = graph.gmsk
-    gdir = graph.gdir
     gconstr = graph.gconstr
     adjdict = graph.adjdict
     req_inds = graph.req_inds
     fix_inds = graph.fix_inds
+    ignored = graph.ignored
+    solve_stack = graph.solve_stack
     data = graph.data
     pkgs = data.pkgs
     pdict = data.pdict
@@ -443,9 +441,10 @@ function check_consistency(graph::Graph)
     pruned = data.pruned
     eq_classes = data.eq_classes
     rlog = data.rlog
+    # TODO: check ignored and solve_stack
 
     @assert np ≥ 0
-    for x in [spp, gadj, gmsk, gdir, gconstr, adjdict, rlog.pool, pkgs, pdict, pvers, vdict]
+    for x in [spp, gadj, gmsk, gconstr, adjdict, ignored, rlog.pool, pkgs, pdict, pvers, vdict]
         @assert length(x) == np
     end
     for p0 = 1:np
@@ -467,11 +466,9 @@ function check_consistency(graph::Graph)
 
         gadj0 = gadj[p0]
         gmsk0 = gmsk[p0]
-        gdir0 = gdir[p0]
         adjdict0 = adjdict[p0]
         @assert length(gmsk0) == length(gadj0)
         @assert length(adjdict0) == length(gadj0)
-        @assert length(gdir0) == length(gadj0)
         for (j0,p1) in enumerate(gadj0)
             @assert adjdict[p1][p0] == j0
             spp1 = spp[p1]
@@ -500,9 +497,50 @@ function check_consistency(graph::Graph)
         @assert rvn ∈ rvs
     end
 
+    for (sav_gconstr,sav_ignored) in solve_stack
+        @assert length(sav_ignored) == np
+        @assert length(sav_gconstr) == np
+        for p0 = 1:np
+            @assert length(sav_gconstr[p0]) == spp[p0]
+        end
+    end
+
     return true
 end
 
+function push_snapshot!(graph::Graph)
+    np = graph.np
+    gconstr = graph.gconstr
+    ignored = graph.ignored
+    solve_stack = graph.solve_stack
+    sav_gconstr = [copy(gc0) for gc0 in gconstr]
+    sav_ignored = copy(ignored)
+    push!(solve_stack, (gconstr, ignored))
+    graph.gconstr = sav_gconstr
+    graph.ignored = sav_ignored
+    return graph
+end
+
+function pop_snapshot!(graph::Graph)
+    np = graph.np
+    solve_stack = graph.solve_stack
+    @assert length(solve_stack) > 0
+    sav_gconstr, sav_ignored = pop!(graph.solve_stack)
+    graph.gconstr = sav_gconstr
+    graph.ignored = sav_ignored
+    return graph
+end
+
+function wipe_snapshots!(graph::Graph)
+    np = graph.np
+    solve_stack = graph.solve_stack
+    if length(solve_stack) > 0
+        graph.gconstr, graph.ignored = first(solve_stack)
+        empty!(solve_stack)
+    end
+    return graph
+end
+
 function init_log!(data::GraphData)
     np = data.np
     pkgs = data.pkgs
@@ -571,6 +609,7 @@ end
 
 function log_event_global!(graph::Graph, msg::String)
     rlog = graph.data.rlog
+    rlog.verbose && info(msg)
     push!(rlog.globals, (nothing, msg))
 end
 
@@ -683,7 +722,7 @@ function log_event_maxsumsolved!(graph::Graph, p0::Int, s0::Int, why::Symbol)
         if s0 == spp[p0] - 1
             msg = "set by the solver to its maximum version: $(pvers[p0][s0])"
         else
-            msg = "set by the solver version: $(pvers[p0][s0]) (version $(pvers[p0][s0+1]) would violate its constraints)"
+            msg = "set by the solver to version: $(pvers[p0][s0]) (version $(pvers[p0][s0+1]) would violate its constraints)"
         end
     end
     entry = rlog.pool[p]
@@ -874,13 +913,14 @@ Propagates current constraints, determining new implicit constraints.
 Throws an error in case impossible requirements are detected, printing
 a log trace.
 """
-function propagate_constraints!(graph::Graph)
+function propagate_constraints!(graph::Graph, sources::Set{Int} = Set{Int}(); log_events::Bool = true)
     np = graph.np
     spp = graph.spp
     gadj = graph.gadj
     gmsk = graph.gmsk
     gconstr = graph.gconstr
     adjdict = graph.adjdict
+    ignored = graph.ignored
     pkgs = graph.data.pkgs
     pvers = graph.data.pvers
     rlog = graph.data.rlog
@@ -888,16 +928,23 @@ function propagate_constraints!(graph::Graph)
 
     id(p0::Int) = pkgID(pkgs[p0], graph)
 
-    log_event_global!(graph, "propagating constraints")
+    log_events && log_event_global!(graph, "propagating constraints")
 
-    # packages which are not allowed to be uninstalled
-    staged = Set{Int}(p0 for p0 = 1:np if !gconstr[p0][end])
+    # unless otherwise specified, start from packages which
+    # are not allowed to be uninstalled
+    staged = isempty(sources) ?
+        Set{Int}(p0 for p0 = 1:np if !gconstr[p0][end]) :
+        sources
 
     while !isempty(staged)
         staged_next = Set{Int}()
         for p0 in staged
             gconstr0 = gconstr[p0]
             for (j1,p1) in enumerate(gadj[p0])
+                # if p1 is ignored, the relation between it and all its neighbors
+                # has already been propagated
+                ignored[p1] && continue
+
                 # we don't propagate to julia (purely to have better error messages)
                 pkgs[p1] == uuid_julia && continue
 
@@ -917,7 +964,7 @@ function propagate_constraints!(graph::Graph)
                 # previous ones, record it and propagate them next
                 if gconstr1 ≠ old_gconstr1
                     push!(staged_next, p1)
-                    log_event_implicit_req!(graph, p1, added_constr1, p0)
+                    log_events && log_event_implicit_req!(graph, p1, added_constr1, p0)
                 end
                 if !any(gconstr1)
                     if exact
@@ -950,7 +997,7 @@ function disable_unreachable!(graph::Graph, sources::Set{Int} = Set{Int}())
 
     log_event_global!(graph, "disabling unreachable nodes")
 
-    # packages which are not allowed to be uninstalled
+    # 2nd argument are packages which are not allowed to be uninstalled
     staged = union(sources, Set{Int}(p0 for p0 = 1:np if !gconstr[p0][end]))
     seen = copy(staged)
 
@@ -979,6 +1026,63 @@ function disable_unreachable!(graph::Graph, sources::Set{Int} = Set{Int}())
     return graph
 end
 
+function deep_clean!(graph::Graph)
+    np = graph.np
+    spp = graph.spp
+
+    log_event_global!(graph, "cleaning graph")
+
+    sumspp = sum(count(graph.gconstr[p0]) for p0 = 1:np)
+
+    while true
+        gconstr_msk = [trues(spp[p0]) for p0 = 1:np]
+
+        str_len = 0
+
+        for p0 = 1:np, v0 in find(graph.gconstr[p0])
+            print("\r" * " "^str_len * "\r")
+            msg = "> $p0 / $np"
+            print(msg)
+            str_len = length(msg)
+            push_snapshot!(graph)
+            fill!(graph.gconstr[p0], false)
+            graph.gconstr[p0][v0] = true
+            try
+                propagate_constraints!(graph, Set{Int}([p0]), log_events = false)
+            catch err
+                err isa PkgError || rethrow(err)
+                gconstr_msk[p0][v0] = false
+            end
+            pop_snapshot!(graph)
+        end
+
+        println()
+
+        affected = Int[]
+        for p0 = 1:np
+            gconstr0 = graph.gconstr[p0]
+            old_gconstr0 = copy(gconstr0)
+            gconstr0 .&= gconstr_msk[p0]
+            if old_gconstr0 ≠ gconstr0
+                push!(affected, p0)
+                #TODO : log event
+            end
+            if !any(gconstr0)
+                # TODO : what should we do here??
+                # throw(PkgError("aaaaaaaaaaaaaahhhhhhhh")) # XXX
+            end
+        end
+        println("> affected = $(length(affected))")
+        isempty(affected) && break
+    end
+
+    sumspp_new = sum(count(graph.gconstr[p0]) for p0 = 1:np)
+
+    log_event_global!(graph, "cleaned graph, stats (total n. of states): before = $(sumspp) after = $(sumspp_new) diff = $(sumspp-sumspp_new)")
+
+    return graph
+end
+
 """
 Reduce the number of versions in the graph by putting all the versions of
 a package that behave identically into equivalence classes, keeping only
@@ -1071,6 +1175,85 @@ function build_eq_classes1!(graph::Graph, p0::Int)
     return
 end
 
+function compute_eq_classes_soft!(graph::Graph; log_events::Bool = true)
+    log_events && log_event_global!(graph, "computing version equivalence classes")
+
+    np = graph.np
+
+    np == 0 && return graph
+
+    ignored = graph.ignored
+    gconstr = graph.gconstr
+    sumspp = sum(count(gconstr[p0]) for p0 = 1:np)
+    for p0 = 1:np
+        ignored[p0] && continue
+        build_eq_classes_soft1!(graph, p0)
+    end
+    sumspp_new = sum(count(gconstr[p0]) for p0 = 1:np)
+
+    log_events && log_event_global!(graph, "computed version equivalence classes, stats (total n. of states): before = $(sumspp) after = $(sumspp_new) diff = $(sumspp_new-sumspp)")
+
+    @assert check_consistency(graph)
+
+    return graph
+end
+
+function build_eq_classes_soft1!(graph::Graph, p0::Int)
+    np = graph.np
+    spp = graph.spp
+    gadj = graph.gadj
+    gmsk = graph.gmsk
+    gconstr = graph.gconstr
+    ignored = graph.ignored
+
+    # concatenate all the constraints; the columns of the
+    # result encode the behavior of each version
+    gadj0 = gadj[p0]
+    gmsk0 = gmsk[p0]
+    gconstr0 = gconstr[p0]
+    eff_spp0 = count(gconstr0)
+    cvecs = BitVector[vcat(BitVector(0), (gmsk0[j1][gconstr[gadj0[j1]],v0] for j1 = 1:length(gadj0) if !ignored[gadj0[j1]])...) for v0 in find(gconstr0)]
+
+    @assert length(cvecs) == eff_spp0
+
+    # find unique behaviors
+    repr_vecs = unique(cvecs)
+
+    # number of equivaent classes
+    neq = length(repr_vecs)
+
+    neq == eff_spp0 && return # nothing to do here
+
+    # group versions into sets that behave identically
+    # each set is represented by its highest-valued member
+    repr_vers = sort!(Int[findlast(equalto(repr_vecs[w0]), cvecs) for w0 = 1:neq])
+    @assert all(repr_vers .> 0)
+    @assert repr_vers[end] == eff_spp0
+
+    # convert the version numbers into the original numbering
+    repr_vers = find(gconstr0)[repr_vers]
+
+    @assert all(gconstr0[repr_vers])
+
+    # disable the other versions by introducing additional constraints
+    fill!(gconstr0, false)
+    gconstr0[repr_vers] = true
+
+    return
+end
+
+function update_ignored!(graph::Graph)
+    np = graph.np
+    gconstr = graph.gconstr
+    ignored = graph.ignored
+
+    for p0 = 1:np
+        ignored[p0] = (count(gconstr[p0]) == 1)
+    end
+
+    return graph
+end
+
 """
 Prune away fixed and unnecessary packages, and the
 disallowed versions for the remaining packages.
@@ -1080,11 +1263,11 @@ function prune_graph!(graph::Graph)
     spp = graph.spp
     gadj = graph.gadj
     gmsk = graph.gmsk
-    gdir = graph.gdir
     gconstr = graph.gconstr
     adjdict = graph.adjdict
     req_inds = graph.req_inds
     fix_inds = graph.fix_inds
+    ignored = graph.ignored
     data = graph.data
     pkgs = data.pkgs
     pdict = data.pdict
@@ -1137,6 +1320,8 @@ function prune_graph!(graph::Graph)
     # Update packages records
     new_pkgs = pkgs[pkg_mask]
     new_pdict = Dict(new_pkgs[new_p0]=>new_p0 for new_p0 = 1:new_np)
+    new_ignored = ignored[pkg_mask]
+    empty!(graph.solve_stack)
 
     # For each package (unless it's going to be pruned) we will remove all
     # versions that aren't allowed (but not the "uninstalled" state)
@@ -1193,16 +1378,6 @@ function prune_graph!(graph::Graph)
         new_adjdict[new_p0][new_p1] = new_j1
     end
 
-    # Recompute gdir on the new adjacency list
-    function compute_gdir(new_p0, new_j0)
-        p0 = old_idx[new_p0]
-        new_p1 = new_gadj[new_p0][new_j0]
-        p1 = old_idx[new_p1]
-        j0 = adjdict[p1][p0]
-        return gdir[p0][j0]
-    end
-    new_gdir = [[compute_gdir(new_p0, new_j0) for new_j0 = 1:length(new_gadj[new_p0])] for new_p0 = 1:new_np]
-
     # Recompute compatibility masks on the new adjacency list, and filtering out some versions
     function compute_gmsk(new_p0, new_j0)
         p0 = old_idx[new_p0]
@@ -1234,13 +1409,14 @@ function prune_graph!(graph::Graph)
     # Replace old structures with new ones
     graph.gadj = new_gadj
     graph.gmsk = new_gmsk
-    graph.gdir = new_gdir
     graph.gconstr = new_gconstr
     graph.adjdict = new_adjdict
     graph.req_inds = new_req_inds
     graph.fix_inds = new_fix_inds
+    graph.ignored = new_ignored
     graph.spp = new_spp
     graph.np = new_np
+    # Note: solve_stack was emptied in-place
 
     @assert check_consistency(graph)
 
@@ -1251,12 +1427,21 @@ end
 Simplifies the graph by propagating constraints, disabling unreachable versions, pruning
 and grouping versions into equivalence classes.
 """
-function simplify_graph!(graph::Graph, sources::Set{Int} = Set{Int}())
+function simplify_graph!(graph::Graph, sources::Set{Int} = Set{Int}(); clean_graph::Bool = false)
     propagate_constraints!(graph)
     disable_unreachable!(graph, sources)
+    clean_graph && deep_clean!(graph)
     prune_graph!(graph)
     compute_eq_classes!(graph)
     return graph
 end
 
+function simplify_graph_soft!(graph::Graph, sources::Set{Int} = Set{Int}(); log_events = true)
+    propagate_constraints!(graph, sources, log_events = log_events)
+    update_ignored!(graph)
+    compute_eq_classes_soft!(graph, log_events = log_events)
+    update_ignored!(graph)
+    return graph
+end
+
 end # module
diff --git a/src/Resolve.jl b/src/Resolve.jl
index fe489588d24e2..300414ee41aaf 100644
--- a/src/Resolve.jl
+++ b/src/Resolve.jl
@@ -15,46 +15,33 @@ export resolve, sanity_check
 
 "Resolve package dependencies."
 function resolve(graph::Graph)
-    id(p) = pkgID(p, graph)
-
     # attempt trivial solution first
-    ok, sol = greedysolver(graph)
+    greedy_ok, sol = greedysolver(graph)
 
-    ok && @goto solved
+    greedy_ok && @goto solved
 
     log_event_global!(graph, "greedy solver failed")
 
     # trivial solution failed, use maxsum solver
-    msgs = Messages(graph)
+    maxsum_ok, sol, staged = maxsum(graph)
 
-    try
-        sol = maxsum(graph, msgs)
-        @goto check
-    catch err
-        isa(err, UnsatError) || rethrow(err)
-        apply_maxsum_trace!(graph, err.trace)
-    end
+    maxsum_ok && @goto solved
 
     log_event_global!(graph, "maxsum solver failed")
 
-    check_constraints(graph) # will throw if it fails
-    simplify_graph!(graph)   # will throw if it fails
-    # NOTE: here it seems like there could be an infinite recursion loop.
-    #       However, if maxsum fails with an empty trace (which could lead to
-    #       the recursion) then the two above checks should be able to
-    #       detect an error. Nevertheless, it's probably better to put some
-    #       kind of failsafe here.
-    return resolve(graph)
+    # the problem is unsat, force-trigger a failure
+    # in order to produce a log - this will contain
+    # information about the best that the solver could
+    # achieve
+    trigger_failure!(graph, sol, staged)
 
-    @label check
+    @label solved
 
     # verify solution (debug code) and enforce its optimality
     @assert verify_solution(sol, graph)
-    enforce_optimality!(sol, graph)
-
-    @label solved
+    greedy_ok || enforce_optimality!(sol, graph)
 
-    log_event_global!(graph, "the solver found a feasible configuration")
+    log_event_global!(graph, "the solver found $(greedy_ok ? "an optimal" : "a feasible") configuration")
 
     # return the solution as a Dict mapping UUID => VersionNumber
     return compute_output_dict(sol, graph)
@@ -109,65 +96,63 @@ function sanity_check(graph::Graph, sources::Set{UUID} = Set{UUID}(); verbose =
 
     last_str_len = 0
 
-    i = 1
-    for (p,vn) in vers
+    for (i,(p,vn)) in enumerate(vers)
         if verbose
             frac_compl = i / nv
-            print("\r", " "^last_str_len)
-            progr_msg = @sprintf("\r%.3i/%.3i (%i%%) — problematic so far: %i", i, nv, round(Int, 100 * frac_compl), length(problematic))
+            print("\r", " "^last_str_len, "\r")
+            progr_msg = @sprintf("%.3i/%.3i (%i%%) — problematic so far: %i", i, nv, round(Int, 100 * frac_compl), length(problematic))
             print(progr_msg)
             last_str_len = length(progr_msg)
         end
 
         length(gadj[pdict[p]]) == 0 && break
-        checked[i] && (i += 1; continue)
+        checked[i] && continue
 
-        req = Requires(p => vn)
-        sub_graph = copy(graph)
-        add_reqs!(sub_graph, req)
+        push_snapshot!(graph)
 
+        # enforce package version
+        # TODO: use add_reqs! instead...
+        p0 = graph.data.pdict[p]
+        v0 = graph.data.vdict[p0][vn]
+        fill!(graph.gconstr[p0], false)
+        graph.gconstr[p0][v0] = true
+        push!(graph.req_inds, p0)
+
+        ok = false
         try
-            simplify_graph!(sub_graph)
+            simplify_graph_soft!(graph, Set{Int}([p0]), log_events = false)
         catch err
             isa(err, PkgError) || rethrow(err)
-            ## info("ERROR MESSAGE:\n" * err.msg)
-            for vneq in eq_classes[p][vn]
-                push!(problematic, (id(p), vneq))
-            end
-            i += 1
-            continue
+            @goto done
         end
 
-        ok, sol = greedysolver(sub_graph)
-
-        ok && @goto solved
+        ok, sol = greedysolver(graph)
+        ok && @goto done
+        ok, sol = maxsum(graph)
 
-        msgs = Messages(sub_graph)
+        @label done
 
-        try
-            sol = maxsum(sub_graph, msgs)
-            @assert verify_solution(sol, sub_graph)
-        catch err
-            isa(err, UnsatError) || rethrow(err)
+        if !ok
             for vneq in eq_classes[p][vn]
                 push!(problematic, (id(p), vneq))
             end
-            i += 1
-            continue
-        end
-
-        @label solved
-
-        sol_dict = compute_output_dict(sol, sub_graph)
-        for (sp, svn) in sol_dict
-            j = svdict[sp,svn]
-            checked[j] = true
+        else
+            @assert verify_solution(sol, graph)
+            sol_dict = compute_output_dict(sol, graph)
+            for (sp,svn) in sol_dict
+                j = svdict[sp,svn]
+                checked[j] = true
+            end
         end
 
-        i += 1
+        # state reset
+        empty!(graph.req_inds)
+        pop_snapshot!(graph)
+    end
+    if verbose
+        print("\r", " "^last_str_len, "\r")
+        println("found $(length(problematic)) problematic versions")
     end
-    verbose && println()
-
     return sort!(problematic)
 end
 
@@ -208,9 +193,11 @@ function greedysolver(graph::Graph)
     spp = graph.spp
     gadj = graph.gadj
     gmsk = graph.gmsk
-    gconstr = graph.gconstr
     np = graph.np
 
+    push_snapshot!(graph)
+    gconstr = graph.gconstr
+
     # initialize solution: all uninstalled
     sol = [spp[p0] for p0 = 1:np]
 
@@ -225,6 +212,17 @@ function greedysolver(graph::Graph)
         rv0 = findlast(gconstr[rp0])
         @assert rv0 ≠ 0 && rv0 ≠ spp[rp0]
         sol[rp0] = rv0
+        fill!(gconstr[rp0], false)
+        gconstr[rp0][rv0] = true
+    end
+
+    # propagate the requirements
+    try
+        simplify_graph_soft!(graph, req_inds, log_events = false)
+    catch err
+        err isa PkgError || rethrow(err)
+        pop_snapshot!(graph)
+        return (false, Int[])
     end
 
     # we start from required packages and explore the graph
@@ -251,6 +249,7 @@ function greedysolver(graph::Graph)
                 if v1 > 0 && (sol[p1] == spp[p1] || sol[p1] == v1)
                     sol[p1] = v1
                 else
+                    pop_snapshot!(graph)
                     return (false, Int[])
                 end
 
@@ -261,7 +260,7 @@ function greedysolver(graph::Graph)
         staged = staged_next
     end
 
-    @assert verify_solution(sol, graph)
+    pop_snapshot!(graph)
 
     for p0 = 1:np
         log_event_greedysolved!(graph, p0, sol[p0])
@@ -281,14 +280,17 @@ function verify_solution(sol::Vector{Int}, graph::Graph)
     gmsk = graph.gmsk
     gconstr = graph.gconstr
 
+    @assert length(sol) == np
+    @assert all(sol .> 0)
+
     # verify constraints and dependencies
     for p0 = 1:np
         s0 = sol[p0]
-        gconstr[p0][s0] || return false
+        gconstr[p0][s0] || (warn("gconstr[$p0][$s0] fail"); return false)
         for (j1,p1) in enumerate(gadj[p0])
             msk = gmsk[p0][j1]
             s1 = sol[p1]
-            msk[s1,s0] || return false # TODO: print debug info
+            msk[s1,s0] || (warn("gmsk[$p0][$p1][$s1,$s0] fail"); return false)
         end
     end
     return true
@@ -305,7 +307,6 @@ function enforce_optimality!(sol::Vector{Int}, graph::Graph)
     spp = graph.spp
     gadj = graph.gadj
     gmsk = graph.gmsk
-    gdir = graph.gdir
     gconstr = graph.gconstr
     pkgs = graph.data.pkgs
 
@@ -377,18 +378,36 @@ function enforce_optimality!(sol::Vector{Int}, graph::Graph)
     end
 end
 
-function apply_maxsum_trace!(graph::Graph, trace::Vector{Any})
-    np = graph.np
-    spp = graph.spp
+function apply_maxsum_trace!(graph::Graph, sol::Vector{Int})
     gconstr = graph.gconstr
 
-    for (p0,s0) in trace
-        new_constr = falses(spp[p0])
-        new_constr[s0] = true
-        old_constr = copy(gconstr[p0])
-        gconstr[p0] .&= new_constr
-        gconstr[p0] ≠ old_constr && log_event_maxsumtrace!(graph, p0, s0)
+    for (p0,s0) in enumerate(sol)
+        s0 == 0 && continue
+        gconstr0 = gconstr[p0]
+        old_constr = copy(gconstr0)
+        @assert old_constr[s0]
+        fill!(gconstr0, false)
+        gconstr0[s0] = true
+        gconstr0 ≠ old_constr && log_event_maxsumtrace!(graph, p0, s0)
     end
 end
 
+function trigger_failure!(graph::Graph, sol::Vector{Int}, staged::Tuple{Int,Int})
+    apply_maxsum_trace!(graph, sol)
+    simplify_graph_soft!(graph, Set(find(sol .> 0)), log_events = true) # this may throw an error...
+
+    np = graph.np
+    gconstr = graph.gconstr
+    p0, v0 = staged
+
+    @assert gconstr[p0][v0]
+    fill!(gconstr[p0], false)
+    gconstr[p0][v0] = true
+    log_event_maxsumtrace!(graph, p0, v0)
+    simplify_graph!(graph) # this may throw an error...
+    outdict = resolve(graph) # ...otherwise, this MUST throw an error
+    open(io->showlog(io, graph, view=:chronological), "logchrono.errresolve.txt", "w")
+    error("this is not supposed to happen... $(Dict(pkgID(p, graph) => vn for (p,vn) in outdict))")
+end
+
 end # module
diff --git a/src/resolve/FieldValues.jl b/src/resolve/FieldValues.jl
index 4cef1b00e4554..abf3e2abd39e5 100644
--- a/src/resolve/FieldValues.jl
+++ b/src/resolve/FieldValues.jl
@@ -15,19 +15,16 @@ export FieldValue, Field, validmax, secondmax
 #       packages
 #  l2 : for favoring higher versions of all other packages
 #  l3 : for favoring uninstallation of non-needed packages
-#  l4 : for favoring dependants over dependencies
 #
 struct FieldValue
     l0::Int64
     l1::VersionWeight
     l2::VersionWeight
     l3::Int64
-    l4::Int64
     FieldValue(l0::Integer = 0,
                l1::VersionWeight = zero(VersionWeight),
                l2::VersionWeight = zero(VersionWeight),
-               l3::Integer = 0,
-               l4::Integer = 0) = new(l0, l1, l2, l3, l4)
+               l3::Integer = 0) = new(l0, l1, l2, l3)
 end
 
 # This isn't nice, but it's for debugging only anyway
@@ -39,8 +36,6 @@ function Base.show(io::IO, a::FieldValue)
     print(io, ".", a.l2)
     a == FieldValue(a.l0, a.l1, a.l2) && return
     print(io, ".", a.l3)
-    a == FieldValue(a.l0, a.l1, a.l2, a.l3) && return
-    print(io, ".", a.l4)
     return
 end
 
@@ -48,10 +43,10 @@ const Field = Vector{FieldValue}
 
 Base.zero(::Type{FieldValue}) = FieldValue()
 
-Base.typemin(::Type{FieldValue}) = (x=typemin(Int64); y=typemin(VersionWeight); FieldValue(x, y, y, x, x))
+Base.typemin(::Type{FieldValue}) = (x=typemin(Int64); y=typemin(VersionWeight); FieldValue(x, y, y, x))
 
-Base.:-(a::FieldValue, b::FieldValue) = FieldValue(a.l0-b.l0, a.l1-b.l1, a.l2-b.l2, a.l3-b.l3, a.l4-b.l4)
-Base.:+(a::FieldValue, b::FieldValue) = FieldValue(a.l0+b.l0, a.l1+b.l1, a.l2+b.l2, a.l3+b.l3, a.l4+b.l4)
+Base.:-(a::FieldValue, b::FieldValue) = FieldValue(a.l0-b.l0, a.l1-b.l1, a.l2-b.l2, a.l3-b.l3)
+Base.:+(a::FieldValue, b::FieldValue) = FieldValue(a.l0+b.l0, a.l1+b.l1, a.l2+b.l2, a.l3+b.l3)
 
 function Base.isless(a::FieldValue, b::FieldValue)
     a.l0 < b.l0 && return true
@@ -63,17 +58,15 @@ function Base.isless(a::FieldValue, b::FieldValue)
     c < 0 && return true
     c > 0 && return false
     a.l3 < b.l3 && return true
-    a.l3 > b.l3 && return false
-    a.l4 < b.l4 && return true
     return false
 end
 
 Base.:(==)(a::FieldValue, b::FieldValue) =
-    a.l0 == b.l0 && a.l1 == b.l1 && a.l2 == b.l2 && a.l3 == b.l3 && a.l4 == b.l4
+    a.l0 == b.l0 && a.l1 == b.l1 && a.l2 == b.l2 && a.l3 == b.l3
 
-Base.abs(a::FieldValue) = FieldValue(abs(a.l0), abs(a.l1), abs(a.l2), abs(a.l3), abs(a.l4))
+Base.abs(a::FieldValue) = FieldValue(abs(a.l0), abs(a.l1), abs(a.l2), abs(a.l3))
 
-Base.copy(a::FieldValue) = FieldValue(a.l0, copy(a.l1), copy(a.l2), a.l3, a.l4)
+Base.copy(a::FieldValue) = FieldValue(a.l0, copy(a.l1), copy(a.l2), a.l3)
 
 # if the maximum field has l0 < 0, it means that
 # some hard constraint is being violated
@@ -96,10 +89,11 @@ end
 
 # secondmax returns the (normalized) value of the second maximum in a
 # field. It's used to determine the most polarized field.
-function secondmax(f::Field)
+function secondmax(f::Field, msk::BitVector = trues(length(f)))
     m = typemin(FieldValue)
     m2 = typemin(FieldValue)
     for i = 1:length(f)
+        msk[i] || continue
         a = f[i]
         if a > m
             m2 = m
diff --git a/src/resolve/MaxSum.jl b/src/resolve/MaxSum.jl
index 3dcbd6229c31d..a0c62a1f07183 100644
--- a/src/resolve/MaxSum.jl
+++ b/src/resolve/MaxSum.jl
@@ -11,26 +11,21 @@ export UnsatError, Messages, maxsum
 # An exception type used internally to signal that an unsatisfiable
 # constraint was detected
 struct UnsatError <: Exception
-    trace
+    p0::Int
 end
 
 # Some parameters to drive the decimation process
 mutable struct MaxSumParams
-    nondec_iterations # number of initial iterations before starting
-                      # decimation
     dec_interval # number of iterations between decimations
     dec_fraction # fraction of nodes to decimate at every decimation
                  # step
 
     function MaxSumParams()
         accuracy = parse(Int, get(ENV, "JULIA_PKGRESOLVE_ACCURACY", "1"))
-        if accuracy <= 0
-            error("JULIA_PKGRESOLVE_ACCURACY must be > 0")
-        end
-        nondec_iterations = accuracy * 20
-        dec_interval = accuracy * 10
+        accuracy > 0 || error("JULIA_PKGRESOLVE_ACCURACY must be > 0")
+        dec_interval = accuracy * 5
         dec_fraction = 0.05 / accuracy
-        return new(nondec_iterations, dec_interval, dec_fraction)
+        return new(dec_interval, dec_fraction)
     end
 end
 
@@ -52,82 +47,117 @@ mutable struct Messages
     # backup of the initial value of fld, to be used when resetting
     initial_fld::Vector{Field}
 
-    # the solution is built progressively by a decimation process
-    solution::Vector{Int}
-    num_nondecimated::Int
-
-    # try to build a trace
-    trace::Vector{Any}
-
     function Messages(graph::Graph)
         np = graph.np
         spp = graph.spp
+        gadj = graph.gadj
         gconstr = graph.gconstr
         req_inds = graph.req_inds
+        ignored = graph.ignored
         pvers = graph.data.pvers
         pdict = graph.data.pdict
 
         ## generate wveights (v0 == spp[p0] is the "uninstalled" state)
         vweight = [[VersionWeight(v0 < spp[p0] ? pvers[p0][v0] : v"0") for v0 = 1:spp[p0]] for p0 = 1:np]
 
-        # external fields: favor newest versions over older, and no-version over all
-        fld = [[FieldValue(0, zero(VersionWeight), vweight[p0][v0], (v0==spp[p0]), 0) for v0 = 1:spp[p0]] for p0 = 1:np]
+        # external fields: favor newest versions over older, and no-version over all;
+        #                  explicit requirements use level l1 instead of l2
+        fv(p0, v0) = p0 ∈ req_inds ?
+            FieldValue(0, vweight[p0][v0],     zero(VersionWeight), (v0==spp[p0])) :
+            FieldValue(0, zero(VersionWeight), vweight[p0][v0],     (v0==spp[p0]))
+        fld = [[fv(p0, v0) for v0 = 1:spp[p0]] for p0 = 1:np]
 
-        # enforce constraints
-        for p0 = 1:np
-            fld0 = fld[p0]
-            gconstr0 = gconstr[p0]
-            for v0 = 1:spp[p0]
-                gconstr0[v0] || (fld0[v0] = FieldValue(-1))
-            end
-        end
+        initial_fld = [copy(f0) for f0 in fld]
 
-        # favor explicit requirements
-        for rp0 in req_inds
-            fld0 = fld[rp0]
-            gconstr0 = gconstr[rp0]
-            for v0 = 1:spp[rp0]-1
-                gconstr0[v0] || continue
-                # the state is one of those explicitly requested:
-                # favor it at a higer level than normal (upgrade
-                # FieldValue from l2 to l1)
-                fld0[v0] += FieldValue(0, vweight[rp0][v0], -vweight[rp0][v0])
-            end
-        end
+        # allocate cavity messages
+        msg = [[Field(spp[p0]) for j1 = 1:length(gadj[p0])] for p0 = 1:np]
+
+        msgs = new(msg, fld, initial_fld)
+
+        reset_messages!(msgs, graph)
 
-        # normalize fields
-        for p0 = 1:np
-            fld[p0] .-= maximum(fld[p0])
+        return msgs
+    end
+end
+
+# enforce constraints and normalize fields;
+# zero out all cavity messages
+function reset_messages!(msgs::Messages, graph::Graph)
+    msg = msgs.msg
+    fld = msgs.fld
+    initial_fld = msgs.initial_fld
+    np = graph.np
+    spp = graph.spp
+    gconstr = graph.gconstr
+    ignored = graph.ignored
+    for p0 = 1:np
+        ignored[p0] && continue
+        map(m->fill!(m, zero(FieldValue)), msg[p0])
+        copy!(fld[p0], initial_fld[p0])
+        gconstr0 = gconstr[p0]
+        for v0 = 1:spp[p0]
+            gconstr0[v0] || (fld[p0][v0] = FieldValue(-1))
         end
+        fld[p0] .-= maximum(fld[p0])
+    end
+    return msgs
+end
 
-        initial_fld = [copy(f0) for f0 in fld]
+mutable struct SolutionTrace
+    # the solution is built progressively by a decimation process
+    solution::Vector{Int}
+    num_nondecimated::Int
 
-        # initialize cavity messages to 0
-        gadj = graph.gadj
-        msg = [[zeros(FieldValue, spp[p0]) for j1 = 1:length(gadj[p0])] for p0 = 1:np]
+    best::Vector{Int}
+    staged::Union{Tuple{Int,Int},Void}
 
+    function SolutionTrace(graph::Graph)
+        np = graph.np
         solution = zeros(Int, np)
         num_nondecimated = np
 
-        trace = []
+        best = zeros(Int, np)
+        staged = nothing
 
-        return new(msg, fld, initial_fld, solution, num_nondecimated, trace)
+        return new(solution, num_nondecimated, best, staged)
+    end
+end
+
+function update_solution!(strace::SolutionTrace, graph::Graph)
+    np = graph.np
+    ignored = graph.ignored
+    gconstr = graph.gconstr
+    solution = strace.solution
+    best = strace.best
+    nnd = np
+    fill!(solution, 0)
+    for p0 in find(ignored)
+        s0 = findfirst(gconstr[p0])
+        solution[p0] = s0
+        nnd -= 1
+    end
+    strace.num_nondecimated = nnd
+    if nnd ≤ sum(best .== 0)
+        copy!(best, solution)
+        strace.staged = nothing
+        return true
+    else
+        return false
     end
 end
 
 # This is the core of the max-sum solver:
 # for a given node p0 (i.e. a package) updates all
 # input cavity messages and fields of its neighbors
-function update(p0::Int, graph::Graph, msgs::Messages)
+function update!(p0::Int, graph::Graph, msgs::Messages)
     gadj = graph.gadj
     gmsk = graph.gmsk
-    gdir = graph.gdir
     adjdict = graph.adjdict
+    ignored = graph.ignored
     spp = graph.spp
     np = graph.np
     msg = msgs.msg
     fld = msgs.fld
-    solution = msgs.solution
 
     maxdiff = zero(FieldValue)
 
@@ -141,23 +171,15 @@ function update(p0::Int, graph::Graph, msgs::Messages)
     for j0 in 1:length(gadj0)
 
         p1 = gadj0[j0]
-        solution[p1] > 0 && continue # already decimated
+        ignored[p1] && continue
         j1 = adjdict0[p1]
         #@assert j0 == adjdict[p1][p0]
         bm1 = gmsk[p1][j1]
-        dir1 = gdir[p1][j1]
         spp1 = spp[p1]
         msg1 = msg[p1]
 
-        # compute the output cavity message p0->p1
-        cavmsg = fld0 - msg0[j0]
-
-        if dir1 == GraphType.BACKWARDS
-            # p0 depends on p1
-            for v0 = 1:spp0-1
-                cavmsg[v0] += FieldValue(0, VersionWeight(0), VersionWeight(0), 0, v0)
-            end
-        end
+        # compute the output cavity field p0->p1
+        cavfld = fld0 - msg0[j0]
 
         # keep the old input cavity message p0->p1
         oldmsg = msg1[j1]
@@ -165,43 +187,27 @@ function update(p0::Int, graph::Graph, msgs::Messages)
         # init the new message to minus infinity
         newmsg = [FieldValue(-1) for v1 = 1:spp1]
 
-        # compute the new message by passing cavmsg
+        # compute the new message by passing cavfld
         # through the constraint encoded in the bitmask
-        # (nearly equivalent to:
-        #    newmsg = [maximum(cavmsg[bm1[:,v1]]) for v1 = 1:spp1]
-        #  except for the directional term)
-        m = FieldValue(-1)
-        for v1 = 1:spp1
-            for v0 = 1:spp0
-                if bm1[v0, v1]
-                    newmsg[v1] = max(newmsg[v1], cavmsg[v0])
-                end
-            end
-            if dir1 == GraphType.FORWARD && v1 != spp1
-                # p1 depends on p0
-                newmsg[v1] += FieldValue(0, VersionWeight(0), VersionWeight(0), 0, v1)
-            end
-            m = max(m, newmsg[v1])
-        end
-        if !validmax(m)
-            # No state available without violating some
-            # hard constraint
-            throw(UnsatError(msgs.trace))
+        # (equivalent to:
+        #    newmsg = [maximum(cavfld[bm1[:,v1]]) for v1 = 1:spp1]
+        # )
+        for v1 = 1:spp1, v0 = 1:spp0
+            bm1[v0, v1] || continue
+            newmsg[v1] = max(newmsg[v1], cavfld[v0])
         end
+        m = maximum(newmsg)
+        validmax(m) || throw(UnsatError(p0)) # No state available without violating some
+                                             # hard constraint
 
         # normalize the new message
-        for v1 = 1:spp1
-            newmsg[v1] -= m
-        end
+        newmsg .-= m
 
         diff = newmsg - oldmsg
         maxdiff = max(maxdiff, maximum(abs.(diff)))
 
         # update the field of p1
-        fld1 = fld[p1]
-        for v1 = 1:spp1
-            fld1[v1] += diff[v1]
-        end
+        fld[p1] .+= diff
 
         # put the newly computed message in place
         msg1[j1] = newmsg
@@ -209,7 +215,7 @@ function update(p0::Int, graph::Graph, msgs::Messages)
     return maxdiff
 end
 
-# A simple shuffling machinery for the update order in iterate()
+# A simple shuffling machinery for the update order in iterate!()
 # (wouldn't pass any random quality test but it's arguably enough)
 mutable struct NodePerm
     p::Vector{Int}
@@ -233,161 +239,242 @@ Base.done(perm::NodePerm, x) = done(perm.p, x)
 
 # Call update for all nodes (i.e. packages) in
 # random order
-function iterate(graph::Graph, msgs::Messages, perm::NodePerm)
+function iterate!(graph::Graph, msgs::Messages, perm::NodePerm)
     maxdiff = zero(FieldValue)
     shuffle!(perm)
     for p0 in perm
-        maxdiff0 = update(p0, graph, msgs)
+        graph.ignored[p0] && continue
+        maxdiff0 = update!(p0, graph, msgs)
         maxdiff = max(maxdiff, maxdiff0)
     end
     return maxdiff
 end
 
-function decimate1(p0::Int, graph::Graph, msgs::Messages)
-    solution = msgs.solution
+function decimate1!(p0::Int, graph::Graph, strace::SolutionTrace, msgs::Messages)
+    solution = strace.solution
     fld = msgs.fld
     adjdict = graph.adjdict
     gmsk = graph.gmsk
     gconstr = graph.gconstr
 
     @assert solution[p0] == 0
+    @assert !graph.ignored[p0]
     fld0 = fld[p0]
     s0 = indmax(fld0)
     # only do the decimation if it is consistent with
     # the constraints...
-    gconstr[p0][s0] || return false
+    gconstr[p0][s0] || return 0
     # ...and with the previously decimated nodes
     for p1 in find(solution .> 0)
         haskey(adjdict[p0], p1) || continue
-        s1 = indmax(fld[p1])
+        s1 = solution[p1]
         j1 = adjdict[p0][p1]
-        gmsk[p1][j1][s0,s1] || return false
-    end
-    #println("DECIMATING $p0 (s0=$s0 fld=$fld0)")
-    for v0 = 1:length(fld0)
-        v0 == s0 && continue
-        fld0[v0] = FieldValue(-1)
-    end
-    msgs.solution[p0] = s0
-    msgs.num_nondecimated -= 1
-    push!(msgs.trace, (p0,s0))
-    return true
-end
-
-function reset_messages!(msgs::Messages)
-    msg = msgs.msg
-    fld = msgs.fld
-    initial_fld = msgs.initial_fld
-    solution = msgs.solution
-    np = length(fld)
-    for p0 = 1:np
-        map(m->fill!(m, zero(FieldValue)), msg[p0])
-        solution[p0] > 0 && continue
-        fld[p0] = copy(initial_fld[p0])
+        gmsk[p1][j1][s0,s1] || return 0
     end
-    return msgs
+    solution[p0] = s0
+    strace.num_nondecimated -= 1
+    return s0
 end
 
-# If normal convergence fails (or is too slow) fix the most
-# polarized packages by adding extra infinite fields on every state
-# but the maximum
-function decimate(n::Int, graph::Graph, msgs::Messages)
-    #println("DECIMATING $n NODES")
-    adjdict = graph.adjdict
+function decimate!(graph::Graph, strace::SolutionTrace, msgs::Messages, n::Integer)
+    np = graph.np
+    gconstr = graph.gconstr
+    ignored = graph.ignored
     fld = msgs.fld
-    solution = msgs.solution
-    fldorder = sortperm(fld, by=secondmax)
-    did_dec = false
-    for p0 in fldorder
-        solution[p0] > 0 && continue
-        did_dec |= decimate1(p0, graph, msgs)
-        n -= 1
-        n == 0 && break
-    end
-    @assert n == 0
 
-    did_dec && @goto ok
+    @assert n ≥ 1
+    dtrace = Tuple{Int,Int}[]
+    dec = 0
 
-    # did not succeed in decimating anything;
-    # try to decimate at least one node
+    fldorder = sort(find(.!(ignored)), by=p0->secondmax(fld[p0], gconstr[p0]))
     for p0 in fldorder
-        solution[p0] > 0 && continue
-        decimate1(p0, graph, msgs) && @goto ok
+        s0 = decimate1!(p0, graph, strace, msgs)
+        s0 == 0 && continue
+        push!(dtrace, (p0,s0))
+        dec += 1
+        dec == n && break
     end
 
-    # still didn't succeed, give up
-    p0 = findfirst(solution .== 0)
-    throw(UnsatError(msgs.trace))
-
-    @label ok
-
-    reset_messages!(msgs)
-    return
+    return dtrace
 end
 
-# In case ties still exist at convergence, break them and
-# keep converging
-function break_ties(msgs::Messages)
+function clean_forbidden!(graph::Graph, msgs::Messages)
+    np = graph.np
+    gconstr = graph.gconstr
+    ignored = graph.ignored
     fld = msgs.fld
-    unbroken_ties = Int[]
-    for p0 = 1:length(fld)
+    affected = Tuple{Int,Int}[]
+    removed = 0
+
+    for p0 = 1:np
+        ignored[p0] && continue
         fld0 = fld[p0]
-        z = 0
-        m = typemin(FieldValue)
-        for v0 = 1:length(fld0)
-            if fld0[v0] > m
-                m = fld0[v0]
-                z = 1
-            elseif fld0[v0] == m
-                z += 1
-            end
-        end
-        if z > 1
-            #println("TIE! p0=$p0")
-            decimate1(p0, msgs) && return false
-            push!(unbroken_ties, p0)
+        gconstr0 = gconstr[p0]
+        for v0 in find(gconstr0)
+            validmax(fld0[v0]) && continue
+            push!(affected, (p0,v0))
+            removed += 1
         end
     end
-    # If there were ties, but none were broken, bail out
-    isempty(unbroken_ties) || throw(PkgError(first(unbroken_ties)))
-    return true
+    return affected
 end
 
-# Iterative solver: run iterate() until convergence
+# Iterative solver: run iterate!() until convergence
 # (occasionally calling decimate())
-function maxsum(graph::Graph, msgs::Messages)
+function maxsum(graph::Graph)
     params = MaxSumParams()
 
-    it = 0
     perm = NodePerm(graph.np)
-    while true
-        it += 1
-        maxdiff = iterate(graph, msgs, perm)
-        #println("it = $it maxdiff = $maxdiff")
+    strace = SolutionTrace(graph)
+    msgs = Messages(graph)
+
+    push_snapshot!(graph)
+    # gconstr_sav = graph.gconstr
+    # ignored_sav = graph.ignored
+    ok = converge!(graph, msgs, strace, perm, params)
+    # @assert graph.gconstr ≡ gconstr_sav
+    # @assert graph.ignored ≡ ignored_sav
+    pop_snapshot!(graph)
+    if ok
+        @assert strace.best == strace.solution
+        @assert strace.num_nondecimated == 0
+        @assert all(strace.solution .> 0)
+        @assert strace.staged ≡ nothing
+    else
+        @assert strace.staged ≢ nothing
+    end
+    return ok, strace.best, strace.staged
+end
+
+function try_simplify_graph_soft!(graph, sources)
+    try
+        simplify_graph_soft!(graph, sources, log_events = false)
+    catch err
+        err isa PkgError || rethrow(err)
+        return false
+    end
+    return true
+end
 
-        if maxdiff == zero(FieldValue)
-            break_ties(msgs) && break
-            continue
+function converge!(graph::Graph, msgs::Messages, strace::SolutionTrace, perm::NodePerm, params::MaxSumParams)
+    is_best_sofar = update_solution!(strace, graph)
+
+    # this is the base of the recursion: the case when
+    # the solver has succeeded in decimating everything
+    strace.num_nondecimated == 0 && return true
+
+    reset_messages!(msgs, graph)
+
+    # perform some maxsum iterations, then decimate one node.
+    # If failure happens during this process, we bail (return false)
+    it = 0
+    for it = 1:params.dec_interval
+        local maxdiff::FieldValue
+        try
+            maxdiff = iterate!(graph, msgs, perm)
+        catch err
+            err isa UnsatError || rethrow(err)
+            if is_best_sofar
+                p0 = err.p0
+                s0 = findlast(graph.gconstr[p0])
+                strace.staged = (p0, s0)
+            end
+            return false
         end
-        if it >= params.nondec_iterations &&
-           (it - params.nondec_iterations) % params.dec_interval == 0
-            numdec = clamp(floor(Int, params.dec_fraction * graph.np), 1, msgs.num_nondecimated)
-            decimate(numdec, graph, msgs)
-            msgs.num_nondecimated == 0 && break
+        maxdiff == zero(FieldValue) && break
+    end
+
+    # if maxsum has found some forbidden states, remove
+    # them and propagate the effect
+    affected = clean_forbidden!(graph, msgs)
+
+    isempty(affected) && @goto decimate
+
+    sources = Set{Int}()
+    for (p0,v0) in affected
+        graph.gconstr[p0][v0] = false
+        push!(sources, p0)
+    end
+
+    if !try_simplify_graph_soft!(graph, sources)
+        # found an implicit contradiction
+        is_best_sofar && (strace.staged = first(affected))
+        return false
+    end
+    return converge!(graph, msgs, strace, perm, params)
+
+    @label decimate
+
+    ndec = max(1, round(Int, params.dec_fraction * strace.num_nondecimated))
+    dtrace = decimate!(graph, strace, msgs, ndec)
+    if isempty(dtrace)
+        # decimation has failed, all candidate states are forbidden
+        # (which shouldn't really happen, this is a failsafe)
+        if is_best_sofar
+            # pick the first decimation candidate
+            smx(p1) = secondmax(msgs.fld[p1], graph.gconstr[p1])
+            p0 = reduce((p1,p2)->(smx(p1)≤smx(p2) ? p1 : p2), find(.!(graph.ignored)))
+            s0 = indmax(fld[p0])
+            strace.staged = dec_firstcandidate(graph, msgs)
         end
+        return false
     end
 
-    # Finally, decimate everything just to
-    # check against inconsistencies
-    # (old_numnondec is saved just to prevent
-    # wrong messages about accuracy)
-    old_numnondec = msgs.num_nondecimated
-    while msgs.num_nondecimated > 0
-        decimate(msgs.num_nondecimated, graph, msgs)
+    while true
+        # decimation has succeeded, at least nominally.
+        # We need to propagate its effects and check for contradictions
+
+        lentr = length(dtrace)
+        if lentr == 1 && is_best_sofar
+            strace.staged = dtrace[1]
+        end
+
+        push_snapshot!(graph)
+        # info("setting dtrace=$dtrace")
+        for (p0,s0) in dtrace
+            @assert !graph.ignored[p0]
+            @assert graph.gconstr[p0][s0]
+            fill!(graph.gconstr[p0], false)
+            graph.gconstr[p0][s0] = true
+            graph.ignored[p0] = true
+        end
+
+        # if decimation has produced an implicit contradiction, backtrack
+        try_simplify_graph_soft!(graph, Set{Int}(first.(dtrace))) || @goto backtrack
+
+        # otherwise, keep going...
+        converge!(graph, msgs, strace, perm, params) && (pop_snapshot!(graph); return true)
+
+        @label backtrack
+
+        # warn("reverting dtrace=$dtrace")
+
+        # if we're here, the last decimation step has been proven to lead
+        # to an unsat situation at some point, we need to roll it back
+
+        # revert the state of the constraints
+        pop_snapshot!(graph)
+
+        lentr == 1 && break
+        # halve the dtrace
+        deleteat!(dtrace, ((lentr÷2)+1):lentr)
     end
-    msgs.num_nondecimated = old_numnondec
 
-    return copy(msgs.solution)
+    @assert length(dtrace) == 1
+    p0, s0 = dtrace[1]
+
+    is_best_sofar && @assert strace.staged ≢ nothing
+
+    # forbid the state used in the last attempt
+    # (note that we're working on the "entry" snapshot here!)
+    graph.gconstr[p0][s0] = false
+    # check if we have finished all available possibilities
+    any(graph.gconstr[p0]) || return false
+    # if neither the s0 state nor its negation are valid, give up
+    try_simplify_graph_soft!(graph, Set{Int}([p0])) || return false
+
+    # keep going, with one possible state less...
+    return converge!(graph, msgs, strace, perm, params)
 end
 
 end
diff --git a/test/NastyGenerator.jl b/test/NastyGenerator.jl
new file mode 100644
index 0000000000000..4f566fb3ace7c
--- /dev/null
+++ b/test/NastyGenerator.jl
@@ -0,0 +1,96 @@
+module NastyGenerator
+
+pn(i) = "P$i"
+randvers(k::Int) = VersionNumber(rand(0:k), rand(0:k), rand(0:k))
+
+function randvspec(k::Int)
+    lb, ub = randvers(k), randvers(k)
+    if lb > ub
+        lb, ub = ub, lb
+    end
+
+    slb = rand() < 0.1 ? "0" : string(lb)
+    sub = rand() < 0.1 ? "*" : string(ub)
+
+    return "$slb-$sub"
+end
+
+"""
+Generates a random graph with 2 planted solutions (or quasi-solutions if sat==false).
+With the right parameters, this is quite hard to solve for large sizes.
+For added fun, the two planted solutions are cycles.
+We want the solver to find the best of the two, of course.
+This is an extremely unrealistic scenario and it's only intended to stress-test the solver.
+Note that the "problematic" output assumes that all non-planted versions will be
+uninstallable, which is only the case for some regimes of the parameters (e.g. large
+enough d).
+"""
+function generate_nasty(n::Int,             # size of planted solutions
+                        m::Int;             # size of the graph
+                        k::Int = 10,        # version number limit
+                        q::Int = 10,        # versions per package (upper bound)
+                        d::Int = 10,        # neighbors per package
+                        seed::Integer = 32524,
+                        sat::Bool = true    # create a satisfiable problem?
+                       )
+    @assert m ≥ n
+    d ≤ m-1 || warn("d=$d, should be ≤ m-1=$(m-1)")
+
+    srand(seed)
+
+    allvers = [sort(unique(randvers(k) for j = 1:q)) for i = 1:m]
+
+    planted1 = [rand(2:length(allvers[i])) for i = 1:n]
+
+    planted2 = [rand(1:(planted1[i]-1)) for i = 1:n]
+
+    deps = []
+    problematic = []
+
+    # random dependencies
+    for i = 1:m, j = 1:length(allvers[i])
+        if i ≤ n && (planted1[i] == j || planted2[i] == j)
+            if j == planted1[i]
+                if i < n
+                    push!(deps, [pn(i), allvers[i][j], pn(i+1), "$(allvers[i+1][planted1[i+1]])-*"])
+                else
+                    if !sat
+                        push!(deps, [pn(i), allvers[i][j], pn(1), "0-$(allvers[1][planted2[1]])"])
+                    else
+                        push!(deps, [pn(i), allvers[i][j], pn(1), "0-*"])
+                    end
+                end
+            else # j == planted2[i]
+                if i < n
+                    push!(deps, [pn(i), allvers[i][j], pn(i+1), "0-$(allvers[i+1][planted2[i+1]])"])
+                else
+                    if !sat
+                        push!(deps, [pn(i), allvers[i][j], pn(1), "$(allvers[1][planted1[1]])-*"])
+                    else
+                        push!(deps, [pn(i), allvers[i][j], pn(1), "0-*"])
+                    end
+                end
+            end
+            sat || push!(problematic, [pn(i), allvers[i][j]])
+            continue
+        end
+
+        s = shuffle([1:(i-1); (i+1):m])[1:min(d,m-1)]
+        for a in s
+            push!(deps, [pn(i), allvers[i][j], pn(a), randvspec(k)])
+        end
+        push!(problematic, [pn(i), allvers[i][j]])
+    end
+
+    reqs = [[pn(1), "*"]]
+    # reqs = [[pn(1), string(allvers[1][planted1[1]])]]
+
+    # info("SOLUTION: $([(i,planted1[i]) for i = 1:n])")
+    # info("REST: $([(i,length(allvers[i])+1) for i = (n+1):m])")
+
+    want = Dict(pn(i) => allvers[i][planted1[i]] for i = 1:n)
+
+    return deps, reqs, want, problematic
+end
+
+end # module
diff --git a/test/resolve.jl b/test/resolve.jl
index ed9d18691b91b..b58e0bdadbe24 100644
--- a/test/resolve.jl
+++ b/test/resolve.jl
@@ -148,7 +148,7 @@ function graph_from_data(deps_data, uuid_to_name = Dict{UUID,String}(Types.uuid_
             end
         end
     end
-    return Graph(all_versions, all_deps, all_compat, uuid_to_name, Requires(), fixed)
+    return Graph(all_versions, all_deps, all_compat, uuid_to_name, Requires(), fixed; verbose = VERBOSE)
 end
 function reqs_from_data(reqs_data, graph::Graph)
     reqs = Dict{UUID,VersionSpec}()
@@ -164,14 +164,14 @@ function reqs_from_data(reqs_data, graph::Graph)
     reqs
 end
 function sanity_tst(deps_data, expected_result; pkgs=[])
-    graph = graph_from_data(deps_data)
-    id(p) = pkgID(pkguuid(p), graph)
     if VERBOSE
         println()
         info("sanity check")
-        @show deps_data
-        @show pkgs
+        # @show deps_data
+        # @show pkgs
     end
+    graph = graph_from_data(deps_data)
+    id(p) = pkgID(pkguuid(p), graph)
     result = sanity_check(graph, Set(pkguuid(p) for p in pkgs), verbose = VERBOSE)
 
     length(result) == length(expected_result) || return false
@@ -183,25 +183,18 @@ function sanity_tst(deps_data, expected_result; pkgs=[])
 end
 sanity_tst(deps_data; kw...) = sanity_tst(deps_data, []; kw...)
 
-function resolve_tst(deps_data, reqs_data, want_data = nothing)
+function resolve_tst(deps_data, reqs_data, want_data = nothing; clean_graph = false)
     if VERBOSE
         println()
         info("resolving")
-        @show deps_data
-        @show reqs_data
+        # @show deps_data
+        # @show reqs_data
     end
     graph = graph_from_data(deps_data)
     reqs = reqs_from_data(reqs_data, graph)
     add_reqs!(graph, reqs)
-
-    simplify_graph!(graph)
+    simplify_graph!(graph, clean_graph = clean_graph)
     want = resolve(graph)
-
-    # rlog = get_resolve_log(graph)
-    # info(sprint(io->showlog(io, rlog)))
-    # println()
-    # info(sprint(io->showlog(io, rlog, view=:chronological)))
-
     return want == wantuuids(want_data)
 end
 
@@ -564,13 +557,27 @@ reqs_data = Any[
 want_data = Dict("A"=>v"1", "B"=>v"2", "C"=>v"2", "D"=>v"2", "E"=>v"2")
 @test resolve_tst(deps_data, reqs_data, want_data)
 
-VERBOSE && info("SCHEME 11")
+VERBOSE && info("SCHEME REALISTIC")
 ## DEPENDENCY SCHEME 11: A REALISTIC EXAMPLE
-## ref issue #21485
+## ref Julia issue #21485
 
 include("resolvedata1.jl")
 
 @test sanity_tst(deps_data, problematic_data)
 @test resolve_tst(deps_data, reqs_data, want_data)
 
+VERBOSE && info("SCHEME NASTY")
+## DEPENDENCY SCHEME 12: A NASTY CASE
+
+include("NastyGenerator.jl")
+deps_data, reqs_data, want_data, problematic_data = NastyGenerator.generate_nasty(5, 20, q=20, d=4, sat = true)
+
+@test sanity_tst(deps_data, problematic_data)
+@test resolve_tst(deps_data, reqs_data, want_data)
+
+deps_data, reqs_data, want_data, problematic_data = NastyGenerator.generate_nasty(5, 20, q=20, d=4, sat = false)
+
+@test sanity_tst(deps_data, problematic_data)
+@test_throws PkgError resolve_tst(deps_data, reqs_data)
+
 end # module