sat_solver/sat/
mod.rs

1#![warn(clippy::all, clippy::pedantic, clippy::nursery, clippy::cargo)]
2
3/// Represents the assignment of variables in a SAT solver.
4pub mod assignment;
5
6/// The `cdcl` module implements the Conflict-Driven Clause Learning (CDCL) algorithm for SAT solving.
7pub mod cdcl;
8
9/// The `cnf` module provides functionality for working with Conjunctive Normal Form (CNF) representations.
10pub mod clause;
11
12/// The `clause_management` module handles the management of clauses in a SAT solver.
13pub mod clause_management;
14
15/// The `clause_storage` module provides storage and retrieval mechanisms for clauses in a SAT solver.
16pub mod clause_storage;
17
18/// The `cnf` module provides functionality for parsing and manipulating CNF (Conjunctive Normal Form) formulas.
19pub mod cnf;
20
21/// The `conflict_analysis` module implements conflict analysis techniques used in SAT solvers.
22pub mod conflict_analysis;
23
24/// The `dimacs` module handles parsing DIMACS format files, which are commonly used for representing SAT problems.
25pub mod dimacs;
26
27/// The `dpll` module implements the DPLL (Davis-Putnam-Logemann-Loveland) algorithm for SAT solving.
28pub mod dpll;
29
30/// The `expr` module provides functionality for working with Boolean expressions, including parsing and manipulation.
31pub mod expr;
32
33/// The `heuristic` module implements various heuristics for variable selection and decision-making in SAT solvers.
34pub mod literal;
35
36/// The `literal` module provides functionality for working with literals in SAT problems.
37pub mod preprocessing;
38
39/// The `propagation` module implements unit propagation and other propagation techniques used in SAT solvers.
40pub mod propagation;
41
42/// The `restarter` module implements restarts in SAT solvers, which can help escape from difficult regions of the search space.
43pub mod restarter;
44
45/// The `solver` module provides the main interface for solving SAT problems using various algorithms and techniques.
46pub mod solver;
47
48/// The `trail` module implements a trail data structure used in SAT solvers to keep track of variable assignments and decisions.
49pub mod trail;
50
51/// The `variable_selection` module implements various strategies for selecting variables during the solving process.
52pub mod variable_selection;
sat_solver/sat/mod.rs

sat_solver/sat/
mod.rs
