Module: Arcteryx

Defined in:
lib/arcteryx/cnf.rb,
lib/arcteryx/arcteryx.rb

Defined Under Namespace

Classes: CNF

Constant Summary collapse

SAT = 
true
UNSAT = 
false

Class Method Summary collapse

Class Method Details

.DPLL(cnf) ⇒ Object 



6
7
8
9
10
11
12
13
 
# File 'lib/arcteryx/arcteryx.rb', line 6

def DPLL(cnf)
  if cnf.empty? then return SAT end
  cnf.unit_propagation
  if cnf.exist_empty_clause? then return UNSAT end
  x = cnf.choose_variable
  dup_cnf = cnf.deep_dup
  return DPLL(cnf.append x) || DPLL(dup_cnf.append -1*x)
end

.solve(input_file, output_file = nil) ⇒ Object 



15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
 
# File 'lib/arcteryx/arcteryx.rb', line 15

def solve( input_file, output_file = nil )
  cnf = Arcteryx::CNF.new
  cnf.parse(input_file)
  case DPLL(cnf)
  when SAT
    if output_file
      File.open(output_file,"w") do |f|
        f.write("SAT\n"+cnf.result)
      end
    else
      puts "SAT"
      puts cnf.result
    end
  when UNSAT
    if output_file
      File.open(output_file,"w") do |f|
        f.write("UNSAT")
      end
    else
      puts "UNSAT"
    end
  end
end