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