xlog_solve/
lib.rs

1//! SAT solver services for XLOG.
2#![warn(missing_docs)]
3//!
4//! This crate contains:
5//! - a CPU Continuous Local Search (CLS) solver (heuristic, not complete), and
6//! - a GPU-native CDCL solver (complete SAT/UNSAT) used as the production verifier.
7//!
8//! # Architecture
9//!
10//! - `instance`: SAT instance representation (CNF clauses, literals)
11//! - `solver`: CLS solver with configurable parameters
12//! - `proof`: Proof artifacts and verification
13//!
14//! # Usage
15//!
16//! ```ignore
17//! use xlog_solve::{SolveInstance, Clause, Literal, Solver};
18//!
19//! // Create a SAT instance: (x0 OR NOT x1) AND (x1 OR x2)
20//! let instance = SolveInstance::new(3, vec![
21//!     Clause::new(vec![Literal::positive(0), Literal::negative(1)]),
22//!     Clause::new(vec![Literal::positive(1), Literal::positive(2)]),
23//! ]);
24//!
25//! // Solve
26//! let solver = Solver::new_cpu();
27//! let result = solver.solve(instance);
28//!
29//! match result.status {
30//!     SolveStatus::Sat => println!("Satisfiable!"),
31//!     SolveStatus::Unsat => println!("Unsatisfiable"),
32//!     SolveStatus::Unknown => println!("Could not determine"),
33//!     SolveStatus::Optimal(_) => println!("Found optimal"),
34//! }
35//! ```
36
37#[allow(missing_docs)] // TODO(v0.6): document GPU CDCL solver methods
38mod gpu_cdcl;
39#[allow(missing_docs)] // TODO(v0.6): document or make pub(crate)
40mod gpu_cnf;
41mod instance;
42mod production;
43mod proof;
44mod service;
45mod solver;
46
47pub use gpu_cdcl::{GpuCdclConfig, GpuCdclRawOutput, GpuCdclSolver, GpuCdclWorkspace};
48pub use gpu_cnf::GpuCnf;
49pub use instance::{Clause, Literal, Objective, SolveInstance};
50pub use production::{
51    production_capabilities, GpuSolverAcceptedCandidateState, GpuSolverProductionAdapter,
52    GpuSolverProductionBatchExecutionEvidence, GpuSolverProductionCapabilities,
53    GpuSolverProductionCapabilityStatus, GpuSolverProductionExpectation,
54    GpuSolverProductionLearnedClauseArenaReport, GpuSolverProductionLearnedClauseReuseReport,
55    GpuSolverProductionLifecycleReport, GpuSolverProductionLifecycleStep,
56    GpuSolverProductionMaxSatCandidate, GpuSolverProductionMaxSatLifecycleReport,
57    GpuSolverProductionMaxSatReport, GpuSolverProductionMaxSatScheduleJob,
58    GpuSolverProductionMaxSatScheduleReport, GpuSolverProductionMaxSatSearchCandidate,
59    GpuSolverProductionMaxSatSearchStatus, GpuSolverProductionPortfolioJob,
60    GpuSolverProductionPortfolioReport, GpuSolverProductionTrace,
61    GpuSolverProductionWeightedMaxSatSelection,
62};
63pub use proof::{compute_checksum, SolveProof, SolveResult, SolveStats, SolveStatus};
64pub use service::{
65    LearnedClauseTransfer, SolverPortfolioStatus, SolverService, SolverServiceBudget,
66    SolverServiceResult, SolverServiceStatus, SolverServiceTrace,
67};
68pub use solver::{Solver, SolverConfig, SolverState};
xlog_solve/lib.rs

xlog_solve/
lib.rs
