xlog_solve/
gpu_cnf.rs

1use std::sync::Arc;
2
3use xlog_core::{Result, XlogError};
4use xlog_cuda::memory::TrackedCudaSlice;
5use xlog_cuda::CudaKernelProvider;
6
7use crate::instance::SolveInstance;
8
9/// GPU-resident CNF in CSR form (DIMACS literals, 1-based variable ids).
10///
11/// This is the solver-facing CNF representation used by the GPU CDCL verifier.
12pub struct GpuCnf {
13    /// Variable capacity (>= num_vars).
14    pub var_cap: u32,
15    /// Clause capacity (>= num_clauses).
16    pub clause_cap: u32,
17    /// Literal capacity (>= num_lits).
18    pub lit_cap: u32,
19    /// Device-resident num_vars (len = 1).
20    pub num_vars: TrackedCudaSlice<u32>,
21    /// Device-resident num_clauses (len = 1).
22    pub num_clauses: TrackedCudaSlice<u32>,
23    /// Device-resident num_lits (len = 1).
24    pub num_lits: TrackedCudaSlice<u32>,
25    /// CSR offsets (len = clause_cap + 1).
26    pub clause_offsets: TrackedCudaSlice<u32>,
27    /// Flattened CSR literal array (len = lit_cap).
28    pub literals: TrackedCudaSlice<i32>,
29}
30
31impl GpuCnf {
32    pub(crate) fn require_provider_memory(
33        &self,
34        provider: &CudaKernelProvider,
35        context: &'static str,
36    ) -> Result<()> {
37        let expected_memory = Arc::as_ptr(provider.memory()) as usize;
38        self.require_slice_provider_memory(
39            context,
40            "num_vars",
41            self.num_vars.memory_manager_ptr_value(),
42            expected_memory,
43        )?;
44        self.require_slice_provider_memory(
45            context,
46            "num_clauses",
47            self.num_clauses.memory_manager_ptr_value(),
48            expected_memory,
49        )?;
50        self.require_slice_provider_memory(
51            context,
52            "num_lits",
53            self.num_lits.memory_manager_ptr_value(),
54            expected_memory,
55        )?;
56        self.require_slice_provider_memory(
57            context,
58            "clause_offsets",
59            self.clause_offsets.memory_manager_ptr_value(),
60            expected_memory,
61        )?;
62        self.require_slice_provider_memory(
63            context,
64            "literals",
65            self.literals.memory_manager_ptr_value(),
66            expected_memory,
67        )?;
68
69        if self.num_vars.len() != 1 || self.num_clauses.len() != 1 || self.num_lits.len() != 1 {
70            return Err(XlogError::UnsupportedEpistemicConstruct {
71                construct: context.to_string(),
72                context: format!(
73                    "GPU CNF scalar buffers must have len=1, got num_vars={} num_clauses={} num_lits={}",
74                    self.num_vars.len(),
75                    self.num_clauses.len(),
76                    self.num_lits.len()
77                ),
78            });
79        }
80        let expected_offsets = (self.clause_cap as usize).checked_add(1).ok_or_else(|| {
81            XlogError::UnsupportedEpistemicConstruct {
82                construct: context.to_string(),
83                context: "GPU CNF clause offset length overflowed".to_string(),
84            }
85        })?;
86        if self.clause_offsets.len() != expected_offsets
87            || self.literals.len() != self.lit_cap as usize
88        {
89            return Err(XlogError::UnsupportedEpistemicConstruct {
90                construct: context.to_string(),
91                context: format!(
92                    "GPU CNF buffer lengths must match capacities, got offsets={}/{} literals={}/{}",
93                    self.clause_offsets.len(),
94                    expected_offsets,
95                    self.literals.len(),
96                    self.lit_cap
97                ),
98            });
99        }
100        Ok(())
101    }
102
103    fn require_slice_provider_memory(
104        &self,
105        context: &'static str,
106        name: &'static str,
107        actual_memory: usize,
108        expected_memory: usize,
109    ) -> Result<()> {
110        if actual_memory != expected_memory {
111            return Err(XlogError::UnsupportedEpistemicConstruct {
112                construct: context.to_string(),
113                context: format!(
114                    "GPU CNF buffer {name} belongs to memory manager {actual_memory}, expected {expected_memory}"
115                ),
116            });
117        }
118        Ok(())
119    }
120
121    #[inline]
122    /// Return the allocated literal capacity of this device CNF.
123    pub fn num_literals_cap(&self) -> usize {
124        self.lit_cap as usize
125    }
126
127    /// Host -> device upload helper for tests and tooling.
128    ///
129    /// Production GPU-native paths should build `GpuCnf` directly on device.
130    pub fn from_host(instance: &SolveInstance, provider: &Arc<CudaKernelProvider>) -> Result<Self> {
131        if instance.objective != crate::Objective::Satisfaction {
132            return Err(XlogError::Compilation(format!(
133                "GpuCnf::from_host only supports Objective::Satisfaction, got {:?}",
134                instance.objective
135            )));
136        }
137        if instance.num_vars == 0 {
138            return Err(XlogError::Compilation(
139                "GpuCnf::from_host requires num_vars > 0".to_string(),
140            ));
141        }
142        if instance.num_vars > i32::MAX as u32 {
143            return Err(XlogError::Compilation(
144                "GpuCnf::from_host requires DIMACS variables to fit i32".to_string(),
145            ));
146        }
147        if !instance.validate() {
148            return Err(XlogError::Compilation(
149                "GpuCnf::from_host saw a literal variable outside num_vars".to_string(),
150            ));
151        }
152
153        let num_vars = instance.num_vars;
154        let num_clauses = u32::try_from(instance.clauses.len()).map_err(|_| {
155            XlogError::Compilation("GpuCnf::from_host clause count exceeds u32".to_string())
156        })?;
157        let offsets_len = instance.clauses.len().checked_add(1).ok_or_else(|| {
158            XlogError::Compilation("GpuCnf::from_host clause offset count overflow".to_string())
159        })?;
160        let total_literals = instance.clauses.iter().try_fold(0usize, |acc, clause| {
161            acc.checked_add(clause.literals.len()).ok_or_else(|| {
162                XlogError::Compilation("GpuCnf::from_host literal count overflow".to_string())
163            })
164        })?;
165        let lit_cap = u32::try_from(total_literals).map_err(|_| {
166            XlogError::Compilation("GpuCnf::from_host literal count exceeds u32".to_string())
167        })?;
168
169        // Build CSR on host.
170        let mut clause_offsets: Vec<u32> = Vec::with_capacity(offsets_len);
171        clause_offsets.push(0);
172
173        let mut literals: Vec<i32> = Vec::with_capacity(total_literals);
174        for clause in &instance.clauses {
175            let start = clause_offsets.last().copied().ok_or_else(|| {
176                XlogError::Kernel(
177                    "GpuCnf::from_host internal error: missing initial clause offset".to_string(),
178                )
179            })?;
180            let len = u32::try_from(clause.literals.len()).map_err(|_| {
181                XlogError::Compilation(
182                    "GpuCnf::from_host clause literal count exceeds u32".to_string(),
183                )
184            })?;
185            let end = start
186                .checked_add(len)
187                .ok_or_else(|| XlogError::Compilation("CNF literal count overflow".to_string()))?;
188            clause_offsets.push(end);
189
190            for &lit in &clause.literals {
191                let dimacs = lit.to_dimacs();
192                if dimacs == 0 {
193                    return Err(XlogError::Compilation(
194                        "CNF contains DIMACS 0 literal".to_string(),
195                    ));
196                }
197                literals.push(dimacs);
198            }
199        }
200
201        if clause_offsets.len() != offsets_len {
202            return Err(XlogError::Kernel(
203                "GpuCnf::from_host internal error: offsets length mismatch".to_string(),
204            ));
205        }
206        if literals.len() != total_literals {
207            return Err(XlogError::Kernel(
208                "GpuCnf::from_host internal error: literal length mismatch".to_string(),
209            ));
210        }
211
212        let memory = provider.memory();
213
214        // Device scalars (len=1 each).
215        let mut d_num_vars = memory.alloc::<u32>(1)?;
216        let mut d_num_clauses = memory.alloc::<u32>(1)?;
217        let mut d_num_lits = memory.alloc::<u32>(1)?;
218
219        provider
220            .htod_launch_metadata_sync_copy_into(&[num_vars], &mut d_num_vars)
221            .map_err(|e| XlogError::Kernel(format!("Failed to upload CNF num_vars: {}", e)))?;
222        provider
223            .htod_launch_metadata_sync_copy_into(&[num_clauses], &mut d_num_clauses)
224            .map_err(|e| XlogError::Kernel(format!("Failed to upload CNF num_clauses: {}", e)))?;
225
226        let mut d_offsets = memory.alloc::<u32>(clause_offsets.len())?;
227        let mut d_lits = memory.alloc::<i32>(literals.len())?;
228
229        provider
230            .htod_sync_copy_into_tracked(&clause_offsets, &mut d_offsets)
231            .map_err(|e| XlogError::Kernel(format!("Failed to upload CNF offsets: {}", e)))?;
232        provider
233            .htod_sync_copy_into_tracked(&literals, &mut d_lits)
234            .map_err(|e| XlogError::Kernel(format!("Failed to upload CNF lits: {}", e)))?;
235
236        provider
237            .htod_launch_metadata_sync_copy_into(&[lit_cap], &mut d_num_lits)
238            .map_err(|e| XlogError::Kernel(format!("Failed to upload CNF num_lits: {}", e)))?;
239
240        Ok(Self {
241            var_cap: num_vars,
242            clause_cap: num_clauses,
243            lit_cap,
244            num_vars: d_num_vars,
245            num_clauses: d_num_clauses,
246            num_lits: d_num_lits,
247            clause_offsets: d_offsets,
248            literals: d_lits,
249        })
250    }
251}
xlog_solve/gpu_cnf.rs

xlog_solve/
gpu_cnf.rs
