Crate oxiz_sat

Expand description

OxiZ SAT Solver - High-performance CDCL SAT solver

This crate implements a Conflict-Driven Clause Learning (CDCL) SAT solver with the following features:

Two-watched literals scheme for efficient unit propagation
Multiple branching heuristics (VSIDS, LRB, CHB, VMTF)
Clause learning with first-UIP scheme and recursive minimization
Preprocessing (BCE, BVE, subsumption elimination)
Incremental solving (push/pop)
DRAT proof generation
Local search integration
Parallel portfolio solving
AllSAT enumeration

§Examples

§Basic SAT Solving

use oxiz_sat::{Solver, SolverResult, Lit};

let mut solver = Solver::new();

// Create variables
let a = solver.new_var();
let b = solver.new_var();
let c = solver.new_var();

// Add clause: a OR b
solver.add_clause([Lit::pos(a), Lit::pos(b)]);

// Add clause: NOT a OR c
solver.add_clause([Lit::neg(a), Lit::pos(c)]);

// Add clause: NOT b OR NOT c
solver.add_clause([Lit::neg(b), Lit::neg(c)]);

match solver.solve() {
    SolverResult::Sat => println!("Satisfiable!"),
    SolverResult::Unsat => println!("Unsatisfiable!"),
    SolverResult::Unknown => println!("Unknown"),
}

§Solving with Assumptions

use oxiz_sat::{Solver, SolverResult, Lit};

let mut solver = Solver::new();
let a = solver.new_var();
let b = solver.new_var();

solver.add_clause([Lit::pos(a), Lit::pos(b)]);

// Solve assuming a is false
let (result, _) = solver.solve_with_assumptions(&[Lit::neg(a)]);
assert_eq!(result, SolverResult::Sat); // b must be true

Re-exports§

pub use parallel::ParallelClauseSimplifier;
pub use parallel::ParallelProofChecker;
pub use parallel::PortfolioConfig as ParallelPortfolioConfig;
pub use parallel::PortfolioResult as ParallelPortfolioResult;
pub use parallel::PortfolioSolver as ParallelPortfolioSolver;
pub use parallel::ProofCheckConfig;
pub use parallel::ProofCheckResult;
pub use parallel::SimplificationConfig;
pub use parallel::SimplificationResult;
pub use parallel::SolverVariant;

Modules§

clause_pool: Clause allocation pool for recycling deleted clause memory.
parallel: Parallel SAT Solver Components.
preprocessing: SAT Preprocessing Techniques - Advanced Extensions.

Macros§

time_scope: Macro for creating a scoped timer that logs on drop

Structs§

ActivityStats: Statistics for activity management
AgilityStats: Statistics for agility tracking
AgilityTracker: Agility tracker
AllSatEnumerator: All-SAT enumerator for finding multiple satisfying assignments
Assumption: Assumption with metadata
AssumptionContext: Assumption-based solving context
AssumptionCoreMinimizer: Assumption core minimizer
AssumptionLevel: Assumption level for hierarchical assumption management
AssumptionStack: Assumption stack with level management
AssumptionStats: Statistics for assumption-based solving
AsymmetricBranching: Asymmetric Branching engine
AsymmetricBranchingStats: Statistics for Asymmetric Branching
AutoTimer: RAII timer that automatically reports on drop
AutomorphismDetector: Graph automorphism detection for finding symmetries
Autotuner: Auto-tuning manager
AutotuningStats: Statistics for auto-tuning
BackboneDetector: Backbone detector
BackboneFilter: Backbone filter for literal selection
BackboneStats: Statistics for backbone computation
BatchPropagationResult: Result of a batch unit propagation operation
BenchmarkHarness: Benchmark harness for running SAT solver on multiple instances
BenchmarkResult: Result of a single benchmark run
BigStats: Statistics for BIG optimization
BinaryImplicationGraph: Binary Implication Graph optimizer
CardinalityEncoder: Cardinality constraint encoder
CceStats: Statistics for CCE
ChronoBacktrackConfig: Configuration for chronological backtracking.
ChronoBacktrackEngine: Chronological backtracking decision engine.
ChronoBacktrackStats: Statistics for chronological backtracking.
Clause: A clause is a disjunction of literals
ClauseActivityManager: Clause activity manager
ClauseArena: Memory arena for clause storage
ClauseDatabase: Database of clauses with memory pool
ClauseDatabaseStats: Statistics for clause database
ClauseExchangeBuffer: Clause exchange buffer shared between solvers
ClauseId: Unique identifier for a clause
ClauseMaintenance: Clause maintenance manager
ClauseManagementResult: Result of clause database management operation
ClauseRef: Clause reference in the memory arena
ClauseSizeManager: Clause size manager
ClauseSubstitution: Clause substitution using extension variables
Communities: Community structure representing a partition of variables.
CommunityOrdering: Community-aware variable ordering.
CommunityPartition: Partitioned clause database organized by variable communities.
CommunityStats: Statistics for community detection.
Configuration: Configuration with parameters and performance metrics
ConflictAnalysisResult: Result of parallel conflict analysis
CoveredClauseElimination: Covered Clause Elimination engine
CpuReferenceAccelerator: CPU reference implementation of GPU-acceleratable operations
Cube: A cube represents a partial assignment (conjunction of literals).
CubeAndConquer: Cube-and-Conquer orchestrator that combines cube generation and solving.
CubeConfig: Configuration for cube generation.
CubeGenerator: Cube generator using recursive splitting.
CubeSolveResult: Result of solving a single cube.
CubeSolverConfig: Configuration for parallel cube solving.
CubeSolverStats: Statistics for cube solving.
CubeStats: Statistics for cube generation.
DimacsParser: DIMACS CNF parser
DimacsWriter: DIMACS CNF writer
Distillation: Clause distillation manager
DistillationStats: Statistics for distillation
DratInprocessingConfig: Configuration for DRAT-based inprocessing
DratInprocessingStats: Statistics for DRAT-based inprocessing
DratInprocessor: DRAT-based Inprocessor
DratProof: DRAT proof logger
DynamicLbdManager: Dynamic LBD manager
DynamicLbdStats: Statistics for dynamic LBD updates
DynamicSubsumption: Dynamic subsumption engine.
DynamicSubsumptionConfig: Configuration for dynamic subsumption.
DynamicSubsumptionStats: Statistics for subsumption.
ElsStats: Statistics for equivalent literal substitution
EnumerationConfig: Configuration for model enumeration
EnumerationStats: Statistics for model enumeration
EquivalentLiteralSubstitution: Equivalent Literal Substitution engine
ExchangeConfig: Configuration for clause exchange
ExchangeStats: Statistics for clause exchange
ExtendedResolution: Extended resolution manager
Extension: Extension variable definition
GF2Matrix: GF(2) matrix for efficient Gaussian elimination
GF2Row: GF(2) row representation using bit vectors for efficient XOR operations
GateDetector: Gate detector and optimizer
GateStats: Statistics for gate detection
GpuBenchmark: GPU benchmark harness
GpuBenchmarkResult: GPU vs CPU benchmark result
GpuBenefitAnalysis: Analysis of when GPU acceleration would be beneficial
GpuConfig: GPU configuration options
GpuStats: GPU operation statistics
HyperBinaryResolver: Hyper-binary resolution manager
HyperBinaryStats: Statistics for hyper-binary resolution
Lit: A literal (positive or negative occurrence of a variable)
LocalSearch: Local Search SAT Solver
LocalSearchConfig: Configuration for local search
LocalSearchStats: Statistics for local search
LookaheadBranching: Look-ahead branching manager
LookaheadStats: Statistics for look-ahead branching
LouvainDetector: Louvain community detection algorithm.
LratProof: LRAT proof logger
MLBranching: ML-based branching heuristic
MLBranchingConfig: Configuration for ML-based branching
MLBranchingStats: Statistics for ML-based branching
MaintenanceStats: Statistics for clause maintenance operations
MatrixSymmetry: Matrix variable indexing helper
MaxSatClause: MaxSAT clause - can be hard or soft (with weight)
MaxSatConfig: MaxSAT solver configuration
MaxSatResult: Result of MaxSAT solving
MaxSatSolver: Core-guided MaxSAT solver
MaxSatStats: Statistics for MaxSAT solving
MemoryOptStats: Memory statistics
MemoryOptimizer: Memory optimizer with size-class pools
MemoryStats: Memory usage statistics
OccurrenceList: Occurrence list manager
OccurrenceStats: Statistics for occurrence tracking
ParallelCubeSolver: Parallel cube solver.
Parameter: A tunable parameter
PartitionStats: Statistics for community-based partitioning.
PerformanceMetrics: Performance metrics tracker
Permutation: Represents a permutation of variables
PortfolioConfig: Configuration for a portfolio solver instance
PortfolioResult: Result from a portfolio solver thread
PortfolioSolver: Portfolio solver that runs multiple solvers in parallel
PortfolioStats: Portfolio statistics
Preprocessor: Preprocessing context
Profiler: Profiler for tracking multiple timers and operation counts
ProofTrimmer: Proof trimmer for removing unnecessary clauses
RecursiveMinStats: Statistics for recursive minimization
RecursiveMinimizer: Recursive clause minimization manager
ReluctantDoubling: Reluctant doubling restart manager
ReluctantStats: Statistics for reluctant doubling
RephasingManager: Rephasing manager
RephasingStats: Statistics for rephasing operations
ResolutionAnalyzer: Resolution Graph Analyzer
ResolutionGraph: Resolution Graph for analyzing proof structure
ResolutionGraphStats: Statistics about the resolution graph
ResolutionNode: Node in the resolution graph
SavedTrail: A saved trail representing a sequence of decisions
ScopedTimer: A named timer for profiling code sections
SharedClause: A shared clause that can be exchanged between solvers
SizeManagerStats: Statistics for clause size management
SmoothedLbdStats: Statistics for smoothed LBD tracking
SmoothedLbdTracker: Smoothed LBD tracker
Solver: CDCL SAT Solver
SolverConfig: Solver configuration
SolverStats: Statistics for the solver
StabilizationConfig: Stabilization strategy configuration
StabilizationManager: Stabilization manager
StabilizationStats: Statistics for stabilization
StatsAggregator: Statistics aggregator for multiple solver runs
StatsDashboard: Comprehensive statistics dashboard
SubsumptionChecker: Subsumption checker for learned clauses
SubsumptionStats: Statistics for subsumption checking
SymmetryBreaker: Symmetry breaker
SymmetryGroup: Symmetry group representation
TargetPhaseSelector: Target-based phase selection manager
TargetPhaseStats: Statistics for target phase selection
Trail: The assignment trail
TrailSavingManager: Trail saving manager
TrailSavingStats: Statistics for trail saving
TuningPerformanceMetrics: Performance metrics for tuning evaluation
UipAnalysisResult: Result of UIP analysis.
UipAnalyzer: UIP conflict analyzer.
UipConfig: Configuration for UIP conflict analysis.
UipStats: Statistics for UIP analysis.
UnsatCore: UNSAT core extractor
VMTF: Variable Move-To-Front (VMTF) branching heuristic
Var: A variable in the SAT formula
VariableActivityManager: Variable activity manager
VariableIncidenceGraph: Variable Incidence Graph (VIG).
Vivification: Clause vivification manager
VivificationStats: Statistics for vivification
VmtfBumpQueue: VMTF bump queue
VmtfBumpStats: Statistics for VMTF bump queue
VmtfStats: Statistics for VMTF
XorClause: XOR clause for propagation with watched literals
XorClauseId: ID for an XOR clause within the propagator
XorConstraint: Represents an XOR constraint: x1 ⊕ x2 ⊕ … ⊕ xn = rhs
XorDetector: XOR clause detector
XorManager: XOR constraint manager with Gaussian elimination
XorPropagator: XOR propagator with watched literal scheme
XorPropagatorStats: Statistics for XOR propagator
XorStrengthening: XOR strengthening: eliminate variables that appear in exactly two XOR constraints
XorSubsumption: XOR subsumption checker

Enums§

BackboneAlgorithm: Backbone computation algorithm
BacktrackDecision: Backtracking decision.
ClauseTier: Clause tier for tiered database management
ConfigPreset: Preset categories for different problem types
CubeResult: Result of solving cubes.
CubeSplittingStrategy: Strategy for cube generation.
DimacsError: Error type for DIMACS parsing
EnumerationResult: Result of enumeration
ExtensionType: Types of extension variable definitions
GateType: Type of logical gate
GpuBackend: GPU backend selection
GpuError: Error type for GPU operations
GpuRecommendation: GPU usage recommendation
HbrResult: Result of hyper-binary resolution
LBool: Boolean value or undefined
LocalSearchResult: Result of local search
LookaheadHeuristic: Look-ahead branching heuristic type
MemoryAction: Recommended memory action
PhaseMode: Phase selection mode
PropagateResult: Result of propagation
Reason: Reason for an assignment
RephasingStrategy: Rephasing strategy
RestartStrategy: Restart strategy
SearchMode: Search mode for stabilization
SizeAdjustmentStrategy: Strategy for adjusting clause size limit
SizeClass: Size class for memory pooling
SolverResult: Result of SAT solving
SubsumptionResult: Result of subsumption check.
SymmetryBreakingMethod: Symmetry breaking method
TheoryCheckResult: Result from a theory check
TuningStrategy: Tuning strategy
UipStrategy: UIP strategy selection.
XorAddResult: Result of adding an XOR constraint

Traits§

GpuSolverAccelerator: Trait for GPU-accelerated SAT solver operations
TheoryCallback: Callback trait for theory solvers The CDCL(T) solver implements this to receive theory callbacks

Type Aliases§

Model: A model (satisfying assignment) represented as a vector of literals
Weight: Weight type for weighted MaxSAT

Crate oxiz_sat

Crate oxiz_sat Copy item path

§Examples

§Basic SAT Solving

§Solving with Assumptions

Re-exports§

Modules§

Macros§

Structs§

Enums§

Traits§

Type Aliases§

Crate oxiz_sat