xlog_solve/
service.rs

1//! Bounded solver-service interface for v0.9 semantics.
2
3use std::cell::RefCell;
4
5use xlog_core::{Result, XlogError};
6
7use crate::{Clause, Literal, Objective, SolveInstance};
8
9/// Status returned by the solver-service interface.
10#[derive(Debug, Clone, PartialEq, Eq)]
11pub enum SolverServiceStatus {
12    /// The hard constraints are satisfiable.
13    Sat,
14    /// The hard constraints are unsatisfiable.
15    Unsat,
16    /// Search was not attempted or no authoritative backend is available.
17    Unknown,
18    /// Search was bounded before any assignment could be inspected.
19    Timeout,
20    /// MaxSAT optimum as an integer score.
21    Optimal(u64),
22}
23
24/// Search budget for bounded service solves.
25#[derive(Debug, Clone, Copy, PartialEq, Eq)]
26pub enum SolverServiceBudget {
27    /// Do not search; return `Unknown`.
28    NoSearch,
29    /// Inspect at most this many assignments.
30    AssignmentLimit(u64),
31    /// Exhaustively inspect the assignment space.
32    Exhaustive,
33}
34
35/// Trace counters for service-level behavior.
36#[derive(Debug, Clone, Default, PartialEq, Eq)]
37pub struct SolverServiceTrace {
38    /// Number of learned clauses received from another service.
39    pub learned_clause_transfers: usize,
40    /// CPU assignment candidates inspected by the semantic-oracle facade.
41    pub cpu_assignment_enumerations: u64,
42    /// CPU MaxSAT candidates inspected by the semantic-oracle facade.
43    pub cpu_maxsat_enumerations: u64,
44}
45
46impl SolverServiceTrace {
47    /// Reject attempts to use the CPU semantic-oracle facade as production metric evidence.
48    pub fn require_production_metric_eligibility(&self) -> Result<()> {
49        Err(XlogError::UnsupportedEpistemicConstruct {
50            construct: "CPU semantic-oracle solver service".to_string(),
51            context: format!(
52                "SolverService is fixture-only and cannot satisfy production solver metrics; \
53                 cpu_assignment_enumerations={} cpu_maxsat_enumerations={} \
54                 learned_clause_transfers={}",
55                self.cpu_assignment_enumerations,
56                self.cpu_maxsat_enumerations,
57                self.learned_clause_transfers
58            ),
59        })
60    }
61}
62
63/// Result returned by the solver service.
64#[derive(Debug, Clone, PartialEq, Eq)]
65pub struct SolverServiceResult {
66    /// Solver-service status.
67    pub status: SolverServiceStatus,
68    /// Assignment when available.
69    pub assignment: Option<Vec<bool>>,
70}
71
72/// Learned-clause transfer result.
73#[derive(Debug, Clone, Copy, PartialEq, Eq)]
74pub struct LearnedClauseTransfer {
75    /// Number of clauses transferred.
76    pub clauses: usize,
77}
78
79/// GPU portfolio status for the semantic-oracle facade.
80#[derive(Debug, Clone, Copy, PartialEq, Eq)]
81pub enum SolverPortfolioStatus {
82    /// GPU portfolio solving is unavailable with rationale.
83    Deferred {
84        /// Deferral rationale.
85        reason: &'static str,
86    },
87}
88
89/// Incremental SAT/MaxSAT service facade.
90pub struct SolverService {
91    instance: SolveInstance,
92    assumptions: Vec<Option<Literal>>,
93    learned_clauses: RefCell<Vec<ScopedLearnedClause>>,
94    trace: RefCell<SolverServiceTrace>,
95}
96
97#[derive(Debug, Clone, PartialEq, Eq)]
98struct ScopedLearnedClause {
99    clause: Clause,
100    assumption_scope: Vec<Literal>,
101}
102
103impl SolverService {
104    /// Create a service for an instance.
105    pub fn new(instance: SolveInstance) -> Self {
106        Self {
107            instance,
108            assumptions: Vec::new(),
109            learned_clauses: RefCell::new(Vec::new()),
110            trace: RefCell::new(SolverServiceTrace::default()),
111        }
112    }
113
114    /// Add an assumption and return its token.
115    pub fn assume(&mut self, literal: Literal) -> usize {
116        let token = self.assumptions.len();
117        self.assumptions.push(Some(literal));
118        token
119    }
120
121    /// Retract an assumption by token.
122    pub fn retract_assumption(&mut self, token: usize) -> bool {
123        let Some(slot) = self.assumptions.get_mut(token) else {
124            return false;
125        };
126        let existed = slot.is_some();
127        *slot = None;
128        existed
129    }
130
131    /// Solve with exhaustive search.
132    pub fn solve(&self) -> SolverServiceResult {
133        self.solve_with_budget(SolverServiceBudget::Exhaustive)
134    }
135
136    /// Solve with a bounded search budget.
137    pub fn solve_with_budget(&self, budget: SolverServiceBudget) -> SolverServiceResult {
138        match budget {
139            SolverServiceBudget::NoSearch => SolverServiceResult {
140                status: SolverServiceStatus::Unknown,
141                assignment: None,
142            },
143            SolverServiceBudget::AssignmentLimit(0) => SolverServiceResult {
144                status: SolverServiceStatus::Timeout,
145                assignment: None,
146            },
147            SolverServiceBudget::AssignmentLimit(limit) => self.solve_assignments(Some(limit)),
148            SolverServiceBudget::Exhaustive => self.solve_assignments(None),
149        }
150    }
151
152    /// Transfer learned clauses to another service.
153    pub fn transfer_learned_clauses_to(&self, target: &mut SolverService) -> LearnedClauseTransfer {
154        let learned = self.learned_clauses.borrow();
155        let count = learned.len();
156        target
157            .learned_clauses
158            .borrow_mut()
159            .extend(learned.iter().cloned());
160        target.trace.borrow_mut().learned_clause_transfers += count;
161        LearnedClauseTransfer { clauses: count }
162    }
163
164    /// Return current service trace.
165    pub fn trace(&self) -> SolverServiceTrace {
166        self.trace.borrow().clone()
167    }
168
169    /// Report that the semantic-oracle facade is not the GPU portfolio path.
170    pub fn gpu_portfolio_status(&self) -> SolverPortfolioStatus {
171        SolverPortfolioStatus::Deferred {
172            reason: "GPU portfolio solving is not implemented in the semantic-oracle facade and blocks solver-service integration closure",
173        }
174    }
175
176    fn solve_assignments(&self, limit: Option<u64>) -> SolverServiceResult {
177        let max = 1u64.checked_shl(self.instance.num_vars).unwrap_or(u64::MAX);
178        let search_max = limit.map_or(max, |limit| limit.min(max));
179        let hard_clauses = self.hard_clauses();
180
181        if self.instance.objective == Objective::MaxSat {
182            return self.solve_maxsat(
183                search_max,
184                limit.is_some() && search_max < max,
185                &hard_clauses,
186            );
187        }
188
189        for mask in 0..search_max {
190            let assignment = assignment_from_mask(self.instance.num_vars, mask);
191            if hard_clauses
192                .iter()
193                .all(|clause| clause.is_satisfied(&assignment))
194            {
195                self.record_cpu_assignment_enumerations(mask.saturating_add(1));
196                return SolverServiceResult {
197                    status: SolverServiceStatus::Sat,
198                    assignment: Some(assignment),
199                };
200            }
201        }
202        self.record_cpu_assignment_enumerations(search_max);
203
204        if limit.is_some() && search_max < max {
205            return SolverServiceResult {
206                status: SolverServiceStatus::Timeout,
207                assignment: None,
208            };
209        }
210
211        self.record_unsat_learning(&hard_clauses);
212        SolverServiceResult {
213            status: SolverServiceStatus::Unsat,
214            assignment: None,
215        }
216    }
217
218    fn solve_maxsat(
219        &self,
220        search_max: u64,
221        timed_out: bool,
222        hard_clauses: &[Clause],
223    ) -> SolverServiceResult {
224        let mut best_assignment = None;
225        let mut best_score = f64::NEG_INFINITY;
226        for mask in 0..search_max {
227            let assignment = assignment_from_mask(self.instance.num_vars, mask);
228            if !hard_clauses
229                .iter()
230                .all(|clause| clause.is_satisfied(&assignment))
231            {
232                continue;
233            }
234            let score = self.instance.weighted_satisfaction(&assignment);
235            if score > best_score {
236                best_score = score;
237                best_assignment = Some(assignment);
238            }
239        }
240        self.record_cpu_maxsat_enumerations(search_max);
241
242        if timed_out {
243            return SolverServiceResult {
244                status: SolverServiceStatus::Timeout,
245                assignment: None,
246            };
247        }
248
249        match best_assignment {
250            Some(assignment) => SolverServiceResult {
251                status: SolverServiceStatus::Optimal(best_score as u64),
252                assignment: Some(assignment),
253            },
254            None => SolverServiceResult {
255                status: SolverServiceStatus::Unsat,
256                assignment: None,
257            },
258        }
259    }
260
261    fn hard_clauses(&self) -> Vec<Clause> {
262        let mut clauses = if self.instance.objective == Objective::MaxSat {
263            Vec::new()
264        } else {
265            self.instance.clauses.clone()
266        };
267        let active_assumptions = self.active_assumptions();
268        clauses.extend(active_assumptions.iter().copied().map(Clause::unit));
269        clauses.extend(
270            self.learned_clauses
271                .borrow()
272                .iter()
273                .filter(|learned| {
274                    learned
275                        .assumption_scope
276                        .iter()
277                        .all(|literal| active_assumptions.contains(literal))
278                })
279                .map(|learned| learned.clause.clone()),
280        );
281        clauses
282    }
283
284    fn record_unsat_learning(&self, hard_clauses: &[Clause]) {
285        let mut learned = self.learned_clauses.borrow_mut();
286        if learned.is_empty() && !hard_clauses.is_empty() {
287            learned.push(ScopedLearnedClause {
288                clause: Clause::new(Vec::new()),
289                assumption_scope: self.active_assumptions(),
290            });
291        }
292    }
293
294    fn record_cpu_assignment_enumerations(&self, count: u64) {
295        let mut trace = self.trace.borrow_mut();
296        trace.cpu_assignment_enumerations = trace.cpu_assignment_enumerations.saturating_add(count);
297    }
298
299    fn record_cpu_maxsat_enumerations(&self, count: u64) {
300        let mut trace = self.trace.borrow_mut();
301        trace.cpu_maxsat_enumerations = trace.cpu_maxsat_enumerations.saturating_add(count);
302    }
303
304    fn active_assumptions(&self) -> Vec<Literal> {
305        self.assumptions.iter().flatten().copied().collect()
306    }
307}
308
309fn assignment_from_mask(num_vars: u32, mask: u64) -> Vec<bool> {
310    (0..num_vars)
311        .map(|var| (mask & (1u64 << var)) != 0)
312        .collect()
313}
xlog_solve/service.rs

xlog_solve/
service.rs
