Table of Contents - dpll_solver-0.0.1 Documentation
Classes and Modules
- AtomicFormula
- BinaryFormula
- DpllSolver
- DpllSolver::DPLL
- DpllSolver::Formulas
- DpllSolver::Formulas::And
- DpllSolver::Formulas::Clause
- DpllSolver::Formulas::Falsum
- DpllSolver::Formulas::Literal
- DpllSolver::Formulas::Not
- DpllSolver::Formulas::Or
- DpllSolver::Formulas::Variable
- DpllSolver::Formulas::Verum
- DpllSolver::Heuristics
- DpllSolver::Heuristics::MostFrequentLiteral
- DpllSolver::Parsers
- DpllSolver::Parsers::DimacsParser
- DpllSolver::Parsers::Grammar
- DpllSolver::Parsers::Parser
- DpllSolver::Parsers::Transformer
- DpllSolver::Util
- Object
Methods
- ::SAT? — DpllSolver::Util
- ::choose_literal — DpllSolver::Heuristics::MostFrequentLiteral
- ::contradiction? — DpllSolver::Util
- ::dimacs_SAT? — DpllSolver::Util
- ::dimacs_to_clause — DpllSolver::Util
- ::falsum? — DpllSolver::Formulas::Falsum
- ::falsum? — DpllSolver::Formulas::Verum
- ::formula_to_clause — DpllSolver::Parsers::Parser
- ::new — DpllSolver::DPLL
- ::new — BinaryFormula
- ::new — DpllSolver::Formulas::Clause
- ::new — DpllSolver::Formulas::Literal
- ::new — DpllSolver::Formulas::Not
- ::new — DpllSolver::Formulas::Variable
- ::new — DpllSolver::Parsers::DimacsParser
- ::tautology? — DpllSolver::Util
- ::to_clause — DpllSolver::Util
- ::to_cnf — DpllSolver::Util
- ::to_s — DpllSolver::Formulas::Falsum
- ::to_s — DpllSolver::Formulas::Verum
- ::verum? — DpllSolver::Formulas::Falsum
- ::verum? — DpllSolver::Formulas::Verum
- #== — BinaryFormula
- #== — DpllSolver::Formulas::Clause
- #== — DpllSolver::Formulas::Literal
- #== — DpllSolver::Formulas::Not
- #== — DpllSolver::Formulas::Variable
- #== — AtomicFormula
- #add — DpllSolver::Formulas::Clause
- #and? — DpllSolver::Formulas::And
- #and? — DpllSolver::Formulas::Not
- #and? — DpllSolver::Formulas::Or
- #and? — AtomicFormula
- #apply_DeMorgan — DpllSolver::Formulas::Not
- #apply_dpll — DpllSolver::DPLL
- #atomic_formula? — BinaryFormula
- #atomic_formula? — DpllSolver::Formulas::Not
- #atomic_formula? — AtomicFormula
- #clause? — DpllSolver::Formulas::And
- #clause? — DpllSolver::Formulas::Not
- #clause? — DpllSolver::Formulas::Or
- #clause? — AtomicFormula
- #cnf — DpllSolver::Formulas::And
- #cnf — DpllSolver::Formulas::Not
- #cnf — DpllSolver::Formulas::Or
- #cnf — AtomicFormula
- #cnf? — DpllSolver::Formulas::And
- #cnf? — DpllSolver::Formulas::Not
- #cnf? — DpllSolver::Formulas::Or
- #cnf? — AtomicFormula
- #contains_empty_clause? — DpllSolver::DPLL
- #create_literal — DpllSolver::Parsers::DimacsParser
- #delete — DpllSolver::Formulas::Clause
- #dnf — AtomicFormula
- #dnf? — BinaryFormula
- #dnf? — DpllSolver::Formulas::Not
- #dnf? — AtomicFormula
- #empty? — DpllSolver::Formulas::Clause
- #eql? — BinaryFormula
- #eql? — DpllSolver::Formulas::Clause
- #eql? — DpllSolver::Formulas::Literal
- #eql? — DpllSolver::Formulas::Not
- #eql? — DpllSolver::Formulas::Variable
- #falsum? — DpllSolver::Formulas::And
- #falsum? — DpllSolver::Formulas::Not
- #falsum? — DpllSolver::Formulas::Or
- #falsum? — DpllSolver::Formulas::Variable
- #get_unit_clause_literal — DpllSolver::DPLL
- #get_unit_literal — DpllSolver::Formulas::Clause
- #include? — DpllSolver::Formulas::Clause
- #literal? — BinaryFormula
- #literal? — DpllSolver::Formulas::Not
- #literal? — AtomicFormula
- #min_term? — DpllSolver::Formulas::And
- #min_term? — DpllSolver::Formulas::Not
- #min_term? — DpllSolver::Formulas::Or
- #min_term? — AtomicFormula
- #negate — DpllSolver::Formulas::Literal
- #nnf — BinaryFormula
- #nnf — DpllSolver::Formulas::Not
- #nnf — AtomicFormula
- #nnf? — BinaryFormula
- #nnf? — DpllSolver::Formulas::Not
- #nnf? — AtomicFormula
- #not? — DpllSolver::Formulas::And
- #not? — DpllSolver::Formulas::Not
- #not? — DpllSolver::Formulas::Or
- #not? — AtomicFormula
- #or? — DpllSolver::Formulas::And
- #or? — DpllSolver::Formulas::Not
- #or? — DpllSolver::Formulas::Or
- #or? — AtomicFormula
- #parse — DpllSolver::Parsers::DimacsParser
- #require_all — Object
- #simplify — DpllSolver::Formulas::And
- #simplify — DpllSolver::Formulas::Not
- #simplify — DpllSolver::Formulas::Or
- #simplify — AtomicFormula
- #to_s — DpllSolver::Formulas::And
- #to_s — DpllSolver::Formulas::Clause
- #to_s — DpllSolver::Formulas::Literal
- #to_s — DpllSolver::Formulas::Not
- #to_s — DpllSolver::Formulas::Or
- #union — DpllSolver::Formulas::Clause
- #union_unit_clause — DpllSolver::DPLL
- #unit? — DpllSolver::Formulas::Clause
- #unit_propagation — DpllSolver::DPLL
- #variable? — DpllSolver::Formulas::And
- #variable? — DpllSolver::Formulas::Not
- #variable? — DpllSolver::Formulas::Or
- #variable? — DpllSolver::Formulas::Variable
- #variable? — AtomicFormula
- #verum? — DpllSolver::Formulas::And
- #verum? — DpllSolver::Formulas::Not
- #verum? — DpllSolver::Formulas::Or
- #verum? — DpllSolver::Formulas::Variable