Class: TRuby::SMT::SATSolver

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

Overview

SAT Solver (DPLL Algorithm)

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize ⇒ SATSolver

Returns a new instance of SATSolver.



528
529
530
531
 
# File 'lib/t_ruby/smt_solver.rb', line 528

def initialize
  @assignments = {}
  @conflicts = []
end

Instance Attribute Details

#assignments ⇒ Object (readonly)

Returns the value of attribute assignments.



526
527
528
 
# File 'lib/t_ruby/smt_solver.rb', line 526

def assignments
  @assignments
end

#conflicts ⇒ Object (readonly)

Returns the value of attribute conflicts.



526
527
528
 
# File 'lib/t_ruby/smt_solver.rb', line 526

def conflicts
  @conflicts
end

Instance Method Details

#solve(cnf) ⇒ Object

Solve CNF formula



534
535
536
537
538
539
 
# File 'lib/t_ruby/smt_solver.rb', line 534

def solve(cnf)
  @assignments = {}
  @conflicts = []

  dpll(cnf.dup, {})
end