class DpllSolver::DPLL
Attributes
heuristics[RW]
Public Class Methods
new(heuristics)
click to toggle source
# File lib/dpll_solver.rb, line 64 def initialize(heuristics) @heuristics = heuristics end
Public Instance Methods
apply_dpll(clauseset)
click to toggle source
# File lib/dpll_solver.rb, line 68 def apply_dpll(clauseset) literal = get_unit_clause_literal(clauseset) while literal do clauseset = unit_propagation(clauseset, literal) literal = get_unit_clause_literal(clauseset) end if clauseset.empty? return true elsif contains_empty_clause?(clauseset) return false end literal = @heuristics.choose_literal(clauseset) return apply_dpll(union_unit_clause(clauseset, literal)) || apply_dpll(union_unit_clause(clauseset, literal.negate())) end
contains_empty_clause?(clauseset)
click to toggle source
# File lib/dpll_solver.rb, line 83 def contains_empty_clause?(clauseset) clauseset.each do |clause| return true if clause.empty? end return false end
get_unit_clause_literal(clauseset)
click to toggle source
# File lib/dpll_solver.rb, line 90 def get_unit_clause_literal(clauseset) clauseset.each do |clause| if clause.unit? return clause.literals.first end end return false end
union_unit_clause(clauseset, literal)
click to toggle source
# File lib/dpll_solver.rb, line 111 def union_unit_clause(clauseset, literal) clauseset.dup.add(DpllSolver::Formulas::Clause.new(literal)) end
unit_propagation(clauseset, literal)
click to toggle source
# File lib/dpll_solver.rb, line 99 def unit_propagation(clauseset, literal) result = Set.new clauseset.each do |clause| if clause.include?(literal.negate()) result.add(clause.delete(literal.negate())) elsif !clause.include?(literal) result.add(clause) end end result end