qualia_cli/
solve.rs

1use qualia_core_db::solvers::linear_algebra::{
2    ConstTensorContractor, FixedLanczosEigensolver, Matrix4x4, StaticLuDecomposition, Tensor3x3x3,
3    Vector4,
4};
5use qualia_core_db::solvers::optimization::{
6    BoundedNewtonRaphson, CurveFitFunction, LevenbergMarquardtStack, NelderMeadSimplex,
7    ObjectiveFunction, RootFunction,
8};
9use qualia_core_db::solvers::quantum_optimizers::{
10    QAOAAngleOptimizer, QAOAAngles, QuantumCostFunction, SpsaCostFunction, SpsaOptimizer,
11};
12use qualia_core_db::solvers::symbolic_logic::{
13    BoundedSatSolver, Clause, DefeasibleRule, Fact, ForwardChainingDefeasible, Literal, RuleType,
14};
15use qualia_core_db::solvers::SolverConfig;
16
17// ── Helpers ───────────────────────────────────────────────────────────────────
18
19fn parse_f64s(s: &str) -> Vec<f64> {
20    s.split(',')
21        .filter_map(|tok| tok.trim().parse::<f64>().ok())
22        .collect()
23}
24
25fn build_matrix4x4(v: &[f64]) -> Matrix4x4 {
26    let mut m = Matrix4x4::zero();
27    for row in 0..4 {
28        for col in 0..4 {
29            m.data[row][col] = v[row * 4 + col];
30        }
31    }
32    m
33}
34
35fn parse_matrix4x4(s: &str) -> Option<Matrix4x4> {
36    let v = parse_f64s(s);
37    if v.len() < 16 {
38        eprintln!(
39            "Need 16 comma-separated values for a 4×4 matrix, got {}.",
40            v.len()
41        );
42        return None;
43    }
44    Some(build_matrix4x4(&v))
45}
46
47fn parse_vector4(s: &str) -> Option<Vector4> {
48    let v = parse_f64s(s);
49    if v.len() < 4 {
50        eprintln!(
51            "Need 4 comma-separated values for a Vector4, got {}.",
52            v.len()
53        );
54        return None;
55    }
56    Some(Vector4::from_array([v[0], v[1], v[2], v[3]]))
57}
58
59fn build_tensor3x3x3(v: &[f64]) -> Tensor3x3x3 {
60    let mut t = Tensor3x3x3::zero();
61    for i in 0..3 {
62        for j in 0..3 {
63            for k in 0..3 {
64                t.data[i][j][k] = v[i * 9 + j * 3 + k];
65            }
66        }
67    }
68    t
69}
70
71fn parse_tensor3x3x3(s: &str) -> Option<Tensor3x3x3> {
72    let v = parse_f64s(s);
73    if v.len() < 27 {
74        eprintln!(
75            "Need 27 comma-separated values for a 3×3×3 tensor, got {}.",
76            v.len()
77        );
78        return None;
79    }
80    Some(build_tensor3x3x3(&v))
81}
82
83fn parse_params4(s: &str) -> Option<[f64; 4]> {
84    let v = parse_f64s(s);
85    if v.len() < 4 {
86        eprintln!("Need 4 comma-separated values, got {}.", v.len());
87        return None;
88    }
89    Some([v[0], v[1], v[2], v[3]])
90}
91
92fn default_config(max_iters: u32, tol: f64) -> SolverConfig {
93    SolverConfig {
94        max_iterations: max_iters,
95        tolerance: tol,
96        step_size: 0.01,
97        verbose: false,
98    }
99}
100
101// ── Linear algebra runners ────────────────────────────────────────────────────
102
103pub fn run_matrix_multiply(a_str: &str, b_str: &str) {
104    let (Some(a), Some(b)) = (parse_matrix4x4(a_str), parse_matrix4x4(b_str)) else {
105        return;
106    };
107    let result = a.multiply_matrix(&b);
108    println!("Matrix A × B:");
109    print_matrix4x4(&result);
110}
111
112pub fn run_determinant(m_str: &str) {
113    let Some(m) = parse_matrix4x4(m_str) else {
114        return;
115    };
116    let det = m.determinant();
117    println!("Determinant: {det:.10e}");
118}
119
120pub fn run_solve_system(m_str: &str, v_str: &str) {
121    let (Some(a), Some(b)) = (parse_matrix4x4(m_str), parse_vector4(v_str)) else {
122        return;
123    };
124    let mut lu = StaticLuDecomposition::new(default_config(100, 1e-12));
125    match lu.solve(&a, &b) {
126        Ok(x) => {
127            println!("Solution x for Ax = b:");
128            println!(
129                "  [{:.6}, {:.6}, {:.6}, {:.6}]",
130                x.data[0], x.data[1], x.data[2], x.data[3]
131            );
132        }
133        Err(e) => eprintln!("Solve failed: {e:?}"),
134    }
135}
136
137pub fn run_eigenvalues(m_str: &str, count: usize) {
138    let Some(m) = parse_matrix4x4(m_str) else {
139        return;
140    };
141    let mut solver = FixedLanczosEigensolver::new(default_config(100, 1e-8));
142    match solver.find_lowest_eigenvalues(&m, count) {
143        Ok(eigs) => {
144            let n = count.min(4);
145            println!("Lowest {n} eigenvalue(s) (Lanczos):");
146            for i in 0..n {
147                println!("  λ[{i}] = {:.10e}", eigs[i]);
148            }
149        }
150        Err(e) => eprintln!("Eigenvalue computation failed: {e:?}"),
151    }
152}
153
154pub fn run_tensor_contract(t_str: &str) {
155    let Some(ta) = parse_tensor3x3x3(t_str) else {
156        return;
157    };
158    let tb = Tensor3x3x3::zero();
159    let indices: [(usize, usize); 3] = [(0, 0), (1, 1), (2, 2)];
160    let mut contractor = ConstTensorContractor::new(default_config(1, 1e-10));
161    match contractor.contract(&ta, &tb, &indices) {
162        Ok(result) => {
163            // Sum all elements as a scalar trace equivalent
164            let scalar: f64 = (0..3)
165                .flat_map(|i| (0..3).flat_map(move |j| (0..3).map(move |k| (i, j, k))))
166                .map(|(i, j, k)| result.data[i][j][k])
167                .sum();
168            println!("Tensor contraction A⊗0 trace-sum: {scalar:.10e}");
169            println!("(pass two tensors via --tensor-a and --tensor-b for a full contraction)");
170        }
171        Err(e) => eprintln!("Tensor contraction failed: {e:?}"),
172    }
173}
174
175fn print_matrix4x4(m: &Matrix4x4) {
176    for row in 0..4 {
177        println!(
178            "  [{:12.6}, {:12.6}, {:12.6}, {:12.6}]",
179            m.data[row][0], m.data[row][1], m.data[row][2], m.data[row][3]
180        );
181    }
182}
183
184// ── ObjectiveFunction adapter for closures ────────────────────────────────────
185
186struct ClosureFn<F: Fn(&[f64; 4]) -> f64>(F);
187impl<F: Fn(&[f64; 4]) -> f64> ObjectiveFunction for ClosureFn<F> {
188    fn evaluate(&self, params: &[f64; 4]) -> f64 {
189        (self.0)(params)
190    }
191}
192
193struct RootClosureFn<F: Fn(f64) -> f64, D: Fn(f64) -> f64>(F, D);
194impl<F: Fn(f64) -> f64, D: Fn(f64) -> f64> RootFunction for RootClosureFn<F, D> {
195    fn evaluate(&self, x: f64) -> f64 {
196        (self.0)(x)
197    }
198    fn derivative(&self, x: f64) -> f64 {
199        (self.1)(x)
200    }
201}
202
203struct CurveFn;
204impl CurveFitFunction for CurveFn {
205    // cubic model: p[0]*x³ + p[1]*x² + p[2]*x + p[3]
206    fn evaluate(&self, x: f64, p: &[f64; 4]) -> f64 {
207        p[0] * x.powi(3) + p[1] * x.powi(2) + p[2] * x + p[3]
208    }
209    fn jacobian(&self, x: f64, _p: &[f64; 4]) -> [f64; 4] {
210        [x.powi(3), x.powi(2), x, 1.0]
211    }
212}
213
214// ── Optimization runners ──────────────────────────────────────────────────────
215
216pub fn run_simplex(initial_str: &str, iterations: u32) {
217    let Some(x0) = parse_params4(initial_str) else {
218        return;
219    };
220    let cfg = default_config(iterations, 1e-8);
221    let mut solver = NelderMeadSimplex::new(x0, cfg);
222    // Rosenbrock 4D: f(x,y,z,w) = (1-x)² + 100(y-x²)² + (1-z)² + 100(w-z²)²
223    let f = ClosureFn(|p: &[f64; 4]| {
224        let a = (1.0 - p[0]).powi(2) + 100.0 * (p[1] - p[0].powi(2)).powi(2);
225        let b = (1.0 - p[2]).powi(2) + 100.0 * (p[3] - p[2].powi(2)).powi(2);
226        a + b
227    });
228    match solver.optimize(&f) {
229        Ok(state) => {
230            let bp = solver.best_point;
231            println!("Nelder-Mead simplex (Rosenbrock 4D, {iterations} iters):");
232            println!(
233                "  x = [{:.6}, {:.6}, {:.6}, {:.6}]",
234                bp[0], bp[1], bp[2], bp[3]
235            );
236            println!("  f(x) = {:.10e}", state.objective_value);
237            println!("  Converged: {}", state.converged);
238        }
239        Err(e) => eprintln!("Simplex failed: {e:?}"),
240    }
241}
242
243pub fn run_root(initial: f64, lower: f64, upper: f64, tolerance: f64) {
244    // f(x) = x³ − x − 1  (plastic constant, root ≈ 1.32472)
245    let cfg = SolverConfig {
246        max_iterations: 200,
247        tolerance,
248        step_size: 0.01,
249        verbose: false,
250    };
251    let mut solver = BoundedNewtonRaphson::new(initial, lower, upper, cfg);
252    let f = RootClosureFn(|x: f64| x * x * x - x - 1.0, |x: f64| 3.0 * x * x - 1.0);
253    match solver.find_root(&f) {
254        Ok(state) => {
255            let root = solver.get_root();
256            println!("Newton-Raphson root of f(x) = x³ − x − 1:");
257            println!("  root ≈ {root:.10e}");
258            println!("  f(root) = {:.4e}", x_cubed_minus_x_minus_one(root));
259            println!(
260                "  Converged: {} ({} iters)",
261                state.converged, state.iteration
262            );
263        }
264        Err(e) => eprintln!("Root finder failed: {e:?}"),
265    }
266}
267
268fn x_cubed_minus_x_minus_one(x: f64) -> f64 {
269    x * x * x - x - 1.0
270}
271
272pub fn run_curve_fit(params_str: &str, x_str: &str, y_str: &str) {
273    let Some(p0) = parse_params4(params_str) else {
274        return;
275    };
276    let xs = parse_f64s(x_str);
277    let ys = parse_f64s(y_str);
278    if xs.is_empty() || ys.is_empty() || xs.len() != ys.len() {
279        eprintln!("x-data and y-data must be equal-length, non-empty comma-separated lists.");
280        return;
281    }
282
283    // Pad/truncate to exactly 10 points (LM stack uses fixed 10-point buffer)
284    let mut xd = [0.0f64; 10];
285    let mut yd = [0.0f64; 10];
286    let n = xs.len().min(10);
287    xd[..n].copy_from_slice(&xs[..n]);
288    yd[..n].copy_from_slice(&ys[..n]);
289
290    let cfg = default_config(200, 1e-8);
291    let mut lm = LevenbergMarquardtStack::new(p0, cfg);
292    let model = CurveFn;
293    match lm.fit_curve(&model, &xd, &yd) {
294        Ok(state) => {
295            let p = lm.parameters;
296            println!("Levenberg-Marquardt curve fit (cubic: p0·x³+p1·x²+p2·x+p3):");
297            println!(
298                "  params = [{:.6}, {:.6}, {:.6}, {:.6}]",
299                p[0], p[1], p[2], p[3]
300            );
301            println!("  χ²     = {:.6e}", state.chi_squared);
302            println!(
303                "  Converged: {} ({} iters)",
304                state.converged, state.iteration
305            );
306        }
307        Err(e) => eprintln!("Curve fit failed: {e:?}"),
308    }
309}
310
311// ── ODE runners ───────────────────────────────────────────────────────────────
312
313pub fn run_ode_rk4(lambda: f64, t_start: f64, t_end: f64, y0: f64, step_size: f64) {
314    use qualia_core_db::modalities::calculus::ode_solver::{ExponentialDecay, Rk4Solver};
315    let system = ExponentialDecay::new(lambda);
316    let mut solver = Rk4Solver::new(system, step_size);
317    let result = solver.solve(t_start, t_end, y0);
318    println!("RK4 ODE (exponential decay λ={lambda}):");
319    println!("  t ∈ [{t_start}, {t_end}],  y(0)={y0},  h={step_size}");
320    println!("  y(t_end) ≈ {result:.10e}");
321    println!(
322        "  exact    = {:.10e}",
323        y0 * (-lambda * (t_end - t_start)).exp()
324    );
325}
326
327pub fn run_ode_harmonic(omega: f64, t_start: f64, t_end: f64, y0: f64, step_size: f64) {
328    use qualia_core_db::modalities::calculus::ode_solver::{HarmonicOscillator, Rk4Solver};
329    let system = HarmonicOscillator::new(omega);
330    let mut solver = Rk4Solver::new(system, step_size);
331    let result = solver.solve(t_start, t_end, y0);
332    println!("RK4 ODE (harmonic oscillator ω={omega}):");
333    println!("  t ∈ [{t_start}, {t_end}],  y(0)={y0},  h={step_size}");
334    println!("  y(t_end) ≈ {result:.10e}");
335}
336
337pub fn run_ode_bvp(t_start: f64, t_end: f64, y_left: f64, y_right: f64, threshold: f64) {
338    use qualia_core_db::modalities::calculus::ode_solver::{BvpSystem, ShootingMethod};
339
340    struct SimpleBvp {
341        lambda: f64,
342    }
343    impl BvpSystem for SimpleBvp {
344        fn derivative(&self, _t: f64, y: f64) -> f64 {
345            -self.lambda * y
346        }
347        fn boundary_left(&self, _a: f64) -> f64 {
348            0.0
349        }
350        fn boundary_right(&self, _b: f64) -> f64 {
351            0.0
352        }
353    }
354
355    let system = SimpleBvp { lambda: 1.0 };
356    let mut solver = ShootingMethod::new(system, threshold).with_max_iterations(500);
357    match solver.solve(t_start, t_end, y_left, y_right) {
358        Ok((ic, residual)) => {
359            println!("BVP shooting method (f'=-y):");
360            println!("  t ∈ [{t_start}, {t_end}]");
361            println!("  Converged IC : {ic:.8e}");
362            println!("  Residual     : {residual:.4e}");
363        }
364        Err(e) => eprintln!("BVP failed to converge: {e}"),
365    }
366}
367
368pub fn run_ode_quantum_spectrum(planck_mass: f64, coupling: f64, max_n: u64, frequency: f64) {
369    use qualia_core_db::modalities::calculus::ode_solver::QuantizationMapper;
370    let qh = QuantizationMapper::new(planck_mass, coupling);
371    let spectrum = qh.compute_mass_spectrum(max_n, frequency);
372    println!("Quantum harmonic mass spectrum (M_p={planck_mass:.3e}, g={coupling:.3e}, f={frequency:.3e}):");
373    for (n, mass) in spectrum.iter().take(10) {
374        println!("  n={n:3}  mass = {mass:.10e}");
375    }
376    if spectrum.len() > 10 {
377        println!("  … ({} total levels)", spectrum.len());
378    }
379}
380
381// ── Quantum optimizer runners ─────────────────────────────────────────────────
382
383struct DemoQaoa(u8);
384
385impl QuantumCostFunction for DemoQaoa {
386    fn evaluate_quantum(&self, angles: &QAOAAngles) -> qualia_core_db::solvers::SolverResult<f64> {
387        // Demo MaxCut-like cost: minimize sum of angle squares
388        let cost: f64 = angles.beta[..self.0 as usize]
389            .iter()
390            .map(|x| x * x)
391            .sum::<f64>()
392            + angles.gamma[..self.0 as usize]
393                .iter()
394                .map(|x| x * x)
395                .sum::<f64>();
396        Ok(cost)
397    }
398    fn evaluate_perturbed(
399        &self,
400        angles: &QAOAAngles,
401        perturbation: &QAOAAngles,
402    ) -> qualia_core_db::solvers::SolverResult<(f64, f64)> {
403        let mut plus = *angles;
404        let mut minus = *angles;
405        for i in 0..self.0 as usize {
406            plus.beta[i] += perturbation.beta[i];
407            minus.beta[i] -= perturbation.beta[i];
408        }
409        Ok((
410            self.evaluate_quantum(&plus)?,
411            self.evaluate_quantum(&minus)?,
412        ))
413    }
414    fn problem_size(&self) -> u8 {
415        self.0
416    }
417}
418
419pub fn run_quantum_qaoa(depth: u8, beta_str: &str, gamma_str: &str) {
420    let cfg = default_config(100, 1e-6);
421    let mut opt = QAOAAngleOptimizer::new(depth, cfg);
422    let betas = parse_f64s(beta_str);
423    let gammas = parse_f64s(gamma_str);
424    let mut init = QAOAAngles {
425        beta: [0.0; 10],
426        gamma: [0.0; 10],
427    };
428    for (i, &b) in betas.iter().take(10).enumerate() {
429        init.beta[i] = b;
430    }
431    for (i, &g) in gammas.iter().take(10).enumerate() {
432        init.gamma[i] = g;
433    }
434    let cost_fn = DemoQaoa(depth.min(10));
435    match opt.optimize(&cost_fn, init) {
436        Ok(state) => {
437            let final_a = opt.get_angles();
438            println!("QAOA angle optimizer (depth={depth}, demo MaxCut cost):");
439            println!("  Iterations   : {}", state.iteration);
440            println!("  Quantum calls: {}", state.quantum_calls);
441            println!("  Final cost   : {:.8e}", state.cost_value);
442            println!("  Converged    : {}", state.converged);
443            println!("  β[0..d] = {:?}", &final_a.beta[..depth as usize]);
444            println!("  γ[0..d] = {:?}", &final_a.gamma[..depth as usize]);
445        }
446        Err(e) => eprintln!("QAOA optimization failed: {e:?}"),
447    }
448}
449
450struct DemoSpsa(#[allow(dead_code)] u8);
451
452impl SpsaCostFunction for DemoSpsa {
453    fn evaluate(&self, params: &[f64; 20], n: u8) -> qualia_core_db::solvers::SolverResult<f64> {
454        Ok(params[..n as usize].iter().map(|x| x * x).sum())
455    }
456    fn valid_parameters(&self, _p: &[f64; 20], _n: u8) -> bool {
457        true
458    }
459}
460
461pub fn run_quantum_spsa(num_params: u8, initial_str: &str) {
462    let vals = parse_f64s(initial_str);
463    let mut params = [0.0f64; 20];
464    let n = (num_params as usize).min(20).min(vals.len());
465    params[..n].copy_from_slice(&vals[..n]);
466    let cfg = default_config(200, 1e-6);
467    let mut opt = SpsaOptimizer::new(num_params, cfg);
468    let cost_fn = DemoSpsa(num_params);
469    match opt.optimize(&cost_fn, &params) {
470        Ok(state) => {
471            let p = opt.get_parameters();
472            println!("SPSA optimizer (demo quadratic cost, {num_params} params):");
473            println!("  Iterations: {}", state.iteration);
474            println!("  Final cost: {:.8e}", state.cost_value);
475            println!("  Converged : {}", state.converged);
476            println!("  Params    : {:?}", &p[..n]);
477        }
478        Err(e) => eprintln!("SPSA optimization failed: {e:?}"),
479    }
480}
481
482// ── Symbolic logic runners ────────────────────────────────────────────────────
483
484fn parse_u8s(s: &str) -> Vec<u8> {
485    s.split(',')
486        .filter_map(|t| t.trim().parse::<u8>().ok())
487        .collect()
488}
489
490pub fn run_symbolic_defeasible(facts_str: &str, rules_str: &str) {
491    let cfg = default_config(500, 1e-6);
492    let mut solver = ForwardChainingDefeasible::new(cfg);
493
494    // Parse facts: comma-separated variable indices (1-based)
495    for (idx, var) in parse_u8s(facts_str).into_iter().enumerate() {
496        let fact = Fact {
497            id: (idx as u32) + 1,
498            literal: Literal {
499                variable: var,
500                negated: false,
501            },
502            supporting_rules: [0; 3],
503            defeated: false,
504            confidence: 1.0,
505        };
506        if let Err(e) = solver.add_fact(fact) {
507            eprintln!("  Fact capacity exceeded: {e:?}");
508            break;
509        }
510    }
511
512    // Parse rules: "ant1,ant2:cons" pairs separated by ';'
513    for (rid, rule_str) in rules_str.split(';').enumerate() {
514        let parts: Vec<&str> = rule_str.splitn(2, ':').collect();
515        if parts.len() != 2 {
516            continue;
517        }
518        let ants: Vec<u8> = parse_u8s(parts[0]);
519        let cons = parts[1].trim().parse::<u8>().unwrap_or(0);
520        let mut antecedents = [Literal {
521            variable: 0,
522            negated: false,
523        }; 5];
524        for (i, &a) in ants.iter().take(5).enumerate() {
525            antecedents[i] = Literal {
526                variable: a,
527                negated: false,
528            };
529        }
530        let rule = DefeasibleRule {
531            id: (rid as u32) + 1,
532            rule_type: RuleType::Defeasible,
533            antecedents,
534            consequent: Literal {
535                variable: cons,
536                negated: false,
537            },
538            priority: 500,
539            active: true,
540            fire_count: 0,
541        };
542        if let Err(e) = solver.add_rule(rule) {
543            eprintln!("  Rule capacity exceeded: {e:?}");
544            break;
545        }
546    }
547
548    match solver.infer() {
549        Ok(state) => {
550            println!("Defeasible logic inference:");
551            println!("  Facts at start : {}", parse_u8s(facts_str).len());
552            println!("  Facts after    : {}", state.num_facts);
553            println!("  Rules fired    : {}", state.rules_fired);
554            println!("  Iterations     : {}", state.iteration);
555            println!("  Converged      : {}", state.converged);
556            let active: Vec<u8> = solver
557                .get_facts()
558                .iter()
559                .filter(|f| f.id != 0 && !f.defeated)
560                .map(|f| f.literal.variable)
561                .collect();
562            println!("  Active literals: {active:?}");
563        }
564        Err(e) => eprintln!("Defeasible inference failed: {e:?}"),
565    }
566}
567
568pub fn run_symbolic_sat(clauses_str: &str) {
569    let cfg = default_config(1000, 1e-8);
570    let mut solver = BoundedSatSolver::new(cfg);
571
572    // Parse clauses: "1,-2,3|4,-5" — pipe-separated clauses, comma-separated literals
573    for (cid, clause_str) in clauses_str.split('|').enumerate() {
574        let lits: Vec<Literal> = clause_str
575            .split(',')
576            .filter_map(|tok| {
577                let tok = tok.trim();
578                let (neg, var_str) = if tok.starts_with('-') {
579                    (true, &tok[1..])
580                } else {
581                    (false, tok)
582                };
583                var_str.parse::<u8>().ok().map(|v| Literal {
584                    variable: v,
585                    negated: neg,
586                })
587            })
588            .collect();
589        let mut literals = [Literal {
590            variable: 0,
591            negated: false,
592        }; 5];
593        let n = lits.len().min(5) as u8;
594        for (i, l) in lits.iter().take(5).enumerate() {
595            literals[i] = *l;
596        }
597        let clause = Clause {
598            id: (cid as u32) + 1,
599            literals,
600            num_literals: n,
601            learned: false,
602            activity: 1.0,
603        };
604        if let Err(e) = solver.add_clause(clause) {
605            eprintln!("  Clause capacity exceeded: {e:?}");
606            break;
607        }
608    }
609
610    match solver.solve() {
611        Ok(state) => {
612            use qualia_core_db::solvers::symbolic_logic::AssignmentValue;
613            println!("SAT solver (DPLL):");
614            println!("  Iterations  : {}", state.iteration);
615            println!("  Decisions   : {}", state.num_decisions);
616            println!(
617                "  Satisfiable : {}",
618                match state.satisfiable {
619                    Some(true) => "yes",
620                    Some(false) => "no",
621                    None => "unknown",
622                }
623            );
624            let assignments = solver.get_assignments();
625            let assigned: Vec<_> = assignments
626                .iter()
627                .filter(|a| a.level != 0 || a.antecedent.is_some())
628                .map(|a| {
629                    let v = match a.value {
630                        AssignmentValue::True => "T",
631                        AssignmentValue::False => "F",
632                        AssignmentValue::Unassigned => "?",
633                    };
634                    format!("x[{}]={}", a.level, v)
635                })
636                .take(10)
637                .collect();
638            if !assigned.is_empty() {
639                println!("  Assignments : {}", assigned.join(", "));
640            }
641        }
642        Err(e) => eprintln!("SAT solve failed: {e:?}"),
643    }
644}
qualia_cli/solve.rs

qualia_cli/
solve.rs
