About this project.

First assignment -- Lucas Escot & Romain Liautaud -- PROJ2 (Daniel Hirschkoff, ENS de Lyon, 2017).

Usage.

• Compile with make.
• Run with ./f2bdd demo.form.
• Add option -tseitin foo.cnf to convert the input formula to the DIMACS SAT format (via a Tseitin transform), and save it in file foo.cnf.
• Add option -minisat to run the SAT conversion of the input formula through minisat, and display the satisfiability results.
• Add option -debug to get useful information, e.g. about the output of the parser and the Tseitin transform.
• Add option -tests to dismiss all the other arguments, and run a series of tests (detailed below).

Test suite.

When running ./f2bdd -tests, the following tests will be performed:

• parity, for n in 15..20.
• adder, for n in 3..7.
• rotation, for n in 5..10.
• drawers, for n in 1..5.
• Randomly generated formulas of depths in 10..15.

Code structure.

We've decided to go for a fairly simple yet effective structure:

• All the source files for our modules are located inside the src folder, while all the build files generated by ocamlbuild are added to the _build folder: this way we don't mix up the two.
• The entrypoint for every command is the Main module, which parses the command's arguments using the Arg module from Ocaml's standard library, and performs calls to other modules accordingly.
• The lexing and parsing of logical formulas is handled by ocamllex and ocamlyacc, which are configured using files lexer.mll and parser.mly.
• Once parsed, those formulas are turned into expressions, which have type Expr.expr. The Expr module also provides a couple of utility functions for expressions, such as string_of_expr, rename_vars or simplify.
• Those expressions, in turn, can be used to either generate a ROBDD using module Bdd, or can be transformed into Cnf form using module Tseitin.
• The module Hashcons provides a generic hashconsing mechanism (detailed below), which in our case is used by module Bdd.
• The module Cnf provides a generic representation of a formula in Conjunctive Normal Form, along with utilities to export such a formula to the DIMACS format, and to feed it to minisat.
• Without surprise, the Tests module contains a few examples of logical formulas, as well as a compare function which makes sure that the BDD generated from an expression and the output of minisat on the same expression are coherent.

Implementation details.

ROBDD & Hash-consing.

After a bit of research on hashconsing (what we want to enforce on our bdds), we found a paper by Filliâtre explaining how to write a proper implementation in OCaml. Hash-consing done in Filliâtre's way makes many things a lot easier: we have the guarantee that values of the type hash_consed are in fact hash-consed, allowing the use of physical equality instead of structural equality (expected speedup). A nice feature of Filliâtre's implementation is that it plays alongside garbage collection, meaning if objects can only be found in the internal table used during the building process, they can be collected by garbage collection (programs should in turn be more memory efficient, as opposed to using a simple Hashmap). Finally, each hash_consed term is associated with a unique integer id (its tag), allowing for the use of somewhat efficient data structures.
In our code, to apply a process to hash_consed objects only once, we create a Set of objects in which they are ordered by their tag.

Notable differences.

• Instead of having a reference to some global integer for the next tag available, used by every hash_consed data structure, we restricted such an integer to the hash_consed data structure to not waste tags as much. It also means two hash_consed terms created from different data structures could have the same tag, but we did not find any situation in which it may have been an issue.

• Filliâtre's implementation allows for a flexible resize mechanism, in which you can specify a treshold (of the mean number of elements stored per bucket of the underlying hashmap) beyond which the table should be resized. We opted to fix this threshold to 3, meaning if there is an average of more than 3 items per bucket, a resize operation is triggered.

• Regarding resizing, the original implementation relies on mutually recursives functions (add and resize) meaning in theory if you're not careful a resize operation could trigger another resize operation and so on. This is where they fiddle with the threshold mentionned earlier, to prevent such an event from happening.
  We decided to make these functions independant, and make hashcons be the function to trigger resize when needed.

About sifting.

After a few fruitless attempts, we've decided not to implement sifting altogether. One of the reasons is purely practical: the swap operation used in sifting is indeed not easily implementable using our tree-based data structure for expressions, so supporting sifting would have meant moving away from this structure to something much less idiomatic, and rewriting most of our existing code in the process.

Tseitin transform.

Our implementation of the Tseitin transform is pretty straightforward: because our Cnf data structure is mutable, we can build it incrementally, adding clauses each time we explore a new sub-formula.

Note that, in order to achieve some form of Hash-consing, we didn't reuse the Hashcons module that is used for ROBDDs. Indeed, the likelihood of two (or more) clauses being equal in our Cnf was very small, as Tseitin uses a new variable name each time it processes a new sub-formula, and so, for instance, say we processed (1 \/ 2) /\ (1 \/ 2):

• The (1 \/ 2) on the left would be explored first. We would assign it variable 3, and so the Cnf would receive clauses (3 \/ -1) and (3 \/ -2) and (-3 \/ 2 \/ 1).
• Then the (1 \/ 2) on the left would also be explored. We would assign it variable 4, and so the Cnf would receive clauses (4 \/ -1) and (4 \/ -2) and (-4 \/ 2 \/ 1).
• Finally, the whole formula would be explored. We would assign it variable 5, and so the Cnf would receive clauses (5) and (5 \/ -4 \/ -3) and (-5 \/ 3) and (-5 \/ 4).

We then see that, if we used our Hash-consing module directly, none of the clauses that were added to the Cnf could be shared because they are all different. What we do, instead, is go through the proxy function of the Tseitin module, which uses a Hashtbl to check, before we process a sub-formula, if an equivalent sub-formula was already processed before, in which case we directly return its variable name. Then, on the same example of (1 \/ 2) /\ (1 \/ 2):

• The (1 \/ 2) on the left would be explored first. We would assign it variable 3, and so the Cnf would receive clauses (3 \/ -1) and (3 \/ -2) and (-3 \/ 2 \/ 1).
• Then the (1 \/ 2) on the left would also be explored. Because we're using the proxy function, we wouldn't add any more clauses to the Cnf, but only return the number 3.
• Finally, the whole formula would be explored. We would assign it variable 4, and so the Cnf would receive clauses (4) and (4 \/ -3 \/ -3) and (-4 \/ 3).