Class: DpllSolver::Util

Inherits:
Object
  • Object
show all
Defined in:
lib/dpll_solver.rb

Constant Summary collapse

@@grammar = 
DpllSolver::Parsers::Grammar.new
@@transformer = 
DpllSolver::Parsers::Transformer.new

Class Method Summary collapse

Class Method Details

.contradiction?(str) ⇒ Boolean

Returns:

  • (Boolean) 


49
50
51
 
# File 'lib/dpll_solver.rb', line 49

def self.contradiction?(str)
  !self.SAT?(str)
end

.dimacs_SAT?(file) ⇒ Boolean

Returns:

  • (Boolean) 


39
40
41
42
 
# 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) ⇒ Object 



34
35
36
37
 
# File 'lib/dpll_solver.rb', line 34

def self.dimacs_to_clause(file)
  parser = DpllSolver::Parsers::DimacsParser.new(file)
  parser.clauseset
end

.SAT?(str) ⇒ Boolean

Returns:

  • (Boolean) 


44
45
46
47
 
# 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

.tautology?(str) ⇒ Boolean

Returns:

  • (Boolean) 


53
54
55
56
57
58
59
 
# 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) ⇒ Object 



29
30
31
32
 
# 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) ⇒ Object 



24
25
26
27
 
# File 'lib/dpll_solver.rb', line 24

def self.to_cnf(str)
  formula = @@grammar.parse(str)
  @@transformer.apply(formula).simplify().cnf()
end