使用二进制决策图解决抽象辩证框架；在德累斯顿（ADF-BDD）开发

这是可执行求解器的readme文件。

抽象辩证框架

抽象辩证框架（ADF）由抽象语句组成。每个语句都有一个唯一的标签，可能与ADF中的其他语句（s）相关。这种关系由一个所谓的接受条件（ac）定义，直观上是一个命题公式，其中的变量符号是语句的标签。解释是一种三值函数，将每个语句映射到真值（真、假、未决）。我们称这种解释为模型，如果每个接受条件都与解释一致。

有序二进制决策图

有序二进制决策图是二进制函数的一种标准化表示，其中可以相对便宜地进行可满足性和有效性检查。

用法

USAGE:
    adf-bdd [OPTIONS] <INPUT>

ARGS:
    <INPUT>    Input filename

OPTIONS:
        --an                      Sorts variables in an alphanumeric manner
        --com                     Compute the complete models
        --counter <COUNTER>       Set if the (counter-)models shall be computed and printed,
                                  possible values are 'nai' and 'mem' for naive and memoization
                                  repectively (only works in hybrid and naive mode)
        --export <EXPORT>         Export the adf-bdd state after parsing and BDD instantiation to
                                  the given filename
        --grd                     Compute the grounded model
    -h, --help                    Print help information
        --heu <HEU>               Choose which heuristics shall be used by the nogood-learning
                                  approach [possible values: Simple, MinModMinPathsMaxVarImp,
                                  MinModMaxVarImpMinPaths]
        --import                  Import an adf- bdd state instead of an adf
        --lib <IMPLEMENTATION>    Choose the bdd implementation of either 'biodivine', 'naive', or
                                  hybrid [default: hybrid]
        --lx                      Sorts variables in an lexicographic manner
    -q                            Sets log verbosity to only errors
        --rust_log <RUST_LOG>     Sets the verbosity to 'warn', 'info', 'debug' or 'trace' if -v and
                                  -q are not use [env: RUST_LOG=debug]
        --stm                     Compute the stable models
        --stmca                   Compute the stable models with the help of modelcounting using
                                  heuristics a
        --stmcb                   Compute the stable models with the help of modelcounting using
                                  heuristics b
        --stmng                   Compute the stable models with the nogood-learning based approach
        --stmpre                  Compute the stable models with a pre-filter (only hybrid lib-mode)
        --stmrew                  Compute the stable models with a single-formula rewriting (only
                                  hybrid lib-mode)
        --stmrew2                 Compute the stable models with a single-formula rewriting on
                                  internal representation(only hybrid lib-mode)
        --twoval                  Compute the two valued models with the nogood-learning based
                                  approach
    -v                            Sets log verbosity (multiple times means more verbose)
    -V, --version                 Print version information

注意，只有在选择原始库的情况下，导入和导出才有效

目前没有关于计算模型的附加信息，因此如果使用 --com --grd --stm，结果之间的边界不会明显地传达。但它们可以很容易地识别

• 计算始终以相同的顺序进行
  • grd
  • com
  • stm
• 我们知道始终存在一个唯一的基础模型
• 我们知道始终至少存在一个完整模型（即基础模型）
• 我们知道不一定存在稳定模型
• 我们知道每个稳定模型也是完整模型

输入文件格式

每个语句由ASP风格的单一谓词s定义，其中包含的项表示语句的标签。二元谓词ac将每个语句与一个前缀表示的命题公式相关联，其中的逻辑运算符和常量如下

• and(x,y): 合取
• or(x,y): 析取
• iff(x,y): 当且仅当
• xor(x,y): 异或
• neg(x): 经典否定
• c(v): 常量符号 "verum" - 重言式/顶
• c(f): 常量符号 "falsum" - 矛盾/底

开发备注

要构建二进制文件，需要运行

$> cargo build --workspace --release

要构建带有调试符号的二进制文件，运行

$> cargo build --workspace

要运行子模块中放置的所有测试，需要运行

$> git submodule init

首次。之后，您需要通过以下方式更新子模块的内容，以使其与当前使用的修订版保持一致

$> git submodule update

可以通过使用 cargo 的测试框架来启动测试，即：

$> cargo test

请注意，其中一些实例相当大，完成所有测试可能需要一些时间。如果您未初始化子模块，则测试将仅在其它单元测试以及（可能即将到来的）其他集成测试上运行。由于生成的测试模块的方式，您需要调用

$> cargo clean

如果您更改了某些测试用例。

要删除测试，只需输入

$> git submodule deinit res/adf-instances

或

$> git submodule deinit --all

致谢

本研究部分得到德国研究协会（DFG，德国研究基金会）在项目编号 389792660（TRR 248，清晰系统中心），联邦教育与研究部（BMBF，联邦教育与研究部）在可扩展数据分析和人工智能中心（ScaDS.AI），以及德累斯顿电子推进中心（cfaed）的支持。

所属机构

本研究部分由知识系统组，计算机科学学院，德累斯顿工业大学开发。

免责声明

在此托管内容不构成与德累斯顿工业大学正式或法律关系的依据。