oxiz_sat/
lib.rs

1//! OxiZ SAT Solver - High-performance CDCL SAT solver
2//!
3//! This crate implements a Conflict-Driven Clause Learning (CDCL) SAT solver
4//! with the following features:
5//! - Two-watched literals scheme for efficient unit propagation
6//! - Multiple branching heuristics (VSIDS, LRB, CHB, VMTF)
7//! - Clause learning with first-UIP scheme and recursive minimization
8//! - Preprocessing (BCE, BVE, subsumption elimination)
9//! - Incremental solving (push/pop)
10//! - DRAT proof generation
11//! - Local search integration
12//! - Parallel portfolio solving
13//! - AllSAT enumeration
14//!
15//! # Examples
16//!
17//! ## Basic SAT Solving
18//!
19//! ```
20//! use oxiz_sat::{Solver, SolverResult, Lit};
21//!
22//! let mut solver = Solver::new();
23//!
24//! // Create variables
25//! let a = solver.new_var();
26//! let b = solver.new_var();
27//! let c = solver.new_var();
28//!
29//! // Add clause: a OR b
30//! solver.add_clause([Lit::pos(a), Lit::pos(b)]);
31//!
32//! // Add clause: NOT a OR c
33//! solver.add_clause([Lit::neg(a), Lit::pos(c)]);
34//!
35//! // Add clause: NOT b OR NOT c
36//! solver.add_clause([Lit::neg(b), Lit::neg(c)]);
37//!
38//! match solver.solve() {
39//!     SolverResult::Sat => println!("Satisfiable!"),
40//!     SolverResult::Unsat => println!("Unsatisfiable!"),
41//!     SolverResult::Unknown => println!("Unknown"),
42//! }
43//! ```
44//!
45//! ## Solving with Assumptions
46//!
47//! ```
48//! use oxiz_sat::{Solver, SolverResult, Lit};
49//!
50//! let mut solver = Solver::new();
51//! let a = solver.new_var();
52//! let b = solver.new_var();
53//!
54//! solver.add_clause([Lit::pos(a), Lit::pos(b)]);
55//!
56//! // Solve assuming a is false
57//! let (result, _) = solver.solve_with_assumptions(&[Lit::neg(a)]);
58//! assert_eq!(result, SolverResult::Sat); // b must be true
59//! ```
60
61#![cfg_attr(not(feature = "std"), no_std)]
62#![cfg_attr(not(feature = "std"), allow(unused_variables))]
63#![deny(unsafe_code)]
64#![warn(missing_docs)]
65
66#[cfg(not(feature = "std"))]
67extern crate alloc;
68
69mod prelude;
70
71// === Always-available modules (no_std compatible) ===
72mod activity;
73mod agility;
74mod allsat;
75mod assumptions;
76mod asymmetric_branching;
77mod autotuning;
78mod backbone;
79mod big;
80mod cardinality;
81mod cce;
82mod chb;
83mod chrono;
84mod chronological_backtrack;
85mod clause;
86mod clause_maintenance;
87pub mod clause_pool;
88mod clause_size_manager;
89mod community;
90mod community_partition;
91mod config_presets;
92mod cube;
93mod distillation;
94#[cfg(feature = "std")]
95mod drat_inprocessing;
96mod dynamic_lbd;
97mod dynamic_subsumption;
98mod els;
99mod extended_resolution;
100mod gate;
101mod hyper_binary;
102mod literal;
103mod local_search;
104mod lookahead;
105mod lrb;
106mod maxsat;
107mod memory;
108mod memory_opt;
109mod ml_branching;
110mod occurrence;
111pub mod preprocessing;
112mod preprocessing_core;
113mod recursive_minimization;
114mod reluctant;
115mod rephasing;
116mod resolution_graph;
117mod smoothed_lbd;
118mod solver;
119mod stabilization;
120mod subsumption;
121mod symmetry;
122mod target_phase;
123mod trail;
124mod trail_saving;
125mod uip_strategies;
126mod unsat_core;
127mod vivification;
128mod vmtf;
129mod vmtf_queue;
130mod vsids;
131mod watched;
132mod xor;
133
134// === std-only modules ===
135#[cfg(feature = "std")]
136mod benchmark;
137#[cfg(feature = "std")]
138mod clause_exchange;
139#[cfg(feature = "std")]
140mod cube_solver;
141#[cfg(feature = "std")]
142mod dimacs;
143#[cfg(feature = "std")]
144mod gpu;
145#[cfg(feature = "std")]
146pub mod parallel;
147#[cfg(feature = "std")]
148mod portfolio;
149#[cfg(feature = "std")]
150mod profiling;
151#[cfg(feature = "std")]
152mod proof;
153#[cfg(feature = "std")]
154mod stats_dashboard;
155
156// === Always-available exports ===
157pub use activity::{ActivityStats, ClauseActivityManager, VariableActivityManager};
158pub use agility::{AgilityStats, AgilityTracker};
159pub use allsat::{AllSatEnumerator, EnumerationConfig, EnumerationResult, EnumerationStats, Model};
160pub use assumptions::{
161    Assumption, AssumptionContext, AssumptionCoreMinimizer, AssumptionLevel, AssumptionStack,
162    AssumptionStats,
163};
164pub use asymmetric_branching::{AsymmetricBranching, AsymmetricBranchingStats};
165pub use autotuning::{
166    Autotuner, AutotuningStats, Configuration, Parameter,
167    PerformanceMetrics as TuningPerformanceMetrics, TuningStrategy,
168};
169pub use backbone::{BackboneAlgorithm, BackboneDetector, BackboneFilter, BackboneStats};
170pub use big::{BigStats, BinaryImplicationGraph};
171pub use cardinality::CardinalityEncoder;
172pub use cce::{CceStats, CoveredClauseElimination};
173pub use chronological_backtrack::{
174    BacktrackDecision, ChronoBacktrackConfig, ChronoBacktrackEngine, ChronoBacktrackStats,
175};
176pub use clause::{Clause, ClauseDatabase, ClauseDatabaseStats, ClauseId, ClauseTier};
177pub use clause_maintenance::{ClauseMaintenance, MaintenanceStats};
178pub use clause_size_manager::{ClauseSizeManager, SizeAdjustmentStrategy, SizeManagerStats};
179pub use community::{
180    Communities, CommunityOrdering, CommunityStats, LouvainDetector, VariableIncidenceGraph,
181};
182pub use community_partition::{CommunityPartition, PartitionStats};
183pub use config_presets::ConfigPreset;
184pub use cube::{Cube, CubeConfig, CubeGenerator, CubeResult, CubeSplittingStrategy, CubeStats};
185pub use distillation::{Distillation, DistillationStats};
186#[cfg(feature = "std")]
187pub use drat_inprocessing::{DratInprocessingConfig, DratInprocessingStats, DratInprocessor};
188pub use dynamic_lbd::{DynamicLbdManager, DynamicLbdStats};
189pub use dynamic_subsumption::{
190    DynamicSubsumption, SubsumptionConfig as DynamicSubsumptionConfig, SubsumptionResult,
191    SubsumptionStats as DynamicSubsumptionStats,
192};
193pub use els::{ElsStats, EquivalentLiteralSubstitution};
194pub use extended_resolution::{ClauseSubstitution, ExtendedResolution, Extension, ExtensionType};
195pub use gate::{GateDetector, GateStats, GateType};
196pub use hyper_binary::{HbrResult, HyperBinaryResolver, HyperBinaryStats};
197pub use literal::{LBool, Lit, Var};
198pub use local_search::{LocalSearch, LocalSearchConfig, LocalSearchResult, LocalSearchStats};
199pub use lookahead::{LookaheadBranching, LookaheadHeuristic, LookaheadStats};
200pub use maxsat::{MaxSatClause, MaxSatConfig, MaxSatResult, MaxSatSolver, MaxSatStats, Weight};
201pub use memory::{ClauseArena, ClauseRef, MemoryStats};
202pub use memory_opt::{MemoryAction, MemoryOptStats, MemoryOptimizer, SizeClass};
203pub use ml_branching::{MLBranching, MLBranchingConfig, MLBranchingStats};
204pub use occurrence::{OccurrenceList, OccurrenceStats};
205pub use preprocessing_core::Preprocessor;
206pub use recursive_minimization::{RecursiveMinStats, RecursiveMinimizer};
207pub use reluctant::{ReluctantDoubling, ReluctantStats};
208pub use rephasing::{RephasingManager, RephasingStats, RephasingStrategy};
209pub use resolution_graph::{
210    GraphStats as ResolutionGraphStats, ResolutionAnalyzer, ResolutionGraph, ResolutionNode,
211};
212pub use smoothed_lbd::{SmoothedLbdStats, SmoothedLbdTracker};
213pub use solver::{
214    RestartStrategy, Solver, SolverConfig, SolverResult, SolverStats, TheoryCallback,
215    TheoryCheckResult,
216};
217pub use stabilization::{
218    SearchMode, StabilizationConfig, StabilizationManager, StabilizationStats,
219};
220pub use subsumption::{SubsumptionChecker, SubsumptionStats};
221pub use symmetry::{
222    AutomorphismDetector, MatrixSymmetry, Permutation, SymmetryBreaker, SymmetryBreakingMethod,
223    SymmetryGroup,
224};
225pub use target_phase::{PhaseMode, TargetPhaseSelector, TargetPhaseStats};
226pub use trail::{Reason, Trail};
227pub use trail_saving::{SavedTrail, TrailSavingManager, TrailSavingStats};
228pub use uip_strategies::{UipAnalysisResult, UipAnalyzer, UipConfig, UipStats, UipStrategy};
229pub use unsat_core::UnsatCore;
230pub use vivification::{Vivification, VivificationStats};
231pub use vmtf::{VMTF, VmtfStats};
232pub use vmtf_queue::{VmtfBumpQueue, VmtfBumpStats};
233pub use xor::{
234    GF2Matrix, GF2Row, PropagateResult, XorAddResult, XorClause, XorClauseId, XorConstraint,
235    XorDetector, XorManager, XorPropagator, XorPropagatorStats, XorStrengthening, XorSubsumption,
236};
237
238// === std-only exports ===
239#[cfg(feature = "std")]
240pub use benchmark::{BenchmarkHarness, BenchmarkResult};
241#[cfg(feature = "std")]
242pub use clause_exchange::{ClauseExchangeBuffer, ExchangeConfig, ExchangeStats, SharedClause};
243#[cfg(feature = "std")]
244pub use cube_solver::{
245    CubeAndConquer, CubeSolveResult, CubeSolverConfig, CubeSolverStats, ParallelCubeSolver,
246};
247#[cfg(feature = "std")]
248pub use dimacs::{DimacsError, DimacsParser, DimacsWriter};
249#[cfg(feature = "std")]
250pub use gpu::{
251    BatchPropagationResult, ClauseManagementResult, ConflictAnalysisResult,
252    CpuReferenceAccelerator, GpuBackend, GpuBenchmark, GpuBenchmarkResult, GpuBenefitAnalysis,
253    GpuConfig, GpuError, GpuRecommendation, GpuSolverAccelerator, GpuStats,
254};
255#[cfg(feature = "std")]
256pub use parallel::{
257    ParallelClauseSimplifier, ParallelProofChecker, PortfolioConfig as ParallelPortfolioConfig,
258    PortfolioResult as ParallelPortfolioResult, PortfolioSolver as ParallelPortfolioSolver,
259    ProofCheckConfig, ProofCheckResult, SimplificationConfig, SimplificationResult, SolverVariant,
260};
261#[cfg(feature = "std")]
262pub use portfolio::{PortfolioConfig, PortfolioResult, PortfolioSolver, PortfolioStats};
263#[cfg(feature = "std")]
264pub use profiling::{AutoTimer, PerformanceMetrics, Profiler, ScopedTimer};
265#[cfg(feature = "std")]
266pub use proof::{DratProof, LratProof, ProofTrimmer};
267#[cfg(feature = "std")]
268pub use stats_dashboard::{StatsAggregator, StatsDashboard};
oxiz_sat/lib.rs

oxiz_sat/
lib.rs
