demystify 0.4.0

use std::collections::{BTreeMap, BTreeSet};
use std::sync::Arc;

use itertools::Itertools;
use rayon::iter::{ParallelBridge, ParallelIterator};
use rustsat::types::Lit;
use serde::{Deserialize, Serialize};
use tracing::info;

use crate::{
    json::{DescriptionStatement, Problem, VerboseSection},
    named_strategy::{Database, FamilyMap, display_name, fingerprint},
    problem::{
        VarValPair, format_puzvar,
        musdict::{MusContext, merge_muscontexts},
    },
    satcore::get_solver_calls,
    time::Instant,
    web::create_html,
};

use super::{
    PuzLit,
    musdict::MusDict,
    parse::PuzzleParse,
    solver::{MusConfig, PuzzleSolver, SolverConfig},
};

#[derive(Copy, Clone, Debug, Default, PartialEq, Serialize, Deserialize, clap::ValueEnum)]
pub enum MusMethod {
    /// Raw SAT cores only: get cores for all lits, minimise the smallest.
    Core,
    /// Standard MUS search (no core pre-pass).
    Mus,
    /// Hybrid: size-1 pass, then cores, then full MUS if needed.
    #[default]
    #[value(name = "core+mus")]
    CorePlusMus,
}

#[derive(Copy, Clone, Serialize, Deserialize)]
pub struct PlannerConfig {
    pub mus_config: MusConfig,
    pub merge_small_threshold: i64,
    pub skip_small_threshold: i64,
    pub expand_to_all_deductions: bool,
    /// Stop after this many solve steps. `None` means run to completion.
    pub max_steps: Option<usize>,
    /// Which MUS generation algorithm to use.
    pub mus_method: MusMethod,
    /// Attach diagnostic [`crate::json::VerboseSection`]s to every
    /// rendered step.  Off by default; CLI: `--verbose`.  When true,
    /// each step's `Problem.state.verbose` is populated with at least
    /// a "$#VAR domains" section (and future entries — strategy
    /// chosen, per-step timing, etc. — slot in alongside without new
    /// flags).
    pub verbose: bool,
}

impl Default for PlannerConfig {
    fn default() -> Self {
        Self {
            mus_config: MusConfig::default(),
            merge_small_threshold: 1,
            skip_small_threshold: 0,
            expand_to_all_deductions: true,
            max_steps: None,
            mus_method: MusMethod::default(),
            verbose: false,
        }
    }
}

/// User-facing form of a single MUS produced by the planner.
///
/// Carries the deduced literals, the human-readable constraint descriptions,
/// the canonical-form fingerprint of the MUS structure (always present —
/// useful for DB curation), and an optional matched technique name (set when
/// the fingerprint hits an entry in the configured `Database`).
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct UserMus {
    pub lits: BTreeSet<PuzLit>,
    pub constraints: Vec<String>,
    /// Canonical-form `MusFingerprint` string. Always set so DB curators can
    /// inspect the fingerprint of any MUS in the GUI/JSON output.
    pub fingerprint: String,
    /// Matched technique name, possibly with an orientation prefix (e.g.
    /// "Row hidden single"). `None` when no DB entry matched the fingerprint.
    pub name: Option<String>,
}

/// The `PuzzlePlanner` struct represents a puzzle planner that can be used to solve puzzles.
///
/// `Clone` produces an exact memcpy of all cached deductive state — the
/// trivially-deduced `knownlits`, the `tosolvelits` cache, the
/// `mus_cache` — so a base planner can be built once (paying the
/// `mark_trivial_lits_as_deduced` cost) and cloned cheaply to explore
/// many forward branches from the same point.  See also
/// [`PuzzlePlanner::fork`] for the checkpoint/restore variant which
/// drops cached forward work and replays known lits from scratch.
#[derive(Clone)]
pub struct PuzzlePlanner {
    psolve: PuzzleSolver,
    config: PlannerConfig,
    /// Cross-step MUS cache. Adding known lits only tightens the SAT problem, so a MUS found
    /// in an earlier step is still a valid unsatisfiable subset in later steps (though it may
    /// no longer be minimal). We carry it forward so we can skip re-searching lits whose cached
    /// MUS size already meets the current search target.
    mus_cache: MusDict,
    /// Named-strategy database for fingerprint → technique name lookup.
    /// Default is empty (every lookup misses); set via `with_database`.
    strategy_db: Arc<Database>,
    /// Family-group remap applied during fingerprint computation. v1 uses
    /// identity (raw constraint families); future versions may try multiple
    /// groupings to broaden DB matches.
    family_map: FamilyMap,
}

type FilterType = Box<dyn Fn(&Lit, &mut PuzzlePlanner) -> bool>;

/// A `PuzzlePlanner` is responsible for finding minimal unsatisfiable subsets (MUSes) in a puzzle
/// and using them to generate solution steps.
///
/// The planner works by identifying the smallest sets of constraints that lead to logical deductions,
/// allowing it to generate human-understandable solution steps. It can also analyze the difficulty
/// of different parts of the puzzle and present solutions in various formats including HTML.
///
///
/// The planner can find different types of MUSes:
/// - Smallish MUSes (more efficient)
/// - All MUSes including larger ones
/// - Filtered MUSes that match specific criteria
///
/// It can also track the puzzle's state by marking literals as deduced and
/// checking overall solvability.
impl PuzzlePlanner {
    /// Creates a new `PuzzlePlanner` instance.
    ///
    /// # Arguments
    ///
    /// * `psolve` - The `PuzzleSolver` instance used for solving the puzzle.
    ///
    /// # Returns
    ///
    /// A new `PuzzlePlanner` instance.
    #[must_use]
    pub fn new(psolve: PuzzleSolver) -> PuzzlePlanner {
        let mut pp = PuzzlePlanner {
            psolve,
            config: PlannerConfig::default(),
            mus_cache: MusDict::new(),
            strategy_db: Arc::new(Database::empty()),
            family_map: FamilyMap::identity(),
        };
        pp.mark_trivial_lits_as_deduced();
        pp
    }

    /// Creates a new `PuzzlePlanner` instance with a custom configuration.
    ///
    /// # Arguments
    ///
    /// * `psolve` - The `PuzzleSolver` instance used for solving the puzzle.
    /// * `config` - The custom configuration for the planner.
    ///
    /// # Returns
    ///
    /// A new `PuzzlePlanner` instance with the specified configuration.
    #[must_use]
    pub fn new_with_config(psolve: PuzzleSolver, config: PlannerConfig) -> PuzzlePlanner {
        let mut pp = Self::new_with_config_skip_trivial_marking(psolve, config);
        pp.mark_trivial_lits_as_deduced();
        pp
    }

    /// Like [`new_with_config`](Self::new_with_config) but **skips** the one-off
    /// `mark_trivial_lits_as_deduced` pass.
    ///
    /// That pass solves once per `$#VAR` literal to find values forced by the
    /// model alone, and is only meaningful once a puzzle's givens / design are
    /// assigned.  Mystify builds its *base* planner with no design assigned (the
    /// design is pinned later, per evaluation), so the pass finds nothing and is
    /// pure overhead there -- O(#`$#VAR` lits) no-limit SAT solves, which
    /// dominate setup at larger sizes.
    ///
    /// SPECIAL / FOOTGUN: only valid when the planner's puzzle has no assigned
    /// givens or design.  If givens *are* present, skipping this silently drops
    /// genuine structural deductions.  Used by mystify for its base planner.
    #[must_use]
    pub fn new_with_config_skip_trivial_marking(
        psolve: PuzzleSolver,
        config: PlannerConfig,
    ) -> PuzzlePlanner {
        PuzzlePlanner {
            psolve,
            config,
            mus_cache: MusDict::new(),
            strategy_db: Arc::new(Database::empty()),
            family_map: FamilyMap::identity(),
        }
    }

    /// Attach a named-strategy database for fingerprint-to-name lookup.
    /// Without this, every `UserMus` returned by the planner has `name: None`
    /// (but the fingerprint string is still populated).
    ///
    /// Logs a warning for each strategy whose `orientation_group` does not
    /// match any `$#FAMILY` declaration in this puzzle's model — those
    /// entries would silently lose their orientation prefix at display time.
    #[must_use]
    pub fn with_database(mut self, db: Arc<Database>) -> Self {
        if let Some(kind) = self.psolve.puzzleparse().eprime.kind.as_deref() {
            let declared: std::collections::BTreeSet<&str> = self
                .psolve
                .puzzleparse()
                .eprime
                .families
                .keys()
                .map(String::as_str)
                .collect();
            for s in db.dangling_orientation_groups(kind, &declared) {
                tracing::warn!(target: "named_strategy",
                    "strategy DB '{}' entry '{}' references orientation_group '{}' \
                     which is not declared in the model; orientation prefix will not apply",
                    kind,
                    s.name,
                    s.orientation_group.as_deref().unwrap_or(""));
            }
        }
        self.strategy_db = db;
        self
    }

    /// Returns a [`MusDict`] of all minimal unsatisfiable subsets (MUSes) of the puzzle,
    pub fn all_smallish_muses(&mut self) -> MusDict {
        let varlits = self.psolve.get_provable_varlits().clone();
        let full_result = self.psolve.get_many_vars_small_mus_quick(
            &varlits,
            &self.config.mus_config,
            Some(self.mus_cache.clone()),
        );
        self.update_mus_cache(&full_result);
        // Return only entries for the current varlits — the full_result may also contain
        // stale entries from earlier steps that must not be seen by callers.
        Self::filter_musdict_to_lits(full_result, &varlits)
    }

    /// Returns a [`MusDict`] of all minimal unsatisfiable subsets (MUSes) of the puzzle.
    ///
    /// The returned dict keeps every MUS the search finds per literal, including strictly
    /// larger ones. Use this when analysing whether a literal has alternative explanations
    /// of different sizes (e.g. whether a deduction that needs a size-2 MUS in one model
    /// still has a size-1 MUS via another path).
    pub fn all_muses_with_larger(&mut self) -> MusDict {
        let varlits = self.psolve.get_provable_varlits().clone();
        let mut conf_clone = self.config.mus_config;
        conf_clone.find_bigger = true;
        conf_clone.find_one = false;
        conf_clone.keep_all_muses = true;
        self.psolve
            .get_many_vars_small_mus_quick(&varlits, &conf_clone, None)
    }

    /// Returns every deduction whose smallest MUS is of the globally-minimum
    /// size, one [`MusContext`] per distinct MUS (deductions sharing a MUS are
    /// merged via [`merge_muscontexts`]).
    ///
    /// This sits between `smallest_muses_with_config` (used by `best_step`,
    /// which sets `find_one = true` and so races to a single smallest MUS) and
    /// `all_muses_with_larger` (used by `difficulties`, which sets
    /// `find_bigger = true` and sizes every literal far beyond the minimum).
    /// Here `find_one = false` gives the `<=` bound so we keep *all* minimum-size
    /// MUSes, while `find_bigger = false` avoids the expensive over-search.
    ///
    /// Pure query: it never marks anything deduced.
    pub fn all_minimum_size_muses(&mut self) -> Vec<MusContext> {
        let varlits = self.psolve.get_provable_varlits().clone();
        let mut conf = self.config.mus_config;
        conf.find_one = false;
        conf.find_bigger = false;
        conf.keep_all_muses = false;
        let dict = self.psolve.get_many_vars_small_mus_quick(
            &varlits,
            &conf,
            Some(self.mus_cache.clone()),
        );
        self.update_mus_cache(&dict);
        let dict = Self::filter_musdict_to_lits(dict, &varlits);
        let muses = Self::smallest_muses_from_dict(&dict);
        merge_muscontexts(&muses)
    }

    /// Core-guided MUS search: get raw SAT cores for all provable lits,
    /// then minimise only the cores of smallest size into true MUSes.
    fn core_guided_muses(&mut self) -> MusDict {
        let varlits = self.psolve.get_provable_varlits().clone();
        let cores = self.psolve.get_all_cores(&varlits);

        if cores.is_empty() {
            return MusDict::new();
        }

        let min_size = cores.iter().map(|(_, core)| core.len()).min().unwrap();

        let smallest: Vec<_> = cores
            .into_iter()
            .filter(|(_, core)| core.len() == min_size)
            .collect();

        self.psolve.minimise_cores(&smallest)
    }

    /// Hybrid MUS search: size-1 pass, then cores, then full MUS if needed.
    fn core_plus_mus_muses(&mut self) -> MusDict {
        let varlits = self.psolve.get_provable_varlits().clone();

        // Phase 1: size-1 scan
        let size1_results: Vec<_> = varlits
            .iter()
            .par_bridge()
            .filter_map(|&lit| {
                let t0 = Instant::now();
                let ret = self.psolve.get_var_mus_size_1(lit, Some(1));
                let elapsed = t0.elapsed();
                let outcome = match &ret {
                    Ok(v) if !v.is_empty() => crate::stats::MusOutcome::Found(1),
                    Ok(_) => crate::stats::MusOutcome::NotFound,
                    Err(_) => crate::stats::MusOutcome::Timeout,
                };
                crate::stats::record_mus_search(elapsed, outcome, crate::stats::MusFunction::Size1);
                match ret {
                    Ok(v) if !v.is_empty() => {
                        let bts: BTreeSet<Lit> = v[0].iter().copied().collect();
                        Some((lit, bts))
                    }
                    _ => None,
                }
            })
            .collect();

        if !size1_results.is_empty() {
            let mut dict = MusDict::new();
            for (lit, mus) in size1_results {
                dict.add_mus(lit, mus);
            }
            self.update_mus_cache(&dict);
            return dict;
        }

        // Phase 2: get raw cores
        let cores = self.psolve.get_all_cores(&varlits);
        if cores.is_empty() {
            return MusDict::new();
        }

        let min_core_size = cores.iter().map(|(_, core)| core.len()).min().unwrap();
        info!(target: "cores", "core+mus: min core size = {min_core_size}");

        // Phase 3: if smallest core <= 2, minimise those and done
        if min_core_size <= 2 {
            let smallest: Vec<_> = cores
                .into_iter()
                .filter(|(_, core)| core.len() == min_core_size)
                .collect();
            let dict = self.psolve.minimise_cores(&smallest);
            self.update_mus_cache(&dict);
            return dict;
        }

        // Phase 4: full MUS search
        self.all_smallish_muses()
    }

    /// Returns a [`MusDict`] of all minimal unsatisfiable subsets (MUSes) of the puzzle which satisfy a filter.
    pub fn filtered_muses(&mut self, filter: FilterType) -> MusDict {
        let varlits = self.psolve.get_provable_varlits().clone();
        let varlits: BTreeSet<_> = varlits.into_iter().filter(|l| filter(l, self)).collect();
        let full_result = self.psolve.get_many_vars_small_mus_quick(
            &varlits,
            &self.config.mus_config,
            Some(self.mus_cache.clone()),
        );
        self.update_mus_cache(&full_result);
        Self::filter_musdict_to_lits(full_result, &varlits)
    }

    /// Updates the MUS cache from a search result, skipping size-0 MUSes (trivial deductions).
    fn update_mus_cache(&mut self, result: &MusDict) {
        for (lit, mus_set) in result.muses() {
            for mc in mus_set {
                if !mc.mus.is_empty() {
                    self.mus_cache.add_mus(*lit, mc.mus.clone());
                }
            }
        }
    }

    /// Filters a `MusDict` to only contain entries whose literal is in `lits`.
    fn filter_musdict_to_lits(dict: MusDict, lits: &BTreeSet<Lit>) -> MusDict {
        let mut result = MusDict::new();
        for lit in lits {
            if let Some(mus_set) = dict.muses().get(lit) {
                for mc in mus_set {
                    result.add_mus(*lit, mc.mus.clone());
                }
            }
        }
        result
    }

    fn smallest_muses_from_dict(dict: &MusDict) -> Vec<MusContext> {
        let min = dict.min();
        if min.is_none() {
            return vec![];
        }
        let min = min.unwrap();
        let mut vec = vec![];
        for v in dict.muses().values() {
            if let Some(m) = v.iter().next()
                && m.mus_len() <= min
            {
                vec.push(m.clone());
            }
        }
        vec
    }

    fn apply_config_to_muses(&mut self, muses: Vec<MusContext>) -> Vec<MusContext> {
        if muses.is_empty() {
            return muses;
        }

        // Re-minimise each MUS: cached MUSes from earlier steps are still
        // unsatisfiable subsets but may no longer be minimal after new
        // known_lits were added.
        let muses: Vec<MusContext> = muses
            .into_iter()
            .map(|mc| {
                let lit = *mc.lits.iter().next().unwrap();
                let cons: Vec<Lit> = mc.mus.iter().copied().collect();
                match self.psolve.minimise_core_for_lit(lit, &cons) {
                    Ok(minimised) => {
                        let new_mus: BTreeSet<Lit> = minimised.into_iter().collect();
                        MusContext { mus: new_mus, ..mc }
                    }
                    Err(_) => mc,
                }
            })
            .collect();

        if cfg!(debug_assertions) {
            for mus in &muses {
                let mus_cons: Vec<Lit> = mus.mus.iter().copied().collect();
                for lit in &mus.lits {
                    self.psolve.verify_mus(*lit, &mus_cons);
                }
            }
        }

        // Re-minimisation may have shrunk some MUSes below the original
        // minimum. Re-filter to the new minimum size.
        let new_min = muses.iter().map(|mc| mc.mus_len()).min().unwrap();
        let muses: Vec<MusContext> = muses
            .into_iter()
            .filter(|mc| mc.mus_len() == new_min)
            .collect();

        let muses = merge_muscontexts(&muses);
        if muses[0].mus_len() as i64 <= self.config.merge_small_threshold {
            return muses;
        }
        if self.config.expand_to_all_deductions {
            let best = muses
                .iter()
                .map(|mc| self.psolve.get_all_lits_solved_by_mus(mc))
                .max_by_key(|mc| mc.lits.len())
                .unwrap();
            vec![best]
        } else {
            vec![muses[0].clone()]
        }
    }

    /// Returns a vector of the smallest MUSes of the puzzle.
    pub fn smallest_muses(&mut self) -> Vec<MusContext> {
        let dict = self.all_smallish_muses();
        Self::smallest_muses_from_dict(&dict)
    }

    /// Returns a vector of the smallest MUSes of the puzzle based on the planner's configuration.
    pub fn smallest_muses_with_config(&mut self) -> Vec<MusContext> {
        let muses = self.smallest_muses();
        self.apply_config_to_muses(muses)
    }

    /// Convert a `MusContext` to a `UserMus`: human-readable constraint
    /// descriptions, deduced `PuzLit`s, the canonical-form fingerprint of
    /// the MUS structure, and (if the planner has a strategy database
    /// attached and the fingerprint matches) the named-technique label.
    pub fn mus_to_user_mus(&self, mc: &MusContext) -> UserMus {
        let parse = self.psolve.puzzleparse();
        let lits: BTreeSet<PuzLit> = mc
            .lits
            .iter()
            .flat_map(|l| parse.lit_to_vars(l))
            .cloned()
            .collect();

        // Mystify uses the `puz_` prefix to mark design variables — the
        // clue cells, colour layout, etc. that the generator chose.  These
        // are meant to be pinned via `--pin-assignment` (see
        // `PuzzleSolver::pin_assignment`); demystify deducing one of them
        // means the user forgot to supply the assignment and the resulting
        // MUS would be a meaningless statement about how the generator
        // could have made a different choice.  Crash with a pointed
        // message rather than emit it.
        for lit in &lits {
            if lit.var().name().starts_with("puz_") {
                panic!(
                    "MUS produced a deduction on `{lit}`, but variables starting \
                     with `puz_` are mystify model design variables — they must be \
                     pinned, not deduced.  Use `--pin-assignment <FILE>` to set \
                     these variables from a mystify output JSON."
                );
            }
        }

        let constraints: Vec<String> = mc
            .mus
            .iter()
            .map(|c| parse.lit_to_con(c))
            .cloned()
            .collect_vec();
        let fp = fingerprint(parse, mc, &self.family_map);
        let name = parse
            .eprime
            .kind
            .as_deref()
            .and_then(|kind| self.strategy_db.lookup(kind, &fp))
            .map(|s| display_name(s, mc, parse));
        UserMus {
            lits,
            constraints,
            fingerprint: fp.into_canonical(),
            name,
        }
    }

    /// Deal with MUSes of 0 (which mean the puzzle has deduction that can be made without
    /// any 'user' constraints. These often arise from initial setup.
    pub fn mark_trivial_lits_as_deduced(&mut self) {
        let varlits = self.psolve.get_provable_varlits().clone();
        let trivial_lits = self.psolve.get_many_vars_mus_size_0(&varlits);
        for l in trivial_lits {
            self.mark_lit_as_deduced(&l);
        }
    }

    /// Marks a literal as deduced.
    ///
    /// This method should only be called if there are no solutions with the negation of the literal.
    ///
    /// # Arguments
    ///
    /// * `lit` - The literal to mark as deduced.
    pub fn mark_lit_as_deduced(&mut self, lit: &Lit) {
        self.psolve.add_known_lit(*lit);
    }

    /// Mark a literal as fixed (not a deduction).  Unlike
    /// [`Self::mark_lit_as_deduced`], this bypasses the provability
    /// assertion — the caller accepts that the literal is an axiom, not
    /// proved by the solver, and that adding it may make the puzzle
    /// unsolvable or invalidate cached state.
    pub fn mark_lit_as_fixed(&mut self, lit: &Lit) {
        self.psolve.add_not_provable_known_lit(*lit);
    }

    /// Marks multiple literals as deduced.
    ///
    /// This method should only be called if there are no solutions with the negation of the literals.
    ///
    /// # Arguments
    ///
    /// * `lits` - A slice of literals to mark as deduced.
    pub fn mark_lits_as_deduced(&mut self, lits: &[Lit]) {
        for lit in lits {
            self.psolve.add_known_lit(*lit);
        }
    }

    /// Returns a reference to the vector of all known literals.
    ///
    /// This includes literals that have been marked as deduced and literals from 'REVEAL' statements.
    ///
    /// # Returns
    ///
    /// A reference to the vector of all known literals.
    pub fn get_all_known_lits(&self) -> &Vec<Lit> {
        self.psolve.get_known_lits()
    }

    /// Solves the puzzle quickly and returns a sequence of steps.
    pub fn quick_solve(&mut self) -> Vec<Vec<UserMus>> {
        let mut solvesteps = vec![];
        'litloop: while !self.psolve.get_provable_varlits().is_empty() {
            if self.config.max_steps.is_some_and(|n| solvesteps.len() >= n) {
                break;
            }
            let _step_timer = crate::stats::PhaseTimer::solve_step();

            let cores_enabled = tracing::enabled!(target: "cores", tracing::Level::INFO);

            let (core_min, core_count_1) =
                if cores_enabled && self.config.mus_method == MusMethod::Mus {
                    let varlits = self.psolve.get_provable_varlits().clone();
                    self.psolve.core_size_summary(&varlits)
                } else {
                    (None, 0)
                };

            let (muses, mus_count_1) = match self.config.mus_method {
                MusMethod::Core => {
                    let dict = self.core_guided_muses();
                    let raw = Self::smallest_muses_from_dict(&dict);
                    (self.apply_config_to_muses(raw), 0)
                }
                MusMethod::CorePlusMus => {
                    let dict = self.core_plus_mus_muses();
                    let count_1 = if cores_enabled {
                        dict.count_at_size(1)
                    } else {
                        0
                    };
                    let raw = Self::smallest_muses_from_dict(&dict);
                    (self.apply_config_to_muses(raw), count_1)
                }
                MusMethod::Mus if cores_enabled => {
                    let dict = self.all_smallish_muses();
                    let count_1 = dict.count_at_size(1);
                    let raw = Self::smallest_muses_from_dict(&dict);
                    (self.apply_config_to_muses(raw), count_1)
                }
                MusMethod::Mus => (self.smallest_muses_with_config(), 0),
            };

            // The whole pipeline runs under the global conflict limit, kept
            // deliberately low so we don't sink time into the huge MUSes (200+
            // constraints) we don't want — the search returns quickly with the
            // small ones we do.  But on a hard step every remaining literal's
            // smallest MUS can sit just past the current budget, so the pass finds
            // nothing.  Don't give up, and don't commit to whichever single
            // literal happens to be cheapest (its smallest MUS might be enormous):
            // raise the global budget and retry the whole pass, keeping the search
            // smallest-first with more effort.  A provable literal always has a
            // MUS, so a large enough budget eventually surfaces one.
            if muses.is_empty() {
                let (old, new) = crate::satcore::multiply_global_conflict_limit(10);
                assert!(
                    new > old,
                    "quick_solve: no MUS found with {} provable lit(s) remaining, but the \
                     conflict limit ({old}) is already unlimited — a provable literal must have a MUS",
                    self.psolve.get_provable_varlits().len(),
                );
                info!(target: "planner",
                    "quick_solve: pass found no MUS within budget; raised conflict limit {old} -> {new} and retrying");
                continue 'litloop;
            }

            for mus in &muses {
                let mus_cons: Vec<Lit> = mus.mus.iter().copied().collect();
                for lit in &mus.lits {
                    self.psolve.verify_mus_provability(*lit, &mus_cons);
                }
            }

            for mus in &muses {
                for lit in &mus.lits {
                    self.mark_lit_as_deduced(lit);
                }
            }

            if !muses.is_empty() && muses[0].mus_len() as i64 <= self.config.skip_small_threshold {
                info!(target: "cores",
                    "Step {} (skipped): core min={} #1={}, true MUS min={} #1={}",
                    solvesteps.len(),
                    core_min.map_or("none".to_string(), |v| v.to_string()),
                    core_count_1,
                    muses[0].mus_len(),
                    mus_count_1,
                );
                continue 'litloop;
            }
            let muses = muses
                .into_iter()
                .map(|mus| self.mus_to_user_mus(&mus))
                .collect_vec();

            info!(target: "cores",
                "Step {}: core min={} #1={}, true MUS min={} #1={}",
                solvesteps.len(),
                core_min.map_or("none".to_string(), |v| v.to_string()),
                core_count_1,
                muses[0].constraints.len(),
                mus_count_1,
            );

            info!(target: "progress",
                "{} steps, just found {} muses of size {}, {} left, {} solver calls so far",
                solvesteps.len(),
                muses.len(),
                muses[0].constraints.len(),
                self.psolve.get_provable_varlits().len(),
                get_solver_calls(),
            );

            solvesteps.push(muses);
        }
        info!(target: "planner", "solved!");
        solvesteps
    }

    /// One cost-tiered greedy pass at MUS-size bound `bound`.
    ///
    /// Tier 1 (cheap): grab a raw core for every provable literal — one SAT call
    /// each.  If *any* raw core is already `≤ bound`, accept those literals and
    /// return.  The accepted cores are then minimised into true (irreducible)
    /// MUSes so the step is readable — this is cheap because we only minimise
    /// cores already known to be `≤ bound` (the huge cores are never touched),
    /// and it cannot change which literals we deduce, only how tightly each is
    /// explained.
    ///
    /// Tier 2 (only when no raw core qualified): bounded-minimise the cores we
    /// already hold, accepting any that drop to `≤ bound`.
    ///
    /// Returns the accepted MUSes (every one of size `≤ bound`), or an empty
    /// vector when nothing could be brought under the bound this pass — the
    /// signal for [`Self::quick_solve_greedy`] to run the frontier search.
    fn greedy_pass(&mut self, bound: i64) -> Vec<MusContext> {
        let varlits = self.psolve.get_provable_varlits().clone();
        if varlits.is_empty() {
            return vec![];
        }

        // Tier 1: raw cores; minimise the ones already small enough to accept.
        let cores = self.psolve.get_all_cores(&varlits);
        if cores.is_empty() {
            return vec![];
        }

        let tier1: Vec<MusContext> = cores
            .iter()
            .filter(|(_, core)| core.len() as i64 <= bound)
            .par_bridge()
            .map(|(lit, core)| {
                // Already ≤ bound, so this is a small minimisation.  If the
                // solver hits a limit, the raw core is still a valid (if
                // non-minimal) explanation, so fall back to it.
                let mus = match self.psolve.minimise_core_for_lit(*lit, core) {
                    Ok(m) => m,
                    Err(_) => core.clone(),
                };
                MusContext::new(*lit, mus.into_iter().collect())
            })
            .collect();
        if !tier1.is_empty() {
            return merge_muscontexts(&tier1);
        }

        // Tier 2: bounded minimisation of the cores already in hand.
        let tier2: Vec<MusContext> = self
            .psolve
            .minimise_cores_bounded(&cores, bound)
            .into_iter()
            .map(|(lit, mus)| MusContext::new(lit, mus.into_iter().collect()))
            .collect();
        merge_muscontexts(&tier2)
    }

    /// Thorough "harvest" pass: gather *every* provable literal that has a MUS of
    /// size ≤ `target` in a single flat all-literals search, and return them
    /// merged, ready to apply together.
    ///
    /// This sits between [`Self::greedy_pass`] (cheap, low recall) and the tight
    /// frontier search in [`Self::quick_solve_greedy`].  When the cheap pass
    /// stalls but the running maximum has *not* been reached, one harvest clears
    /// the whole backlog at the current size — instead of re-paying the expensive
    /// smallest-MUS search once per remaining literal of that size.  It does not
    /// raise the maximum (everything it returns is ≤ `target`).
    fn harvest_up_to(&mut self, target: i64) -> Vec<MusContext> {
        let varlits = self.psolve.get_provable_varlits().clone();
        if varlits.is_empty() {
            return vec![];
        }
        let found = self.psolve.get_muses_up_to(&varlits, target);
        let muses: Vec<MusContext> = found
            .into_iter()
            .map(|(lit, mus)| MusContext::new(lit, mus.into_iter().collect()))
            .collect();
        merge_muscontexts(&muses)
    }

    /// Select the next greedy step's MUSes, advancing `current_max` if the step
    /// raised the running maximum.  Does **not** mark anything deduced — the
    /// caller applies the returned MUSes (so the same selection logic drives both
    /// [`Self::quick_solve_greedy`] and [`Self::quick_solve_greedy_html`]).
    ///
    /// Escalates cheapest-first: a [`Self::greedy_pass`] at the current bound,
    /// then (if that stalls and the bound is ≥ 2) a thorough [`Self::harvest_up_to`]
    /// of everything ≤ `current_max`, and only if *that* also stalls the tight
    /// `smallest_muses_with_config` frontier search — the sole place `current_max`
    /// can rise.  Returns an empty vector only when the puzzle is fully solved.
    fn next_greedy_step(&mut self, current_max: &mut i64) -> Vec<MusContext> {
        let muses = self.greedy_pass(*current_max);
        if !muses.is_empty() {
            return muses;
        }

        // Cheap pass stalled but the maximum is ≥ 2: try a thorough harvest of
        // everything ≤ current_max before paying for the tight search.  (At
        // current_max ≤ 1 the frontier's size-1 scan is the better tool.)
        if *current_max >= 2 {
            let harvested = self.harvest_up_to(*current_max);
            if !harvested.is_empty() {
                return harvested;
            }
        }

        // Genuinely nothing ≤ current_max: run the tight smallest-MUS search to
        // find the new minimum.  This is the only place `current_max` can rise.
        let frontier = self.smallest_muses_with_config();
        if frontier.is_empty() {
            return vec![];
        }
        let m = frontier.iter().map(|mc| mc.mus_len()).max().unwrap() as i64;
        *current_max = (*current_max).max(m);
        frontier
    }

    /// Solve the puzzle greedily, optimised to find the largest MUS in the solve
    /// path as fast as possible.
    ///
    /// [`Self::quick_solve`] runs a full smallest-MUS search every step.  This
    /// instead clears every deduction reachable at or below the largest MUS size
    /// seen so far with cheap bounded passes ([`Self::greedy_pass`] /
    /// [`Self::harvest_up_to`]), and only pays for a full smallest-MUS search when
    /// those passes stall — which is the *only* place the running maximum can
    /// rise.  Greedy minimisation is incomplete, so a stall does not by itself
    /// prove no small MUS remains; the maximum is therefore only ever raised by
    /// the frontier search, whose result is a true minimum (so the reported
    /// maximum cannot over-report).
    ///
    /// Conceptually this is `--merge` with a threshold that auto-discovers the
    /// puzzle's difficulty: each step applies every deduction whose MUS is ≤ the
    /// largest size seen so far, instead of a fixed `--merge N`.  Every displayed
    /// MUS is minimised (irreducible), so the output is as readable as
    /// [`Self::quick_solve`]'s; only the *order* differs (a single step may mix
    /// sizes rather than grouping by exact size).
    pub fn quick_solve_greedy(&mut self) -> Vec<Vec<UserMus>> {
        let mut solvesteps = vec![];
        let mut current_max: i64 = 0;
        while !self.psolve.get_provable_varlits().is_empty() {
            if self.config.max_steps.is_some_and(|n| solvesteps.len() >= n) {
                break;
            }
            let _step_timer = crate::stats::PhaseTimer::solve_step();

            let muses = self.next_greedy_step(&mut current_max);
            if muses.is_empty() {
                break;
            }

            for mus in &muses {
                let mus_cons: Vec<Lit> = mus.mus.iter().copied().collect();
                for lit in &mus.lits {
                    self.psolve.verify_mus_provability(*lit, &mus_cons);
                }
            }

            for mus in &muses {
                for lit in &mus.lits {
                    self.mark_lit_as_deduced(lit);
                }
            }

            let muses = muses
                .into_iter()
                .map(|mus| self.mus_to_user_mus(&mus))
                .collect_vec();

            info!(target: "progress",
                "greedy: {} steps, applied {} muses (max size so far {}), {} left, {} solver calls so far",
                solvesteps.len(),
                muses.len(),
                current_max,
                self.psolve.get_provable_varlits().len(),
                get_solver_calls(),
            );

            solvesteps.push(muses);
        }
        info!(target: "planner", "greedy solved!");
        solvesteps
    }

    /// HTML rendering of a greedy solve: same step selection as
    /// [`Self::quick_solve_greedy`], rendered with the shared per-step HTML
    /// builder used by [`Self::quick_solve_html`].
    pub fn quick_solve_greedy_html(&mut self) -> String {
        let mut html = String::new();
        let mut current_max: i64 = 0;
        while !self.psolve.get_provable_varlits().is_empty() {
            let muses = self.next_greedy_step(&mut current_max);
            let (new_html, lits) = if muses.is_empty() {
                self.quick_display_html_step_impl(None, "There are no more values to deduce")
            } else {
                self.quick_display_html_step(Some(muses))
            };
            html += &new_html;
            self.mark_lits_as_deduced(&lits);
            html += "<br/>";
        }
        html
    }

    /// Checks the solvability of the current problem state. This can be used
    /// to both check if a problem is inconsistent, or how much of the problem
    /// does not have a unique solution
    ///
    /// # Returns
    /// - `Some(i64)`: If the problem is not inconsistent, return the number of literals
    ///   which are not fixed to a single value.
    /// - `None`: If the problem is has no solution.
    pub fn check_solvability(&mut self) -> Option<i64> {
        while !self.psolve.get_provable_varlits().is_empty() {
            let lits = self.psolve.get_provable_varlits().clone();

            for l in lits {
                self.mark_lit_as_deduced(&l);
            }
        }

        if self.psolve.is_currently_solvable() {
            let lits = self.psolve.get_literals_to_try_solving();

            for l in &lits {
                self.solver().lit_to_puzlit(l);
            }

            Some(lits.len().try_into().unwrap())
        } else {
            None
        }
    }

    /// Cheaply tests whether the puzzle has exactly one solution.
    ///
    /// Unlike [`Self::check_solvability`], this does **not** enumerate forced
    /// literals: it finds one solution and re-solves once with that solution
    /// blocked over the puzzle's decision variables.  Returns `true` iff
    /// exactly one solution exists; an unsolvable puzzle (and a puzzle with
    /// multiple solutions) returns `false`.  Any literals pinned beforehand
    /// (a partial assignment) are respected.
    pub fn is_uniquely_solvable(&mut self) -> bool {
        self.psolve.is_uniquely_solvable()
    }

    /// Returns the solution variables that could not be uniquely determined after
    /// exhausting all constraint propagation.
    ///
    /// This is meaningful only after `check_solvability()` or `quick_solve()` has been
    /// called, which exhausts all deductions. Before that call, the result is undefined.
    ///
    /// Each returned `PuzVar` is a variable whose value is not pinned to a single value
    /// by the current set of puzzle clues. Returns an empty set if the puzzle is fully
    /// solvable (all variables determined) or inconsistent (no solution).
    pub fn unsolved_vars_after_solve(&mut self) -> BTreeSet<super::PuzVar> {
        let lits = self.psolve.get_literals_to_try_solving();
        lits.iter()
            .flat_map(|lit| {
                self.psolve
                    .puzzleparse()
                    .lit_to_vars(lit)
                    .iter()
                    .map(|puzlit| puzlit.var())
                    .collect::<Vec<_>>()
            })
            .collect()
    }

    pub fn get_provable_varlits(&mut self) -> BTreeSet<Lit> {
        self.psolve.get_provable_varlits().clone()
    }

    pub fn get_provable_varlits_including_reveals(&mut self) -> BTreeSet<Lit> {
        let mut all_lits = BTreeSet::new();

        while !self.psolve.get_provable_varlits().is_empty() {
            let varlits = self.psolve.get_provable_varlits().clone();

            for v in &varlits {
                self.mark_lit_as_deduced(v);
            }

            all_lits.extend(varlits);
        }

        all_lits
    }

    /// Solves the puzzle quickly and returns a sequence of steps in HTML format.
    ///
    /// # Returns
    ///
    /// A string containing the HTML representation of the solution steps.
    pub fn quick_solve_html(&mut self) -> String {
        let mut html = String::new();
        while !self.psolve.get_provable_varlits().is_empty() {
            let (new_html, lits) = self.quick_solve_html_step();
            html += &new_html;
            self.mark_lits_as_deduced(&lits);
            html += "<br/>";
        }
        html
    }

    pub fn quick_solve_html_step(&mut self) -> (String, Vec<Lit>) {
        let base_muses = self.smallest_muses_with_config();
        if base_muses.is_empty() {
            return self.quick_display_html_step_impl(None, "There are no more values to deduce");
        }
        self.quick_display_html_step(Some(base_muses))
    }

    pub fn quick_display_html_step(
        &mut self,
        base_muses: Option<Vec<MusContext>>,
    ) -> (String, Vec<Lit>) {
        self.quick_display_html_step_impl(base_muses, "The initial puzzle state")
    }

    /// Diagnostic sections to attach to a step's `State.verbose`.  Called
    /// from each Problem-building site when `PlannerConfig::verbose` is on.
    ///
    /// Returns `None` when verbose mode is off — the call site assigns
    /// straight through to `state.verbose`, so the JSON field stays
    /// absent for non-verbose runs.
    ///
    /// First (and currently only) section is `"Variable domains"`: every
    /// instance of every `$#VAR` with its current set of still-possible
    /// values.  Reads from the solver's `direct.domainmap` (the initial
    /// domain) and prunes values whose `!=` lit is already known.
    fn build_verbose_sections(&self) -> Option<Vec<VerboseSection>> {
        if !self.config.verbose {
            return None;
        }

        let pp = self.psolve.puzzleparse();

        // Collect known PuzLits once — we'll classify each (var, val)
        // pair below.
        let known_puzlits: BTreeSet<PuzLit> = self
            .get_all_known_lits()
            .iter()
            .flat_map(|l| self.psolve.lit_to_puzlit(l))
            .cloned()
            .collect();

        // Group PuzVar instances by their `$#VAR` name so the output
        // sections track the model's variable structure.  Variables not
        // declared as `$#VAR` (auxiliaries, framework `puz_*`, constraint
        // bools) are skipped; they're rarely useful for "what's going
        // on with this variable" debugging.
        let mut by_name: BTreeMap<&str, Vec<&super::PuzVar>> = BTreeMap::new();
        for var in pp.direct.domainmap.keys() {
            if pp.eprime.vars.contains(var.name()) {
                by_name.entry(var.name().as_str()).or_default().push(var);
            }
        }

        let mut body = String::new();
        for (name, vars) in &by_name {
            body.push_str(&format!("$#VAR {name}:\n"));
            for var in vars {
                let initial = &pp.direct.domainmap[var];
                let var_str = format_puzvar(var);

                // Partition the initial domain by current knowledge.
                let mut pinned: Option<i64> = None;
                let mut still_possible: Vec<i64> = Vec::new();
                for &val in initial {
                    let vvp = VarValPair::new(var, val);
                    if known_puzlits.contains(&PuzLit::new_eq(vvp.clone())) {
                        pinned = Some(val);
                        break;
                    }
                    if !known_puzlits.contains(&PuzLit::new_neq(vvp)) {
                        still_possible.push(val);
                    }
                }

                if let Some(v) = pinned {
                    body.push_str(&format!("  {var_str} = {v}\n"));
                } else if still_possible.len() == initial.len() {
                    body.push_str(&format!(
                        "  {var_str} ∈ {{{}}} (untouched)\n",
                        still_possible
                            .iter()
                            .map(i64::to_string)
                            .collect::<Vec<_>>()
                            .join(", ")
                    ));
                } else {
                    body.push_str(&format!(
                        "  {var_str} ∈ {{{}}}\n",
                        still_possible
                            .iter()
                            .map(i64::to_string)
                            .collect::<Vec<_>>()
                            .join(", ")
                    ));
                }
            }
            body.push('\n');
        }

        Some(vec![VerboseSection {
            title: "Variable domains".to_owned(),
            body,
        }])
    }

    fn build_step_problem(
        &mut self,
        base_muses: Option<Vec<MusContext>>,
        fallback_description: &str,
    ) -> (Problem, Vec<Lit>) {
        let (mut problem, lits) = self.build_step_problem_inner(base_muses, fallback_description);
        if let Some(verbose) = self.build_verbose_sections()
            && let Some(state) = problem.state.as_mut()
        {
            state.verbose = Some(verbose);
        }
        (problem, lits)
    }

    fn build_step_problem_inner(
        &mut self,
        base_muses: Option<Vec<MusContext>>,
        fallback_description: &str,
    ) -> (Problem, Vec<Lit>) {
        if let Some(base_muses) = base_muses {
            let muses = base_muses
                .iter()
                .map(|mus| self.mus_to_user_mus(mus))
                .collect_vec();

            let all_deduced: BTreeSet<_> = muses.iter().flat_map(|x| x.lits.clone()).collect();

            let pre_string = if base_muses.len() > 1 {
                format!(
                    "{} simple deductions are being shown here in a single step. <br/>",
                    base_muses.len()
                )
            } else {
                "Made the following deductions:<br/>".to_owned()
            };

            let mut description_list: Vec<DescriptionStatement> = Vec::new();
            for mus in &muses {
                let deduced = PuzLit::nice_puzlit_list_html(&mus.lits);
                description_list.push(DescriptionStatement {
                    result: deduced,
                    constraints: mus.constraints.clone(),
                    name: mus.name.clone(),
                    fingerprint: Some(mus.fingerprint.clone()),
                });
            }

            let v = base_muses
                .iter()
                .flat_map(|mc| &mc.lits)
                .copied()
                .collect_vec();

            for mc in &base_muses {
                let mus_cons: Vec<Lit> = mc.mus.iter().copied().collect();
                for lit in &mc.lits {
                    self.psolve.verify_mus_provability(*lit, &mus_cons);
                }
            }

            // Snapshot tosolve BEFORE marking deduced, so eliminated
            // candidates remain visible (rendered with litneg).
            let varlits = self.psolve.get_provable_varlits().clone();
            let tosolve_varvals: BTreeSet<_> = varlits
                .iter()
                .flat_map(|x| self.psolve.lit_to_puzlit(x))
                .map(super::PuzLit::varval)
                .collect();

            for m in &v {
                self.mark_lit_as_deduced(m);
            }

            let known_lits = self.get_all_known_lits().clone();
            let known_puzlits: BTreeSet<PuzLit> = known_lits
                .iter()
                .flat_map(|x| self.psolve.lit_to_puzlit(x))
                .cloned()
                .collect();

            let problem = Problem::new_from_puzzle_and_mus(
                &self.psolve,
                &tosolve_varvals,
                &known_puzlits,
                &all_deduced,
                &description_list,
                &pre_string,
                false,
            )
            .expect("Cannot make puzzle json");

            (problem, v)
        } else {
            let varlits = self.psolve.get_provable_varlits().clone();

            let tosolve_varvals: BTreeSet<_> = varlits
                .iter()
                .flat_map(|x| self.psolve.lit_to_puzlit(x))
                .map(super::PuzLit::varval)
                .collect();

            let known_puzlits: BTreeSet<PuzLit> = self
                .get_all_known_lits()
                .iter()
                .flat_map(|x| self.psolve.lit_to_puzlit(x))
                .cloned()
                .collect();

            let deduced = BTreeSet::new();

            let problem = Problem::new_from_puzzle_and_state(
                &self.psolve,
                &tosolve_varvals,
                &known_puzlits,
                &deduced,
                fallback_description,
            )
            .expect("Cannot make puzzle json");

            (problem, vec![])
        }
    }

    fn quick_display_html_step_impl(
        &mut self,
        base_muses: Option<Vec<MusContext>>,
        fallback_description: &str,
    ) -> (String, Vec<Lit>) {
        let (problem, lits) = self.build_step_problem(base_muses, fallback_description);
        (create_html(&problem), lits)
    }

    pub fn solve_step(&mut self) -> (Problem, Vec<Lit>) {
        let base_muses = self.smallest_muses_with_config();
        if base_muses.is_empty() {
            return self.build_step_problem(None, "There are no more values to deduce");
        }
        self.build_step_problem(Some(base_muses), "Made the following deductions")
    }

    pub fn refresh_problem(&mut self) -> (Problem, Vec<Lit>) {
        self.build_step_problem(None, "Current puzzle state")
    }

    /// Render a single MUS as a `Problem` for display without advancing solver state.
    pub fn preview_mus(&mut self, mus: &MusContext) -> Problem {
        let user_mus = self.mus_to_user_mus(mus);
        let all_deduced: BTreeSet<_> = user_mus.lits.clone();

        let description_list = vec![DescriptionStatement {
            result: PuzLit::nice_puzlit_list_html(&user_mus.lits),
            constraints: user_mus.constraints.clone(),
            name: user_mus.name.clone(),
            fingerprint: Some(user_mus.fingerprint.clone()),
        }];

        let varlits = self.psolve.get_provable_varlits().clone();
        let tosolve_varvals: BTreeSet<_> = varlits
            .iter()
            .flat_map(|x| self.psolve.lit_to_puzlit(x))
            .map(super::PuzLit::varval)
            .collect();

        let known_puzlits: BTreeSet<PuzLit> = self
            .get_all_known_lits()
            .iter()
            .flat_map(|x| self.psolve.lit_to_puzlit(x))
            .cloned()
            .collect();

        let pre_string = format!(
            "Explanation using {} constraint{}:<br/>",
            mus.mus_len(),
            if mus.mus_len() == 1 { "" } else { "s" }
        );

        Problem::new_from_puzzle_and_mus(
            &self.psolve,
            &tosolve_varvals,
            &known_puzlits,
            &all_deduced,
            &description_list,
            &pre_string,
            false,
        )
        .expect("Cannot make puzzle json")
    }

    /// All alternative MUSes for a single literal, sorted smallest to largest,
    /// each promoted to the user-facing `UserMus` form (with fingerprint and
    /// looked-up technique name).
    ///
    /// Wraps [`Self::all_muses_for_literal`] + [`Self::mus_to_user_mus`] for
    /// callers that want to enumerate alternative explanations of a single
    /// deduction without re-implementing the conversion.
    pub fn all_alternatives_for_literal(&mut self, lit_def: Vec<i64>) -> Vec<UserMus> {
        let muses = self.all_muses_for_literal(lit_def);
        muses.iter().map(|mc| self.mus_to_user_mus(mc)).collect()
    }

    /// Compute all MUSes for a single literal, sorted smallest to largest.
    pub fn all_muses_for_literal(&mut self, lit_def: Vec<i64>) -> Vec<MusContext> {
        let varlits = self.psolve.get_provable_varlits().clone();
        let lit_def_clone = lit_def.clone();
        let varlits: BTreeSet<_> = varlits
            .into_iter()
            .filter(|lit| {
                let puzlit_list = self.psolve.lit_to_puzlit(lit);
                for puzlit in puzlit_list {
                    let mut indices = puzlit.var().indices().clone();
                    indices.push(puzlit.val());
                    if indices == lit_def_clone {
                        return true;
                    }
                }
                false
            })
            .collect();

        let mut conf = self.config.mus_config;
        conf.find_bigger = true;
        conf.find_one = false;
        conf.keep_all_muses = true;

        let result = self
            .psolve
            .get_many_vars_small_mus_quick(&varlits, &conf, None);

        let mut seen = BTreeSet::new();
        let mut all: Vec<MusContext> = result
            .muses()
            .values()
            .flat_map(|set| set.iter().cloned())
            .filter(|mc| seen.insert(mc.mus.clone()))
            .collect();
        all.sort_by_key(|mc| mc.mus_len());
        all
    }

    pub fn solve_step_for_literal(&mut self, lit_def: Vec<i64>) -> (Problem, Vec<Lit>) {
        let muses = self.filtered_muses(Box::new(move |lit, planner| {
            let puzlit_list = planner.solver().lit_to_puzlit(lit);
            for puzlit in puzlit_list {
                let mut indices = puzlit.var().indices().clone();
                indices.push(puzlit.val());
                if indices == lit_def {
                    return true;
                }
            }
            false
        }));

        let min = muses.min();
        if min.is_none() {
            return self.build_step_problem(None, "There are no more values to deduce");
        }
        let min = min.unwrap();

        let mut vec = vec![];
        for v in muses.muses().values() {
            if let Some(m) = v.iter().next()
                && m.mus_len() == min
            {
                vec.push(m.clone());
            }
        }

        self.build_step_problem(Some(vec), "Made the following deductions")
    }

    /// Render the difficulty heatmap.  `hide_untouched_candidates`: when
    /// true, cells with no known literal yet are left blank ("?") instead
    /// of being filled with every value the planner could in principle
    /// deduce.  Used by walkthrough scripts in tutorial mode.
    pub fn difficulty_problem(&mut self, hide_untouched_candidates: bool) -> Problem {
        let base_muses = self.all_muses_with_larger();

        let base_difficulties: BTreeMap<Lit, usize> = base_muses
            .muses()
            .iter()
            .filter_map(|(k, v)| v.iter().map(MusContext::mus_len).min().map(|m| (*k, m)))
            .collect();

        let mut vvpmap: BTreeMap<VarValPair, usize> = BTreeMap::new();
        for (lit, &val) in &base_difficulties {
            for puzlit in self.psolve.puzzleparse().lit_to_vars(lit) {
                let vvp = puzlit.varval();
                vvpmap.insert(vvp, val);
            }
        }

        let varlits = self.psolve.get_provable_varlits().clone();
        let tosolve_varvals: BTreeSet<_> = varlits
            .iter()
            .flat_map(|x| self.psolve.lit_to_puzlit(x))
            .map(super::PuzLit::varval)
            .collect();

        let known_puzlits: BTreeSet<PuzLit> = self
            .get_all_known_lits()
            .iter()
            .flat_map(|x| self.psolve.lit_to_puzlit(x))
            .cloned()
            .collect();

        let mut problem = Problem::new_from_puzzle_and_difficulty(
            &self.psolve,
            &tosolve_varvals,
            &known_puzlits,
            &vvpmap,
            "The difficulty of the problem",
            hide_untouched_candidates,
        )
        .expect("Cannot make puzzle json");
        if let Some(verbose) = self.build_verbose_sections()
            && let Some(state) = problem.state.as_mut()
        {
            state.verbose = Some(verbose);
        }
        problem
    }

    /// Returns a reference to the puzzle being solved.
    ///
    /// # Returns
    ///
    /// A reference to the `PuzzleParse` instance representing the puzzle being solved.
    pub fn puzzle(&self) -> &PuzzleParse {
        self.psolve.puzzleparse()
    }

    pub fn puzzle_arc(&self) -> Arc<PuzzleParse> {
        self.psolve.puzzleparse_arc()
    }

    pub fn planner_config(&self) -> PlannerConfig {
        self.config
    }

    pub fn solver_config(&self) -> SolverConfig {
        self.psolve.solver_config()
    }

    pub fn fork(&self) -> anyhow::Result<PuzzlePlanner> {
        let solver = PuzzleSolver::fork_with_known_lits(
            self.psolve.puzzleparse_arc(),
            self.psolve.get_known_lits(),
            self.psolve.solver_config(),
        )?;
        Ok(PuzzlePlanner {
            psolve: solver,
            config: self.config,
            mus_cache: self.mus_cache.clone(),
            strategy_db: Arc::clone(&self.strategy_db),
            family_map: self.family_map.clone(),
        })
    }

    /// Returns a mutable reference to the solver. Warning, incorrect use of underlying
    /// solver can result in incorrect answers.
    pub fn solver(&mut self) -> &mut PuzzleSolver {
        &mut self.psolve
    }

    /// Mutable access to the planner's config — for callers that need to
    /// adjust `MusConfig` (`repeats`, `strategy`, etc.) between steps.
    /// The walkthrough script driver is the primary consumer.
    pub fn config_mut(&mut self) -> &mut PlannerConfig {
        &mut self.config
    }
}

#[cfg(test)]
mod tests {
    use std::{collections::BTreeSet, sync::Arc};

    use crate::problem::{
        PuzLit,
        planner::{PlannerConfig, PuzzlePlanner, UserMus},
        solver::{MusConfig, PuzzleSolver},
    };
    use itertools::Itertools;
    use test_log::test;

    /// Cloning a base planner and running `quick_solve` on the clone must
    /// yield exactly the same UserMus sequence (lits, constraints,
    /// fingerprint, name) as running `quick_solve` on a freshly-built
    /// planner.  The clone shares the trivially-deduced base state.
    #[test]
    fn test_clone_planner_quick_solve_matches_fresh() {
        let result = Arc::new(crate::problem::util::test_utils::build_puzzleparse(
            "./tst/little1.eprime",
            "./tst/little1.param",
        ));

        let base = PuzzlePlanner::new(PuzzleSolver::new(result.clone()).unwrap());
        let mut from_clone = base.clone();
        let from_clone_steps = from_clone.quick_solve();

        let mut from_fresh = PuzzlePlanner::new(PuzzleSolver::new(result).unwrap());
        let from_fresh_steps = from_fresh.quick_solve();

        // Same number of steps, same number of MUSes per step.
        assert_eq!(from_clone_steps.len(), from_fresh_steps.len());
        // Lits and constraints should match step-for-step.
        for (c, f) in from_clone_steps.iter().zip(from_fresh_steps.iter()) {
            let c_lits: BTreeSet<&PuzLit> = c.iter().flat_map(|m| m.lits.iter()).collect();
            let f_lits: BTreeSet<&PuzLit> = f.iter().flat_map(|m| m.lits.iter()).collect();
            assert_eq!(c_lits, f_lits, "deduced lits diverge across clone vs fresh");
        }
    }

    #[test]
    fn test_clone_planner_independent_branches() {
        // Two clones of the same base must remain independent: marking a
        // lit on one must not affect the other's view of provable lits.
        let result = Arc::new(crate::problem::util::test_utils::build_puzzleparse(
            "./tst/little1.eprime",
            "./tst/little1.param",
        ));
        let base = PuzzlePlanner::new(PuzzleSolver::new(result).unwrap());

        let mut branch_a = base.clone();
        let mut branch_b = base.clone();

        let varlits_before: BTreeSet<_> = branch_a.get_provable_varlits();
        assert!(!varlits_before.is_empty(), "expect non-trivial puzzle");
        let pick = *varlits_before.iter().next().unwrap();

        branch_a.mark_lit_as_deduced(&pick);

        assert!(branch_a.solver().get_known_lits().contains(&pick));
        assert!(!branch_b.solver().get_known_lits().contains(&pick));
    }

    #[test]
    fn test_plan_little_essence() {
        let result = crate::problem::util::test_utils::build_puzzleparse(
            "./tst/little1.eprime",
            "./tst/little1.param",
        );

        let result = Arc::new(result);

        let puz = PuzzleSolver::new(result).unwrap();

        let mut plan = PuzzlePlanner::new(puz);

        let sequence = plan.quick_solve();

        assert_eq!(sequence.iter().flatten().collect_vec().len(), 8);

        for um in sequence.iter().flatten() {
            assert!(!um.lits.is_empty());
            // It should be trivial to prove we only need one
            // constraint here, but MUS algorithms be tricky, if
            // this next line starts failing, it can be commented out.
            assert!(um.constraints.len() <= 1);
        }
    }

    #[test]
    fn test_solvability_little_essence() {
        let result = crate::problem::util::test_utils::build_puzzleparse(
            "./tst/little1.eprime",
            "./tst/little1.param",
        );

        let result = Arc::new(result);

        let puz = PuzzleSolver::new(result).unwrap();

        let mut plan = PuzzlePlanner::new(puz);

        assert_eq!(plan.check_solvability(), Some(0));
    }

    /// Resolve a `var[..]=val` / `var[..]!=val` string to its SAT literal via
    /// the direct encoding, mirroring how the FFI surfaces pin assumptions.
    fn lit_for(plan: &PuzzlePlanner, name: &str) -> rustsat::types::Lit {
        use crate::problem::format_puzlit;
        plan.puzzle()
            .direct
            .litmap
            .iter()
            .find(|(puzlit, _)| format_puzlit(puzlit) == name)
            .map(|(_, lit)| *lit)
            .unwrap_or_else(|| panic!("no lit for {name}"))
    }

    fn planner_for(eprime: &str, param: &str) -> PuzzlePlanner {
        let result = Arc::new(crate::problem::util::test_utils::build_puzzleparse(
            eprime, param,
        ));
        PuzzlePlanner::new(PuzzleSolver::new(result).unwrap())
    }

    #[test]
    fn test_is_uniquely_solvable_unique() {
        let mut plan = planner_for("./tst/little1.eprime", "./tst/little1.param");
        assert!(plan.is_uniquely_solvable());
        // It must not advance the planner's logical state.
        let known_before = plan.get_all_known_lits().len();
        assert!(plan.is_uniquely_solvable());
        assert_eq!(plan.get_all_known_lits().len(), known_before);
    }

    #[test]
    fn test_is_uniquely_solvable_multiple() {
        // A clueless 3-cell all-different puzzle has 6 solutions.
        let mut plan = planner_for("./tst/little-sudoku.eprime", "./tst/little-sudoku.param");
        assert!(!plan.is_uniquely_solvable());
    }

    #[test]
    fn test_is_uniquely_solvable_partial_assignment() {
        // No clues: multiple solutions.
        let mut plan = planner_for("./tst/little-sudoku.eprime", "./tst/little-sudoku.param");
        assert!(!plan.is_uniquely_solvable());

        // Pinning two of the three cells forces the third: unique.
        let mut unique = planner_for("./tst/little-sudoku.eprime", "./tst/little-sudoku.param");
        let g1 = lit_for(&unique, "grid[1]=1");
        let g2 = lit_for(&unique, "grid[2]=2");
        unique.mark_lit_as_fixed(&g1);
        unique.mark_lit_as_fixed(&g2);
        assert!(unique.is_uniquely_solvable());

        // Two cells pinned to the same value contradicts all-different: unsolvable.
        let mut bad = planner_for("./tst/little-sudoku.eprime", "./tst/little-sudoku.param");
        let b1 = lit_for(&bad, "grid[1]=1");
        let b2 = lit_for(&bad, "grid[2]=1");
        bad.mark_lit_as_fixed(&b1);
        bad.mark_lit_as_fixed(&b2);
        assert!(!bad.is_uniquely_solvable());
    }

    /// `all_muses_with_larger` must return a dict configured to retain larger MUSes.
    /// Whether the parallel search happens to *find* multi-size MUSes on a given
    /// instance is nondeterministic, so we check the wiring rather than a specific
    /// search outcome (the MusDict-level unit tests cover retention semantics).
    #[test]
    fn test_all_muses_with_larger_uses_keep_all() {
        let result = crate::problem::util::test_utils::build_puzzleparse(
            "./tst/binairo.eprime",
            "./tst/binairo-1.param",
        );
        let result = Arc::new(result);
        let puz = PuzzleSolver::new(result).unwrap();
        let mut plan = PuzzlePlanner::new(puz);

        let muses = plan.all_muses_with_larger();
        assert!(
            muses.keep_all(),
            "all_muses_with_larger must return a keep_all MusDict"
        );
    }

    /// find_one=true (the new default) must produce the same set of deduced literals as find_one=false.
    #[test]
    fn test_find_one_same_deductions_as_find_all() {
        let result = crate::problem::util::test_utils::build_puzzleparse(
            "./tst/minesweeper.eprime",
            "./tst/minesweeperWall.param",
        );
        let result = Arc::new(result);

        let run_solve = |find_one: bool| {
            let puz = PuzzleSolver::new(result.clone()).unwrap();
            let config = PlannerConfig {
                mus_config: MusConfig {
                    find_one,
                    ..MusConfig::default()
                },
                ..PlannerConfig::default()
            };
            let mut plan = PuzzlePlanner::new_with_config(puz, config);
            let seq = plan.quick_solve();
            // Collect the flat list of deduced literal sets across all steps.
            seq.into_iter().flatten().map(|um| um.lits).collect_vec()
        };

        let with_find_one = run_solve(true);
        let without_find_one = run_solve(false);

        // Both runs must deduce the same number of steps (deductions are deterministic).
        assert_eq!(
            with_find_one.len(),
            without_find_one.len(),
            "find_one changed the number of deduction steps"
        );
    }

    /// `quick_solve_greedy` must reach the same full set of deduced literals as
    /// `quick_solve`.  The maximum MUS size and the per-step breakdown differ
    /// (greedy applies non-minimal MUSes below the running maximum, and the
    /// underlying search is nondeterministic), but the solution closure — the
    /// union of all deduced `PuzLit`s — is path-independent, so it must match.
    fn assert_greedy_deduces_same_lits(model: &str, param: &str) {
        let result = Arc::new(crate::problem::util::test_utils::build_puzzleparse(
            model, param,
        ));

        let mut quick = PuzzlePlanner::new(PuzzleSolver::new(result.clone()).unwrap());
        let quick_seq = quick.quick_solve();

        let mut greedy = PuzzlePlanner::new(PuzzleSolver::new(result).unwrap());
        let greedy_seq = greedy.quick_solve_greedy();

        // Greedy must fully solve the puzzle, with a well-formed sequence.
        assert_valid_sequence(&greedy_seq);
        assert!(
            greedy.psolve.get_provable_varlits().is_empty(),
            "quick_solve_greedy left literals unsolved"
        );

        let quick_lits: BTreeSet<PuzLit> = quick_seq
            .into_iter()
            .flatten()
            .flat_map(|um| um.lits)
            .collect();
        let greedy_lits: BTreeSet<PuzLit> = greedy_seq
            .into_iter()
            .flatten()
            .flat_map(|um| um.lits)
            .collect();
        assert_eq!(
            quick_lits, greedy_lits,
            "quick_solve_greedy deduced a different set of literals than quick_solve"
        );
    }

    #[test]
    fn test_greedy_solves_little_essence() {
        assert_greedy_deduces_same_lits("./tst/little1.eprime", "./tst/little1.param");
    }

    #[test]
    fn test_greedy_solves_binairo_essence() {
        assert_greedy_deduces_same_lits("./tst/binairo.eprime", "./tst/binairo-1.param");
    }

    #[test]
    fn test_greedy_solves_minesweeper_wall_essence() {
        assert_greedy_deduces_same_lits("./tst/minesweeper.eprime", "./tst/minesweeperWall.param");
    }

    /// Verify that a solve sequence is well-formed:
    /// - non-empty (the puzzle was actually solved)
    /// - every sub-step deduces at least one literal
    /// - no PuzLit appears in more than one sub-step
    fn assert_valid_sequence(sequence: &[Vec<UserMus>]) {
        assert!(!sequence.is_empty(), "solve produced no steps");

        let mut seen = BTreeSet::<PuzLit>::new();
        for step in sequence {
            for substep in step {
                assert!(!substep.lits.is_empty(), "sub-step deduced no literals");
                assert!(
                    !substep.constraints.is_empty(),
                    "sub-step has no constraints"
                );
                for lit in &substep.lits {
                    assert!(
                        seen.insert(lit.clone()),
                        "PuzLit {lit:?} appears in more than one sub-step"
                    );
                }
            }
        }
    }

    #[test]
    fn test_plan_binairo_essence() {
        let result = crate::problem::util::test_utils::build_puzzleparse(
            "./tst/binairo.eprime",
            "./tst/binairo-1.param",
        );

        let result = Arc::new(result);

        let puz = PuzzleSolver::new(result).unwrap();

        let mut plan = PuzzlePlanner::new(puz);

        let sequence = plan.quick_solve();

        assert_valid_sequence(&sequence);
    }

    #[test]
    fn test_plan_minesweeper_essence() {
        let result = crate::problem::util::test_utils::build_puzzleparse(
            "./tst/minesweeper.eprime",
            "./tst/minesweeperPrinted.param",
        );

        let result = Arc::new(result);

        let puz = PuzzleSolver::new(result).unwrap();

        let mut plan = PuzzlePlanner::new(puz);

        let sequence = plan.quick_solve();

        assert_valid_sequence(&sequence);
    }

    #[test]
    fn test_varlits_minesweeper_essence() {
        let result = crate::problem::util::test_utils::build_puzzleparse(
            "./tst/minesweeper.eprime",
            "./tst/minesweeperPrinted.param",
        );

        let result = Arc::new(result);

        let puz = PuzzleSolver::new(result).unwrap();

        let mut plan = PuzzlePlanner::new(puz);

        let first_step = plan.get_provable_varlits();

        let all_steps = plan.get_provable_varlits_including_reveals();

        let first_step: BTreeSet<_> = first_step
            .into_iter()
            .map(|x| plan.psolve.lit_to_puzlit(&x).clone())
            .collect();

        let all_steps: BTreeSet<_> = all_steps
            .into_iter()
            .map(|x| plan.psolve.lit_to_puzlit(&x).clone())
            .collect();

        insta::assert_debug_snapshot!(first_step);
        insta::assert_debug_snapshot!(all_steps);
    }

    #[test]
    fn test_plan_minesweeper_wall_essence() {
        let result = crate::problem::util::test_utils::build_puzzleparse(
            "./tst/minesweeper.eprime",
            "./tst/minesweeperWall.param",
        );

        let result = Arc::new(result);

        let puz = PuzzleSolver::new(result).unwrap();

        let mut plan = PuzzlePlanner::new(puz);

        let sequence = plan.quick_solve();

        // Warning: This number may change as MUS detection / merging improves.
        // Changes should be sanity checked by printing out the sequence.
        assert_eq!(sequence.iter().flatten().collect_vec().len(), 8);

        for um in sequence.iter().flatten() {
            assert!(!um.lits.is_empty());
            // If this next line starts failing, it can be commented out.
            assert!(um.constraints.len() <= 2);
        }
    }

    #[test]
    fn test_solvability_minesweeper_wall_essence() {
        let result = crate::problem::util::test_utils::build_puzzleparse(
            "./tst/minesweeper.eprime",
            "./tst/minesweeperWall.param",
        );

        let result = Arc::new(result);

        let puz = PuzzleSolver::new(result).unwrap();

        let mut plan = PuzzlePlanner::new(puz);

        assert_eq!(plan.check_solvability(), Some(20));
    }

    // This test doesn't really do any deep tests,
    // just do a full end-to-end run
    #[test]
    fn test_plan_binairo_essence_html() {
        let result = crate::problem::util::test_utils::build_puzzleparse(
            "./tst/binairo.eprime",
            "./tst/binairo-1.param",
        );

        let result = Arc::new(result);

        let puz = PuzzleSolver::new(result).unwrap();

        let mut plan = PuzzlePlanner::new(puz);

        let _ = plan.quick_solve_html();
    }
}