Crate xlog_solve 

SAT solver services for XLOG.

This crate contains:

• a CPU Continuous Local Search (CLS) solver (heuristic, not complete), and
• a GPU-native CDCL solver (complete SAT/UNSAT) used as the production verifier.

Architecture

• instance: SAT instance representation (CNF clauses, literals)
• solver: CLS solver with configurable parameters
• proof: Proof artifacts and verification

Usage

use xlog_solve::{SolveInstance, Clause, Literal, Solver};

// Create a SAT instance: (x0 OR NOT x1) AND (x1 OR x2)
let instance = SolveInstance::new(3, vec![
    Clause::new(vec![Literal::positive(0), Literal::negative(1)]),
    Clause::new(vec![Literal::positive(1), Literal::positive(2)]),
]);

// Solve
let solver = Solver::new_cpu();
let result = solver.solve(instance);

match result.status {
    SolveStatus::Sat => println!("Satisfiable!"),
    SolveStatus::Unsat => println!("Unsatisfiable"),
    SolveStatus::Unknown => println!("Could not determine"),
    SolveStatus::Optimal(_) => println!("Found optimal"),
}

Structs

Clause

A clause is a disjunction (OR) of literals.

GpuCdclConfig

Configuration for the GPU CDCL (Conflict-Driven Clause Learning) solver.

GpuCdclRawOutput

Raw CDCL outputs (device-resident) for debugging and research.

GpuCdclSolver

GPU-native CDCL SAT solver backed by CUDA kernels.

GpuCdclWorkspace

Pre-allocated solver arena for reuse across multiple CDCL solves.

GpuCnf

GPU-resident CNF in CSR form (DIMACS literals, 1-based variable ids).

GpuSolverAcceptedCandidateState

Solver-facing state derived from an accepted GPU epistemic execution result.

GpuSolverProductionAdapter

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

GpuSolverProductionBatchExecutionEvidence

Accepted split/batch GPU epistemic evidence for solver production reuse.

GpuSolverProductionCapabilities

Capability report for the solver production adapter.

GpuSolverProductionLearnedClauseArenaReport

Summary of a GPU CDCL learned-clause arena publication.

GpuSolverProductionLearnedClauseReuseReport

Summary of a bounded GPU CDCL learned-clause reuse run.

GpuSolverProductionLifecycleReport

Summary of an accepted solver lifecycle run.

GpuSolverProductionLifecycleStep

One accepted solver lifecycle step backed by existing GPU CDCL inputs.

GpuSolverProductionMaxSatCandidate

One GPU-CDCL-backed candidate for bounded weighted MaxSAT production solving.

GpuSolverProductionMaxSatLifecycleReport

Summary of a combined accepted solver lifecycle plus MaxSAT run.

GpuSolverProductionMaxSatReport

Summary of one bounded GPU-backed MaxSAT production adapter run.

GpuSolverProductionMaxSatScheduleReport

Summary of a heterogeneous GPU-backed MaxSAT scheduler batch.

GpuSolverProductionMaxSatSearchCandidate

One GPU-CDCL-backed candidate in a bounded weighted MaxSAT search.

GpuSolverProductionPortfolioReport

Summary of one bounded GPU SAT/MaxSAT/status-aware portfolio run.

GpuSolverProductionTrace

Trace counters proving the production adapter stayed on the GPU CDCL path.

GpuSolverProductionWeightedMaxSatSelection

One caller-declared weighted soft-clause selection for GPU MaxSAT search encoding.

LearnedClauseTransfer

Learned-clause transfer result.

Literal

A propositional variable with optional negation.

SolveInstance

A SAT or MaxSAT instance in Conjunctive Normal Form (CNF).

SolveResult

Complete result from a solve operation.

SolveStats

Statistics from a solve operation.

Solver

The CLS-based SAT/MaxSAT solver.

SolverConfig

Configuration parameters for the CLS solver.

SolverService

Incremental SAT/MaxSAT service facade.

SolverServiceResult

Result returned by the solver service.

SolverServiceTrace

Trace counters for service-level behavior.

SolverState

Internal state during CLS optimization.

Enums

GpuSolverProductionCapabilityStatus

Production capability status for solver paths required by production metric gates.

GpuSolverProductionExpectation

Expected GPU CDCL result for one production lifecycle step.

GpuSolverProductionMaxSatScheduleJob

One job in an accepted GPU-backed MaxSAT scheduler batch.

GpuSolverProductionMaxSatSearchStatus

Expected GPU-CDCL status for a bounded MaxSAT search candidate.

GpuSolverProductionPortfolioJob

One job in a bounded GPU solver portfolio.

Objective

The optimization objective for a SAT/MaxSAT instance.

SolveProof

Proof artifact from a SAT/MaxSAT solver.

SolveStatus

Status of a solve operation.

SolverPortfolioStatus

GPU portfolio status for the semantic-oracle facade.

SolverServiceBudget

Search budget for bounded service solves.

SolverServiceStatus

Status returned by the solver-service interface.

Functions

compute_checksum

Computes an FNV-1a checksum for a boolean assignment.

production_capabilities

Return the current production solver capability report.