What is the semantics of the Qbf.result type?

[AbdallahS]

Consider the following formulas f1 = E x1 x2 x3 (x1 | -x2 | -x3) & (-x1 | x2 | x3) and f2 = E x1 x2 x3 (x1 | x2 | x3) & (-x1 | -x2 | -x3). In both cases, running Qbf.solve with Quantor.solver returns SAT with the following assignment: mu: x1=undef, x2=false, x3=false.

This is very strange: in both cases, if I assign x2 and x3 to false, the formulas don't simplify completely. In one case, the application of the partial assignment mu gives f1/mu = E x1, (-x1) and in the second case we get f2/mu = E x1, (x1). In other words, the partial assignment insufficient to prove/confirm that the formula is SAT, it is not a witness. Additionally, even if we complete the partial assignment by assigning a default value to the undefined variables, we can't actually know in advance what would be the correct default (since it would be different for f1 and for f2).

If the returned partial assignment is not a witness and cannot be easily extended to a witness, why not simply returning all variables as undef (or even simpler, not returning any partial assignment)? If the current situation is not a bug, how can we characterize the return partial assignment?

Example code:

open Printf

let literal (p, i) = if p then Qbf.Lit.make i else Qbf.Lit.neg (Qbf.Lit.make i)
let vars = [1;2;3]
let block1 = List.map Qbf.Lit.make vars
let clause1 = List.map literal [(true, 1); (false,2); (false,3)]
let clause2 = List.map literal [(false,1); (true, 2); (true, 3)]
let clause3 = List.map literal [(true, 1); (true, 2); (true, 3)]
let clause4 = List.map literal [(false,1); (false,2); (false,3)]
let formula = Qbf.QCNF.exists block1 (Qbf.QCNF.prop [clause1; clause2])
let formula = Qbf.QCNF.exists block1 (Qbf.QCNF.prop [clause3; clause4])

let assignment a var =
  let l = Qbf.Lit.make var in
  match a l with
  | Qbf.True  -> Either.Right (true,  var)
  | Qbf.False -> Either.Right (false, var)
  | Qbf.Undef -> Either.Left var

let print_result = function
  | Qbf.Unsat -> failwith "unsat"
  | Qbf.Timeout  -> failwith "timeout in qbf solver"
  | Qbf.Spaceout -> failwith "spaceout in qbf solver"
  | Qbf.Unknown  -> failwith "unknown error in qbf solver"
  | Qbf.Sat a ->
     let undefs, model = List.partition_map (assignment a) vars in
     eprintf "variables %s have no value assigned\n" (String.concat ", " (List.map string_of_int undefs));
     eprintf "model: %s\n" (String.concat ", " (List.map (fun (b, v) -> (if b then "" else "-") ^ string_of_int v) model))

let main () =
  eprintf "formula:%!";
  Qbf.QCNF.print Format.err_formatter formula;
  Format.pp_print_flush Format.err_formatter ();
  Format.print_newline ();
  let result = Qbf.solve ~solver:Quantor.solver formula in
  print_result result

let _ = main ()

[c-cube]

Good question, I have no idea.

[c-cube]

I can't find anything obviously bad in the bindings. It might be that quantor decides -2, -3, and then propagates +1 but doesn't assign it properly?

[AbdallahS]

Very puzzling!

[AbdallahS]

Do you know of any alternative ocaml bindings to some qbf solver that provides assignments? Thanks!

[c-cube]

sadly, no.