Module sat 

The sat module implements the SAT solver, which determines the satisfiability of Boolean formulas.

Modules

assignment

Represents the assignment of variables in a SAT solver. This module defines the Assignment trait and its implementations for managing variable states in the SAT solvers.

cdcl

The cdcl module implements the Conflict-Driven Clause Learning (CDCL) algorithm for SAT solving. Implements the core Conflict-Driven Clause Learning (CDCL) SAT solver.

clause

The cnf module provides functionality for working with Conjunctive Normal Form (CNF) representations. Contains details of a clause, a fundamental component in SAT solvers.

clause_management

The clause_management module handles the management of clauses in a SAT solver. This module defines strategies for managing the clause database in a SAT solver.

clause_storage

The clause_storage module provides storage and retrieval mechanisms for clauses in a SAT solver. Defines how literals are stored within a clause.

cnf

The cnf module provides functionality for parsing and manipulating CNF (Conjunctive Normal Form) formulas. Defines the Conjunctive Normal Form (CNF) representation for SAT formulas.

conflict_analysis

The conflict_analysis module implements conflict analysis techniques used in SAT solvers. Defines functions and structures related to conflict analysis in a SAT solver.

dimacs

The dimacs module handles parsing DIMACS format files, which are commonly used for representing SAT problems. A parser for the DIMACS CNF (Conjunctive Normal Form) file format.

dpll

The dpll module implements the DPLL (Davis-Putnam-Logemann-Loveland) algorithm for SAT solving. Defines the DPLL (Davis-Putnam-Logemann-Loveland) SAT solver.

expr

The expr module provides functionality for working with Boolean expressions, including parsing and manipulation. Defines an arbitrary boolean expression type and functions for its manipulation.

literal

The heuristic module implements various heuristics for variable selection and decision-making in SAT solvers. Defines literals, the fundamental building blocks of clauses in SAT formulas.

preprocessing

The literal module provides functionality for working with literals in SAT problems. Defines traits and implementations for preprocessing SAT formulas.

propagation

The propagation module implements unit propagation and other propagation techniques used in SAT solvers. Defines traits and implementations for literal propagation in a SAT solver.

restarter

The restarter module implements restarts in SAT solvers, which can help escape from difficult regions of the search space. Defines restart strategies for SAT solvers.

solver

The solver module provides the main interface for solving SAT problems using various algorithms and techniques. Defines common types and traits for SAT solvers, including solver configurations, solution representation, and statistics.

trail

The trail module implements a trail data structure used in SAT solvers to keep track of variable assignments and decisions.

variable_selection

The variable_selection module implements various strategies for selecting variables during the solving process. Defines variable selection strategies (decision heuristics) for SAT solvers.