Struct GpuCdclSolver 

pub struct GpuCdclSolver { /* private fields */ }

GPU-native CDCL SAT solver backed by CUDA kernels.

Implementations

impl GpuCdclSolver

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

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

Pre-allocate a reusable solver arena.

max_var_cap and max_clause_cap must be >= the var_cap / clause_cap of any GpuCnf that will be solved with this workspace. If a solve call exceeds these capacities, it returns XlogError::Kernel.

pub fn solve_raw_with_branch_limit( &self, cnf: &GpuCnf, branch_var_limit: &TrackedCudaSlice<u32>, ) -> Result<GpuCdclRawOutput>

Launch CDCL and return raw device outputs without enforcing SAT/UNSAT on device.

This is intentionally not used in production verifier paths. It exists so tests and debugging tools can inspect out_status/out_error without modifying kernel behavior.

pub fn solve_raw_with_branch_limit_gated( &self, cnf: &GpuCnf, compile_needed: &TrackedCudaSlice<u32>, branch_var_limit: &TrackedCudaSlice<u32>, ) -> Result<GpuCdclRawOutput>

Gated variant of solve_raw_with_branch_limit.

pub fn solve_raw_with_decision_ranges( &self, cnf: &GpuCnf, decision_base_limit: &TrackedCudaSlice<u32>, decision_extra_base: &TrackedCudaSlice<u32>, decision_extra_count: &TrackedCudaSlice<u32>, ) -> Result<GpuCdclRawOutput>

Launch CDCL and return raw device outputs without enforcing SAT/UNSAT on device, using an explicit decision variable set:

• decision vars include all v in 1..=decision_base_limit[0] and decision_extra_base[0]..(decision_extra_base[0] + decision_extra_count[0] - 1).

Production verifier paths should prefer solve_expect_* methods which enforce results on GPU without host reads.

pub fn solve_raw_with_decision_ranges_gated( &self, cnf: &GpuCnf, compile_needed: &TrackedCudaSlice<u32>, decision_base_limit: &TrackedCudaSlice<u32>, decision_extra_base: &TrackedCudaSlice<u32>, decision_extra_count: &TrackedCudaSlice<u32>, ) -> Result<GpuCdclRawOutput>

Gated variant of solve_raw_with_decision_ranges.

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

Solve and enforce SAT entirely on GPU (no device->host reads).

pub fn solve_expect_sat_gated( &self, cnf: &GpuCnf, compile_needed: &TrackedCudaSlice<u32>, ) -> Result<TrackedCudaSlice<i8>>

Solve and enforce SAT entirely on GPU (no device->host reads), skipping all GPU work if compile_needed is 0.

pub fn solve_expect_sat_with_decision_ranges( &self, cnf: &GpuCnf, decision_base_limit: &TrackedCudaSlice<u32>, decision_extra_base: &TrackedCudaSlice<u32>, decision_extra_count: &TrackedCudaSlice<u32>, ) -> Result<TrackedCudaSlice<i8>>

Solve and enforce SAT entirely on GPU (no device->host reads), using an explicit decision variable set:

• decision vars include all v in 1..=decision_base_limit[0] and decision_extra_base[0]..(decision_extra_base[0] + decision_extra_count[0] - 1).

pub fn solve_expect_sat_with_decision_ranges_gated( &self, cnf: &GpuCnf, compile_needed: &TrackedCudaSlice<u32>, decision_base_limit: &TrackedCudaSlice<u32>, decision_extra_base: &TrackedCudaSlice<u32>, decision_extra_count: &TrackedCudaSlice<u32>, ) -> Result<TrackedCudaSlice<i8>>

Gated variant of solve_expect_sat_with_decision_ranges.

pub fn solve_expect_sat_with_branch_limit( &self, cnf: &GpuCnf, branch_var_limit: &TrackedCudaSlice<u32>, ) -> Result<TrackedCudaSlice<i8>>

Solve and enforce SAT entirely on GPU (no device->host reads), restricting branching to variables in 1..=branch_var_limit[0].

pub fn solve_expect_sat_with_branch_limit_gated( &self, cnf: &GpuCnf, compile_needed: &TrackedCudaSlice<u32>, branch_var_limit: &TrackedCudaSlice<u32>, ) -> Result<TrackedCudaSlice<i8>>

Solve and enforce SAT entirely on GPU (no device->host reads), skipping all GPU work if compile_needed is 0, and restricting branching to variables in 1..=branch_var_limit[0].

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

Solve and enforce UNSAT entirely on GPU (no device->host reads).

pub fn solve_expect_unsat_gated( &self, cnf: &GpuCnf, compile_needed: &TrackedCudaSlice<u32>, ) -> Result<()>

Solve and enforce UNSAT entirely on GPU (no device->host reads), skipping all GPU work if compile_needed is 0.

pub fn solve_expect_unsat_with_branch_limit( &self, cnf: &GpuCnf, branch_var_limit: &TrackedCudaSlice<u32>, ) -> Result<()>

Solve and enforce UNSAT entirely on GPU (no device->host reads), restricting branching to variables in 1..=branch_var_limit[0].

pub fn solve_expect_unsat_with_decision_ranges( &self, cnf: &GpuCnf, decision_base_limit: &TrackedCudaSlice<u32>, decision_extra_base: &TrackedCudaSlice<u32>, decision_extra_count: &TrackedCudaSlice<u32>, ) -> Result<()>

Solve and enforce UNSAT with GPU proof verification, using an explicit decision variable set:

• decision vars include all v in 1..=decision_base_limit[0] and decision_extra_base[0]..(decision_extra_base[0] + decision_extra_count[0] - 1).

pub fn solve_expect_unsat_with_branch_limit_gated( &self, cnf: &GpuCnf, compile_needed: &TrackedCudaSlice<u32>, branch_var_limit: &TrackedCudaSlice<u32>, ) -> Result<()>

Solve and enforce UNSAT entirely on GPU (no device->host reads), skipping all GPU work if compile_needed is 0, and restricting branching to variables in 1..=branch_var_limit[0].

pub fn solve_expect_unsat_with_decision_ranges_gated( &self, cnf: &GpuCnf, compile_needed: &TrackedCudaSlice<u32>, decision_base_limit: &TrackedCudaSlice<u32>, decision_extra_base: &TrackedCudaSlice<u32>, decision_extra_count: &TrackedCudaSlice<u32>, ) -> Result<()>

Solve and enforce UNSAT entirely on GPU (no device->host reads), using an explicit decision variable set:

• decision vars include all v in 1..=decision_base_limit[0] and decision_extra_base[0]..(decision_extra_base[0] + decision_extra_count[0] - 1).

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

Solve and enforce UNSAT entirely on GPU using a pre-allocated workspace, restricting branching to variables in 1..=branch_var_limit[0].

pub fn solve_expect_unsat_with_branch_limit_gated_ws( &self, ws: &mut GpuCdclWorkspace, cnf: &GpuCnf, compile_needed: &TrackedCudaSlice<u32>, branch_var_limit: &TrackedCudaSlice<u32>, ) -> Result<()>

Gated workspace variant: solve and enforce UNSAT entirely on GPU, restricting branching to variables in 1..=branch_var_limit[0]. Skips all GPU work if compile_needed is 0.

pub fn solve_expect_unsat_with_decision_ranges_ws( &self, ws: &mut GpuCdclWorkspace, cnf: &GpuCnf, decision_base_limit: &TrackedCudaSlice<u32>, decision_extra_base: &TrackedCudaSlice<u32>, decision_extra_count: &TrackedCudaSlice<u32>, ) -> Result<()>

Solve and enforce UNSAT entirely on GPU using a pre-allocated workspace, with explicit decision variable ranges.

pub fn solve_expect_unsat_with_decision_ranges_gated_ws( &self, ws: &mut GpuCdclWorkspace, cnf: &GpuCnf, compile_needed: &TrackedCudaSlice<u32>, decision_base_limit: &TrackedCudaSlice<u32>, decision_extra_base: &TrackedCudaSlice<u32>, decision_extra_count: &TrackedCudaSlice<u32>, ) -> Result<()>

Gated workspace variant (LEAF): solve and enforce UNSAT entirely on GPU using a pre-allocated workspace, with explicit decision variable ranges. Skips all GPU work if compile_needed is 0.

This is the leaf implementation for all _ws UNSAT methods. It:

1. Launches CDCL via launch_cdcl_with_workspace_gated
2. Asserts UNSAT status on GPU
3. Verifies the UNSAT proof on GPU (sat_proof_mark_needed + sat_proof_check + sat_assert_ok)

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

Solve and enforce UNSAT on GPU while importing the current workspace learned arena.

The imported learned count is read from ws.out_learned_count on device. Callers must only use this when the imported learned clauses are valid for cnf.