class DpllSolver::Util

Public Class Methods

SAT?(str) click to toggle source
# File lib/dpll_solver.rb, line 44
def self.SAT?(str)
  solver = DPLL.new(DpllSolver::Heuristics::MostFrequentLiteral)
  solver.apply_dpll(self.to_clause(str))
end
contradiction?(str) click to toggle source
# File lib/dpll_solver.rb, line 49
def self.contradiction?(str)
  !self.SAT?(str)
end
dimacs_SAT?(file) click to toggle source
# File lib/dpll_solver.rb, line 39
def self.dimacs_SAT?(file)
  solver = DPLL.new(DpllSolver::Heuristics::MostFrequentLiteral)
  solver.apply_dpll(self.dimacs_to_clause(file))
end
dimacs_to_clause(file) click to toggle source
# File lib/dpll_solver.rb, line 34
def self.dimacs_to_clause(file)
  parser = DpllSolver::Parsers::DimacsParser.new(file)
  parser.clauseset
end
tautology?(str) click to toggle source
# File lib/dpll_solver.rb, line 53
def self.tautology?(str)
  formula = @@grammar.parse(str)
  #negate formula
  clause = DpllSolver::Parsers::Parser.formula_to_clause(DpllSolver::Formulas::Not.new(@@transformer.apply(formula)))
  solver = DPLL.new(DpllSolver::Heuristics::MostFrequentLiteral)
  !solver.apply_dpll(clause)
end
to_clause(str) click to toggle source
# File lib/dpll_solver.rb, line 29
def self.to_clause(str)
  formula = @@grammar.parse(str)
  DpllSolver::Parsers::Parser.formula_to_clause(@@transformer.apply(formula))
end
to_cnf(str) click to toggle source
# File lib/dpll_solver.rb, line 24
def self.to_cnf(str)
  formula = @@grammar.parse(str)
  @@transformer.apply(formula).simplify().cnf()
end