Class: Arcteryx::CNF

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

Instance Method Summary collapse

Constructor Details

#initialize(formula = [], truth = {}) ⇒ CNF

Returns a new instance of CNF.



3
4
5
6
 
# File 'lib/arcteryx/cnf.rb', line 3

def initialize(formula=[],truth={})
  @formula = formula
  @truth_assignment = truth
end

Instance Method Details

#append(l) ⇒ Object 



57
58
59
60
 
# File 'lib/arcteryx/cnf.rb', line 57

def append l
  @formula.append [l] if l
  return self
end

#choose_variable ⇒ Object 



52
53
54
55
 
# 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 ⇒ Object 



62
63
64
65
66
 
# 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? ⇒ Boolean

Returns:

  • (Boolean) 


38
39
40
 
# File 'lib/arcteryx/cnf.rb', line 38

def empty?
  @formula.empty?
end

#exist_empty_clause? ⇒ Boolean

Returns:

  • (Boolean) 


47
48
49
50
 
# 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 ⇒ Object 



42
43
44
45
 
# 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) ⇒ Object 



8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
 
# 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 ⇒ Object 



68
69
70
71
72
 
# 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) ⇒ Object 



31
32
33
34
35
36
 
# 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 ⇒ Object 



24
25
26
27
28
29
 
# 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