Implementation of SAT solver. More...
Include dependency graph for sat.h:
This graph shows which files directly or indirectly include this file:
Go to the source code of this file.
Classes | |
| class | gymbosat::Expr |
| Base class for representing logical expressions. More... | |
| class | gymbosat::Var |
| Class representing a variable in a logical expression. More... | |
| class | gymbosat::And |
| Class representing the logical AND operation. More... | |
| class | gymbosat::Or |
| Class representing the logical OR operation. More... | |
| class | gymbosat::Not |
| Class representing the logical NOT operation. More... | |
| class | gymbosat::Const |
| Class representing a boolean constant in a logical expression. More... | |
Namespaces | |
| gymbosat | |
Enumerations | |
| enum | gymbosat::OpCode { gymbosat::VAR , gymbosat::AND , gymbosat::OR , gymbosat::NOT , gymbosat::CONST } |
| Enum representing different logical operation codes. More... | |
| enum | gymbosat::Polarity { gymbosat::Positive , gymbosat::Negative , gymbosat::Mixed } |
| Enum representing different polarities in logical expressions. More... | |
Functions | |
| std::shared_ptr< Expr > | gymbosat::cnf (std::shared_ptr< Expr > expr) |
| Convert a logical expression to conjunctive normal form (CNF). More... | |
| std::shared_ptr< Expr > | gymbosat::literalElimination (std::shared_ptr< Expr > expr, std::unordered_map< std::string, bool > &assignments_map) |
| Eliminate literals in a logical expression based on assignments. More... | |
| std::vector< std::pair< std::string, bool > > | gymbosat::allUnitClauses (std::shared_ptr< Expr > expr) |
| Extract all unit clauses from a logical expression. More... | |
| std::shared_ptr< Expr > | gymbosat::unitPropagation (std::shared_ptr< Expr > expr, std::unordered_map< std::string, bool > &assignments_map) |
| Perform unit propagation on a logical expression based on assignments. More... | |
| bool | gymbosat::satisfiableDPLL (std::shared_ptr< Expr > expr, std::unordered_map< std::string, bool > &assignments_map) |
| Check satisfiability of a logical expression using the DPLL algorithm. More... | |
| std::shared_ptr< Expr > | gymbosat::sym2expr (gymbo::Sym *sym, std::unordered_map< std::string, gymbo::Sym * > &unique_sym_map) |
| Convert a symbolic expression to a logical expression. More... | |
| std::shared_ptr< Expr > | gymbosat::pathconstraints2expr (std::vector< gymbo::Sym > &constraints, std::unordered_map< std::string, gymbo::Sym * > &unique_sym_map) |
| Convert a vector of symbolic path constraints to a logical expression. More... | |
Detailed Description
Implementation of SAT solver.
