Struct GpuSolverProductionAdapter 

pub struct GpuSolverProductionAdapter { /* private fields */ }

Thin adapter from epistemic solver work to the existing GPU CDCL verifier.

Implementations

impl GpuSolverProductionAdapter

pub fn new(provider: Arc<CudaKernelProvider>, config: GpuCdclConfig) -> Self

Create an adapter over the existing GPU CDCL solver implementation.

pub fn trace(&self) -> GpuSolverProductionTrace

Return the current production-path trace counters.

pub fn accepted_candidate_state( &self, provider: &CudaKernelProvider, result: &EpistemicGpuExecutionResult, ) -> Result<GpuSolverAcceptedCandidateState>

Validate accepted GPU epistemic evidence and return the solver-facing candidate state.

pub fn new_workspace( &self, max_var_cap: u32, max_clause_cap: u32, ) -> Result<GpuCdclWorkspace>

Allocate a reusable GPU CDCL workspace through the existing solver.

pub fn solve_expect_sat(&mut self, cnf: &GpuCnf) -> Result<TrackedCudaSlice<i8>>

Solve and enforce SAT entirely on GPU.

pub fn solve_expect_sat_with_gpu_execution_result( &mut self, provider: &CudaKernelProvider, result: &EpistemicGpuExecutionResult, cnf: &GpuCnf, ) -> Result<TrackedCudaSlice<i8>>

Solve SAT through GPU CDCL after an accepted GPU epistemic execution result.

pub fn solve_expect_unsat_with_gpu_execution_result( &mut self, provider: &CudaKernelProvider, result: &EpistemicGpuExecutionResult, cnf: &GpuCnf, ) -> Result<()>

Solve UNSAT through GPU CDCL after an accepted GPU epistemic execution result.

pub fn solve_expect_unsat(&mut self, cnf: &GpuCnf) -> Result<()>

Solve and enforce UNSAT entirely on GPU.

pub fn solve_expect_unsat_with_branch_limit_ws( &mut self, workspace: &mut GpuCdclWorkspace, cnf: &GpuCnf, branch_var_limit: &TrackedCudaSlice<u32>, ) -> Result<()>

Solve and enforce UNSAT entirely on GPU using a reusable workspace.

pub fn solve_expect_unsat_with_branch_limit_ws_with_gpu_execution_result( &mut self, provider: &CudaKernelProvider, result: &EpistemicGpuExecutionResult, workspace: &mut GpuCdclWorkspace, cnf: &GpuCnf, branch_var_limit: &TrackedCudaSlice<u32>, ) -> Result<()>

Solve workspace-backed UNSAT through GPU CDCL after accepted GPU epistemic execution.

pub fn solve_assumption_lifecycle_with_gpu_execution_result( &mut self, provider: &CudaKernelProvider, result: &EpistemicGpuExecutionResult, workspace: &mut GpuCdclWorkspace, steps: &[GpuSolverProductionLifecycleStep<'_>], ) -> Result<GpuSolverProductionLifecycleReport>

Execute an accepted push/solve/retract lifecycle through existing GPU CDCL calls.

pub fn solve_multi_candidate_assumption_lifecycle_with_gpu_execution_results( &mut self, provider: &CudaKernelProvider, results: &[&EpistemicGpuExecutionResult], workspace: &mut GpuCdclWorkspace, steps: &[GpuSolverProductionLifecycleStep<'_>], ) -> Result<GpuSolverProductionLifecycleReport>

Execute accepted push/solve/retract lifecycles for multiple GPU epistemic candidates.

Each candidate result is validated against the accepted GPU execution boundary, then the same lifecycle steps are dispatched through the existing GPU CDCL SAT/UNSAT paths.

pub fn solve_assumption_lifecycle_with_gpu_batch_execution_result( &mut self, provider: &CudaKernelProvider, evidence: GpuSolverProductionBatchExecutionEvidence<'_>, workspace: &mut GpuCdclWorkspace, steps: &[GpuSolverProductionLifecycleStep<'_>], ) -> Result<GpuSolverProductionLifecycleReport>

Execute accepted split/batch push/solve/retract lifecycles through existing GPU CDCL calls.

The batch evidence must prove every split component ran through the single-plan GPU runtime path with zero aggregate CPU recomposition, candidate/world-view fallback, tracked hot-path device-to-host transfer, and per-candidate host round trips, plus aggregate CUDA-event timing.

pub fn solve_unsat_and_publish_learned_clause_arena_with_gpu_execution_result( &mut self, provider: &CudaKernelProvider, result: &EpistemicGpuExecutionResult, workspace: &mut GpuCdclWorkspace, cnf: &GpuCnf, branch_var_limit: &TrackedCudaSlice<u32>, ) -> Result<GpuSolverProductionLearnedClauseArenaReport>

Populate and publish the existing GPU CDCL learned-clause/proof arena.

This records that an accepted epistemic candidate reached the GPU CDCL learned-clause device buffers. Import/reuse is covered by the bounded same-device-CNF reuse API below.

pub fn solve_unsat_then_reuse_learned_clauses_with_gpu_execution_result( &mut self, provider: &CudaKernelProvider, result: &EpistemicGpuExecutionResult, workspace: &mut GpuCdclWorkspace, source_cnf: &GpuCnf, source_branch_var_limit: &TrackedCudaSlice<u32>, target_cnf: &GpuCnf, target_branch_var_limit: &TrackedCudaSlice<u32>, ) -> Result<GpuSolverProductionLearnedClauseReuseReport>

Publish learned clauses from one accepted GPU UNSAT solve and import them into another.

This is deliberately bounded to same-device-CNF reuse. The existing GPU proof trace is valid for the imported solve only when the base CNF buffers are the same.

pub fn solve_multi_candidate_learned_clause_reuse_with_gpu_execution_results( &mut self, provider: &CudaKernelProvider, results: &[&EpistemicGpuExecutionResult], workspace: &mut GpuCdclWorkspace, source_cnf: &GpuCnf, source_branch_var_limit: &TrackedCudaSlice<u32>, target_cnf: &GpuCnf, target_branch_var_limit: &TrackedCudaSlice<u32>, ) -> Result<GpuSolverProductionLearnedClauseReuseReport>

Publish and reuse learned clauses once per accepted GPU epistemic candidate.

pub fn solve_learned_clause_reuse_with_gpu_batch_execution_result( &mut self, provider: &CudaKernelProvider, evidence: GpuSolverProductionBatchExecutionEvidence<'_>, workspace: &mut GpuCdclWorkspace, source_cnf: &GpuCnf, source_branch_var_limit: &TrackedCudaSlice<u32>, target_cnf: &GpuCnf, target_branch_var_limit: &TrackedCudaSlice<u32>, ) -> Result<GpuSolverProductionLearnedClauseReuseReport>

Publish and reuse learned clauses once per accepted split/batch GPU component.

The batch evidence must prove every split component reused the existing single-plan GPU runtime path before each component is delegated to the existing multi-candidate learned-clause reuse adapter.

pub fn solve_weighted_maxsat_candidates_with_gpu_execution_result( &mut self, provider: &CudaKernelProvider, result: &EpistemicGpuExecutionResult, candidates: &[GpuSolverProductionMaxSatCandidate<'_>], ) -> Result<GpuSolverProductionMaxSatReport>

Solve a bounded weighted MaxSAT candidate set after accepted GPU epistemic execution.

CPU orchestration is limited to launching/checking the provided candidate CNFs and comparing their declared scores. Each candidate is certified by the existing GPU CDCL SAT path; this adapter performs no CPU assignment or MaxSAT enumeration.

pub fn solve_maxsat_lifecycle_with_gpu_execution_result( &mut self, provider: &CudaKernelProvider, result: &EpistemicGpuExecutionResult, workspace: &mut GpuCdclWorkspace, steps: &[GpuSolverProductionLifecycleStep<'_>], candidates: &[GpuSolverProductionMaxSatCandidate<'_>], ) -> Result<GpuSolverProductionMaxSatLifecycleReport>

Execute an accepted solver lifecycle, then a bounded MaxSAT candidate set.

The same accepted GPU epistemic evidence gates both phases. The adapter records that evidence once, while lifecycle and MaxSAT counters prove the existing GPU CDCL paths handled all solver work without CPU search.

pub fn solve_multi_candidate_maxsat_lifecycle_with_gpu_execution_results( &mut self, provider: &CudaKernelProvider, results: &[&EpistemicGpuExecutionResult], workspace: &mut GpuCdclWorkspace, steps: &[GpuSolverProductionLifecycleStep<'_>], candidates: &[GpuSolverProductionMaxSatCandidate<'_>], ) -> Result<GpuSolverProductionMaxSatLifecycleReport>

Execute accepted solver lifecycle plus MaxSAT candidate-set work once per evidence record.

pub fn solve_maxsat_lifecycle_with_gpu_batch_execution_result( &mut self, provider: &CudaKernelProvider, evidence: GpuSolverProductionBatchExecutionEvidence<'_>, workspace: &mut GpuCdclWorkspace, steps: &[GpuSolverProductionLifecycleStep<'_>], candidates: &[GpuSolverProductionMaxSatCandidate<'_>], ) -> Result<GpuSolverProductionMaxSatLifecycleReport>

Execute accepted split/batch solver lifecycle plus MaxSAT candidate-set work.

pub fn solve_multi_candidate_weighted_maxsat_with_gpu_execution_results( &mut self, provider: &CudaKernelProvider, results: &[&EpistemicGpuExecutionResult], candidates: &[GpuSolverProductionMaxSatCandidate<'_>], ) -> Result<GpuSolverProductionMaxSatReport>

Solve a bounded weighted MaxSAT candidate set once per accepted GPU epistemic candidate.

pub fn solve_weighted_maxsat_candidates_with_gpu_batch_execution_result( &mut self, provider: &CudaKernelProvider, evidence: GpuSolverProductionBatchExecutionEvidence<'_>, candidates: &[GpuSolverProductionMaxSatCandidate<'_>], ) -> Result<GpuSolverProductionMaxSatReport>

Solve a bounded weighted MaxSAT candidate set once per accepted split/batch GPU component.

The batch evidence must prove every split component reused the existing single-plan GPU runtime path before each component is delegated to the existing multi-candidate MaxSAT adapter.

pub fn solve_weighted_maxsat_search_with_gpu_execution_result( &mut self, provider: &CudaKernelProvider, result: &EpistemicGpuExecutionResult, workspace: &mut GpuCdclWorkspace, candidates: &[GpuSolverProductionMaxSatSearchCandidate<'_>], ) -> Result<GpuSolverProductionMaxSatReport>

Search a bounded weighted MaxSAT candidate set after accepted GPU epistemic execution.

Satisfiable candidates are scored through the existing GPU CDCL SAT path. Unsatisfiable candidates are pruned through the existing workspace-backed GPU CDCL UNSAT path. The adapter records no CPU assignment or MaxSAT enumeration.

pub fn solve_weighted_maxsat_search_with_gpu_batch_execution_result( &mut self, provider: &CudaKernelProvider, evidence: GpuSolverProductionBatchExecutionEvidence<'_>, workspace: &mut GpuCdclWorkspace, candidates: &[GpuSolverProductionMaxSatSearchCandidate<'_>], ) -> Result<GpuSolverProductionMaxSatReport>

Search a bounded weighted MaxSAT candidate set once per accepted split-batch component.

pub fn solve_multi_candidate_weighted_maxsat_search_with_gpu_execution_results( &mut self, provider: &CudaKernelProvider, results: &[&EpistemicGpuExecutionResult], workspace: &mut GpuCdclWorkspace, candidates: &[GpuSolverProductionMaxSatSearchCandidate<'_>], ) -> Result<GpuSolverProductionMaxSatReport>

Search a bounded weighted MaxSAT candidate set once per accepted GPU evidence record.

pub fn solve_weighted_maxsat_encoded_search_with_gpu_execution_result( &mut self, provider: &CudaKernelProvider, result: &EpistemicGpuExecutionResult, workspace: &mut GpuCdclWorkspace, weighted: &SolveInstance, branch_var_limit: &TrackedCudaSlice<u32>, selections: &[GpuSolverProductionWeightedMaxSatSelection<'_>], ) -> Result<GpuSolverProductionMaxSatReport>

Encode weighted soft-clause selections, then search them after accepted GPU evidence.

Candidate construction is bounded by caller-declared selections. The adapter builds satisfaction CNFs for those selections, uploads them through the existing GPU CNF layout, and dispatches SAT/UNSAT certification through GPU CDCL. It performs no CPU assignment or MaxSAT subset enumeration.

pub fn solve_multi_candidate_weighted_maxsat_encoded_search_with_gpu_execution_results( &mut self, provider: &CudaKernelProvider, results: &[&EpistemicGpuExecutionResult], workspace: &mut GpuCdclWorkspace, weighted: &SolveInstance, branch_var_limit: &TrackedCudaSlice<u32>, selections: &[GpuSolverProductionWeightedMaxSatSelection<'_>], ) -> Result<GpuSolverProductionMaxSatReport>

Encode weighted soft-clause selections, then search once per accepted GPU evidence record.

This is the multi-candidate scheduler-facing variant of the bounded encoded MaxSAT search adapter. It validates all accepted GPU epistemic evidence up front, encodes the caller-declared selections through the existing GPU CNF layout for each accepted record, and dispatches each candidate through GPU CDCL SAT/UNSAT certification without CPU assignment or MaxSAT enumeration.

pub fn solve_weighted_maxsat_encoded_search_with_gpu_batch_execution_result( &mut self, provider: &CudaKernelProvider, evidence: GpuSolverProductionBatchExecutionEvidence<'_>, workspace: &mut GpuCdclWorkspace, weighted: &SolveInstance, branch_var_limit: &TrackedCudaSlice<u32>, selections: &[GpuSolverProductionWeightedMaxSatSelection<'_>], ) -> Result<GpuSolverProductionMaxSatReport>

Encode weighted soft-clause selections, then search once per accepted split-batch component.

The batch evidence must prove every split component reused the existing single-plan GPU runtime path before each component is delegated to the existing multi-candidate weighted MaxSAT encoding adapter.

pub fn solve_maxsat_schedule_with_gpu_execution_results( &mut self, provider: &CudaKernelProvider, results: &[&EpistemicGpuExecutionResult], workspace: &mut GpuCdclWorkspace, jobs: &[GpuSolverProductionMaxSatScheduleJob<'_>], ) -> Result<GpuSolverProductionMaxSatScheduleReport>

Execute a heterogeneous MaxSAT schedule once per accepted GPU evidence record.

The scheduler is a thin production-path adapter: it validates accepted epistemic GPU execution up front, then dispatches candidate-set, search-pruning, and weighted encoded-search jobs through the existing GPU CNF/CDCL helpers. UNKNOWN and TIMEOUT jobs are status propagation records; they never fall back to CPU assignment or MaxSAT enumeration.

pub fn solve_maxsat_schedule_with_gpu_batch_execution_result( &mut self, provider: &CudaKernelProvider, evidence: GpuSolverProductionBatchExecutionEvidence<'_>, workspace: &mut GpuCdclWorkspace, jobs: &[GpuSolverProductionMaxSatScheduleJob<'_>], ) -> Result<GpuSolverProductionMaxSatScheduleReport>

Execute a heterogeneous MaxSAT schedule once per accepted split-batch component.

This preserves the scheduler’s existing GPU CNF/CDCL dispatch behavior while requiring aggregate split-batch evidence with zero CPU recomposition, fallback, and per-candidate host round trips before any scheduled job runs.

pub fn solve_portfolio_with_gpu_execution_result( &mut self, provider: &CudaKernelProvider, result: &EpistemicGpuExecutionResult, jobs: &[GpuSolverProductionPortfolioJob<'_>], ) -> Result<GpuSolverProductionPortfolioReport>

Execute a bounded SAT/MaxSAT/status-aware portfolio after accepted GPU epistemic execution.

The portfolio is a production adapter over existing GPU CDCL calls. It records per-job counters and rejects empty portfolios without falling back to the CPU semantic-oracle solver.

pub fn solve_multi_candidate_portfolio_with_gpu_execution_results( &mut self, provider: &CudaKernelProvider, results: &[&EpistemicGpuExecutionResult], jobs: &[GpuSolverProductionPortfolioJob<'_>], ) -> Result<GpuSolverProductionPortfolioReport>

Execute the same bounded portfolio once per accepted GPU epistemic candidate.

pub fn solve_portfolio_with_gpu_batch_execution_result( &mut self, provider: &CudaKernelProvider, evidence: GpuSolverProductionBatchExecutionEvidence<'_>, jobs: &[GpuSolverProductionPortfolioJob<'_>], ) -> Result<GpuSolverProductionPortfolioReport>

Execute a bounded SAT/MaxSAT/status-aware portfolio for accepted split/batch evidence.

The batch evidence must prove every split component reused the existing single-plan GPU runtime path before each component is delegated to the existing multi-candidate portfolio adapter.