Оцените все возможные интерпретации в OCaml - PullRequest
Новая
       30

Оцените все возможные интерпретации в OCaml

3 голосов
/ 08 марта 2011

Мне нужно оценить, эквивалентны ли две формулы или нет.Здесь я использую простое определение формулы, которая является префиксной формулой.

Например, And(Atom("b"), True) означает b and true, а And(Atom("b"), Or(Atom("c"), Not(Atom("c")))) означает (b and (c or not c))

Моя идея заключается в том,просто, получить все атомы, применить каждую комбинацию (для моих случаев у меня будет 4 комбинации: истина-истина, истина-ложь, ложь-истина и ложь-ложь).Дело в том, что я не знаю, как создавать эти комбинации.

На данный момент я знаю, как получить все участвующие атомы, поэтому в случае 5 атомов я должен создать 32 комбинации.Как это сделать в OCaml?

Ответы [ 2 ]

4 голосов
/ 08 марта 2011

Хорошо, так что вам нужна функция combinations n, которая будет генерировать все логические комбинации длины n;давайте представим их как списки списков логических значений (т. е. одно назначение переменных будет списком логических значений).Тогда эта функция выполнит свою работу: 

let rec combinations = function
  | 0 -> [[]]
  | n ->
    let rest = combinations (n - 1) in
    let comb_f = List.map (fun l -> false::l) rest in
    let comb_t = List.map (fun l -> true::l) rest in
    comb_t @ comb_f

Существует только одна пустая комбинация длины 0, а для n > 0 мы создаем комбинации n-1 и добавляем их к false и true для получения всех возможных комбинаций длины n.

Вы можете написать функцию для печати таких комбинаций, скажем: 

let rec combinations_to_string = function
  | [] -> ""
  | x::xs ->
      let rec bools_to_str = function
        | [] -> ""
        | b::bs -> Printf.sprintf "%s%s" (if b then "T" else "F") (bools_to_str bs)
      in
      Printf.sprintf "[%s]%s" (bools_to_str x) (combinations_to_string xs)

, а затем протестировать все с помощью: 

let _ =
  let n = int_of_string Sys.argv.(1) in
  let combs = combinations n in
  Printf.eprintf "combinations(%d) = %s\n" n (combinations_to_string combs)

чтобы получить: 

> ./combinations 3
combinations(3) = [TTT][TTF][TFT][TFF][FTT][FTF][FFT][FFF]
1 голос
/ 09 марта 2011

Если вы рассматриваете список логических значений как список битов фиксированной длины, есть очень простое решение: Count!

Если вы хотите иметь все комбинации из 4 логических значений, считайте от 0 до 15 (2 ^ 4 - 1) - затем интерпретируйте каждый бит как один из логических значений. Для простоты я буду использовать цикл for, но вы также можете сделать это с помощью рекурсии: 

let size = 4 in
(* '1 lsl size' computes 2^size *)
for i = 0 to (1 lsl size) - 1 do
   (* from: is the least significant bit '1'? *)
   let b0 = 1 = ((i / 1) mod 2) in
   let b1 = 1 = ((i / 2) mod 2) in
   let b2 = 1 = ((i / 4) mod 2) in
   (* to: is the most significant bit '1'? *)
   let b3 = 1 = ((i / 8) mod 2) in
   (* do your thing *)
   compute b0 b1 b2 b3
done

Конечно, вы можете сделать тело цикла более общим, например: создает список / массив логических значений в зависимости от размера, указанного выше и т. д .; Дело в том, что вы можете решить эту проблему, перечислив все значения, которые вы ищете. Если это так, вычислите все целые числа до размера вашей проблемы. Напишите функцию, которая генерирует значение вашей исходной задачи из целого числа. Соберите все это вместе.

Этот метод имеет то преимущество, что вам не необходимо сначала создавать все комбинации, прежде чем начинать вычисления. При больших проблемах это может вас спасти. Для довольно маленького размера = 16 вам уже понадобится 65535 * sizeof (type) memory - и это растет экспоненциально с размером! Приведенное выше решение потребует только постоянного объема памяти sizeof (тип) .

И ради науки: ваша проблема NP-полная , поэтому, если вам нужно точное решение, это займет экспоненциальное время.

...