Evaluate all possible interpretations in OCaml

Question

I need to evaluate whether two formulas are equivalent or not. Here, I use a simple definition of formula, which is a prefix formula.

For example, And(Atom("b"), True) means b and true, while And(Atom("b"), Or(Atom("c"), Not(Atom("c")))) means (b and (c or not c))

My idea is simple, get all atoms, apply every combination (for my cases, I will have 4 combination, which are true-true, true-false, false-true, and false-false). The thing is, I don't know how to create these combinations.

For now, I have known how to get all involving atoms, so in case of there are 5 atoms, I should create 32 combinations. How to do it in OCaml?

score 4 · Accepted Answer · answered Mar 08 '11 at 14:00

Ok, so what you need is a function combinations n that will produce all the booleans combinations of length n; let's represent them as lists of lists of booleans (i.e. a single assignment of variables will be a list of booleans). Then this function would do the job:

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

There is only one empty combination of length 0 and for n > 0 we produce combinations of n-1 and prefix them with false and with true to produce all possible combinations of length n.

You could write a function to print such combinations, let's say:

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)

and then test it all with:

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)

to get:

> ./combinations 3
combinations(3) = [TTT][TTF][TFT][TFF][FTT][FTF][FFT][FFF]

this is incredible! could you explain to me the meaning of @ there? is it the same as List.append? and one more, what's the meaning of fun l -> false::l ? — zfm, Mar 08 '11 at 14:21
@zfm: sure, `@` is indeed a shortcut for `List.append` (see http://caml.inria.fr/pub/docs/manual-ocaml/libref/Pervasives.html). `fun l -> false::l` is an anonymous function. You could write `let ff l = false::l in List.map ff rest` but instead you can "inline" the function as I did above. Hope that helps. — akoprowski, Mar 08 '11 at 15:12
If you cannot hold all the combinations in memory, check out a post I made awhile ago (with some ocaml) for creating an index of the combination in lexicographical order, http://stackoverflow.com/questions/127704/algorithm-to-return-all-combinations-of-k-elements-from-n/127856#127856 — nlucaroni, Mar 08 '11 at 15:23

lambdapower · Answer 2 · 2011-03-09T09:19:49.810

If you think of a list of booleans as a list of bits of fixed length, there is a very simple solution: Count!

If you want to have all combinations of 4 booleans, count from 0 to 15 (2^4 - 1) -- then interpret each bit as one of the booleans. For simplicity I'll use a for-loop, but you can also do it with a recursion:

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

Of course you can make the body of the loop more general so that it e.g. creates a list/array of booleans depending on the size given above etc.; The point is that you can solve this problem by enumerating all values you are searching for. If this is the case, compute all integers up to your problem size. Write a function that generates a value of your original problem from an integer. Put it all together.

This method has the advantage that you do not need to first create all combinations, before starting your computation. For large problems this might well save you. For rather small size=16 you will already need 65535 * sizeof(type) memory -- and this is growing exponentially with the size! The above solution will require only a constant amount of memory of sizeof(type).

And for science's sake: Your problem is NP-complete, so if you want the exact solution, it will take exponential time.

I agree that this problem is **NP-complete**, however since the size will not very big (less than 10 variables) for any formulas given, I don't really care about the space consuming here. — zfm, Mar 09 '11 at 20:47

Evaluate all possible interpretations in OCaml

2 Answers2