class Arcteryx::CNF
Public Class Methods
new(formula=[],truth={})
click to toggle source
# File lib/arcteryx/cnf.rb, line 3 def initialize(formula=[],truth={}) @formula = formula @truth_assignment = truth end
Public Instance Methods
append(l)
click to toggle source
# File lib/arcteryx/cnf.rb, line 57 def append l @formula.append [l] if l return self end
choose_variable()
click to toggle source
# File lib/arcteryx/cnf.rb, line 52 def choose_variable @truth_assignment.map{|key,value| if value == nil then return key.to_s.to_i end} return false end
deep_dup()
click to toggle source
# File lib/arcteryx/cnf.rb, line 62 def deep_dup tmp_formula = Marshal.load(Marshal.dump(@formula)) tmp_truth = Marshal.load(Marshal.dump(@truth_assignment)) CNF.new(tmp_formula,tmp_truth) end
empty?()
click to toggle source
# File lib/arcteryx/cnf.rb, line 38 def empty? @formula.empty? end
exist_empty_clause?()
click to toggle source
# File lib/arcteryx/cnf.rb, line 47 def exist_empty_clause? @formula.map{|cls| if cls.empty? then return true end} return false end
find_unit_clause()
click to toggle source
# File lib/arcteryx/cnf.rb, line 42 def find_unit_clause @formula.map{|cls| if cls.size == 1 then return cls.first end} return false end
parse(file_path)
click to toggle source
# File lib/arcteryx/cnf.rb, line 8 def parse(file_path) header = ""; clauses = []; File.open(file_path,"r") do |f| header = f.readline clauses = f.readlines end header.split[2].to_i.times do |i| @truth_assignment["#{i+1}".to_sym] = nil end clauses.each do |e| clause = e.split.map{|i| i.to_i} clause.pop @formula.append clause end end
result()
click to toggle source
# File lib/arcteryx/cnf.rb, line 68 def result str = "" @truth_assignment.map{|key,value| unless value then str<<"-" end; str<<key.to_s+" "} return str << "0" end
simplify(l)
click to toggle source
# File lib/arcteryx/cnf.rb, line 31 def simplify(l) @formula.delete_if do |cls| cls.include?(l) end @formula.map{|cls| if cls.include?(-1*l) then cls.delete(-1*l) end} end
unit_propagation()
click to toggle source
# File lib/arcteryx/cnf.rb, line 24 def unit_propagation while !self.exist_empty_clause? and l = self.find_unit_clause @truth_assignment["#{l.abs}".to_sym] = l > 0 self.simplify(l) end end