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