New Canonical Representations by Augmenting OBDDs with Conjunctive Decomposition
Authors: Yong Lai, Dayou Liu, Minghao Yin
JAIR 2017 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Empirical results show that the compiler significantly advances the compiling efficiency of canonical representations. In fact, its compiling efficiency is comparable with that of the state-of-the-art compilers of non-canonical representations. We also provide a compiler for the i-th language in the first family by translating the last language in the first family into the i-th language (i < ). Empirical results show that we can sometimes use the i-th language instead of the last language without any obvious loss of space efficiency. |
| Researcher Affiliation | Academia | Yong Lai EMAIL College of Computer Science and Technology, Jilin University, Changchun, 130012, P.R. China Dayou Liu EMAIL Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education, Changchun, 130012, P.R. China Minghao Yin EMAIL College of Computer Science and Information Technology, Northeast Normal University, Changchun, 130117, P. R. China |
| Pseudocode | Yes | Algorithm 1: Decompose(u) ... Algorithm 2: Condition(u, ω) ... Algorithm 3: Condition Min(u, b) ... Algorithm 4: Entail Tree(u, v) ... Algorithm 5: Disjoin Tree(u, v) ... Algorithm 8: Compile(ϕ, C) |
| Open Source Code | No | The paper does not provide a direct link to a source code repository for their developed compiler or explicitly state that their code is open-source or available in supplementary materials. It mentions third-party tools like 'CUDD: CU decision diagram package release 2.5.0' and 'Dsharp: Fast d-DNNF compilation with sharp SAT' which are not their own implementation code. |
| Open Datasets | Yes | The four compilers were tested on eight domains of benchmarks, including Bejing, blocksworld, emptyroom, grid, flat200, inductive-inference (II for short), iscas89 and sortnet, 7 and then we compared their compiling time and output sizes. ... 7. Bejing, blocksworld, flat200 and II come from SATLIB (http://people.cs.ubc.ca/ hoos/SATLIB/benchm .html); emptyroom, grid and sortnet are CNF formulas (https://bitbucket.org/haz/dsharp/downloads) converted from conformant planning problems described in a standard application of d-DNNF (Palacios et al., 2005); and iscas89 incorporates CNF formulas converted from the circuits iscas89 by iscas2cnf (http://vlsicad.eecs.umich.edu/BK/Slots/cache/sat.inesc.pt/ jpms/scripts/). |
| Dataset Splits | No | The paper mentions testing on 'eight domains of benchmarks' but does not specify how these datasets were split into training, validation, or test sets, nor does it refer to any standard predefined splits used in the experiments. It focuses on compilation results rather than model training. |
| Hardware Specification | Yes | Since the ROBDD-L compiler can only run in 32-bit systems, we conducted experiments to compare ROBDD[ c ]C with the ROBDD-L and d-DNNF compilers on a computer with a 32-bit two-core 2.99GHz CPU and 3.4GB RAM. Since mini C2D can only run in 64-bit systems, we conducted experiments to compare the ROBDD[ c ]C compiler with mini C2D on a computer with a 64-bit four-core 3.6GHz CPU and 8GB RAM. |
| Software Dependencies | No | The paper mentions several tools and technologies like 'd-DNNF compiler Dsharp', 'c2d', 'mini C2D', 'SAT solver', and 'CUDD: CU decision diagram package release 2.5.0'. While CUDD has a version specified, it is a third-party package. The paper does not provide specific version numbers for the key software components of their own or comparative systems, except for the third-party CUDD. |
| Experiment Setup | Yes | Individual runs were limited to a one-hour time-out. The ROBDD-L compiler does not use any variable order heuristic to guide compilation. We employed a preprocessing program to make it use the minfill heuristic. We also set mini C2D to use the minfill heuristic to guide compilation. ... In our experiments, the chain C was generated by the minfill heuristic. |