Module: PropLogic::BruteForceSatSolver

Defined in:
lib/prop_logic/brute_force_sat_solver.rb

Class Method Summary collapse

Class Method Details

.call(term) ⇒ Object 



4
5
6
7
8
9
10
11
12
13
14
15
16
17
 
# File 'lib/prop_logic/brute_force_sat_solver.rb', line 4

def call(term)
  # obvious value
  return True if term == True
  variables = term.variables
  PropLogic.all_combination(variables) do |trues|
    falses = variables - trues
    next unless term.assign(trues, falses).reduce == True
    # SAT
    negated_falses = falses.map(&:not)
    return PropLogic.all_and(*trues, *negated_falses)
  end
  # UNSAT
  false
end