Gymbo

Classes | Namespaces | Enumerations | Functions
sat.h File Reference

Implementation of SAT solver. More...

`#include <memory>`
`#include "type.h"`
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.

Author
  Hideaki Takahashi