module Arcteryx

Constants

SAT
UNSAT

Public Class Methods

DPLL(cnf) click to toggle source

# 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 ) click to toggle source

# 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

Private Instance Methods

DPLL(cnf) click to toggle source

# 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 ) click to toggle source

# 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