通过二叉决策图解决抽象辩证框架；在德累斯顿开发（ADF-BDD）

此库通过使用有序二叉决策图（OBDD）的实现，以高效的方式表示抽象辩证框架（ADf）

抽象辩证框架

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

语义之间值得注意的关系

它们可以很容易地识别

• 计算总是按照相同的顺序进行
  • grd
  • com
  • stm
• 我们知道总有一个唯一的地面模型
• 我们知道总存在至少一个完整模型（即地面模型）
• 我们知道不一定存在一个稳定模型
• 我们知道每个稳定模型也是完整模型

有序二叉决策图

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

请注意，此实现的一个优点是只使用一个oBDD对所有接受条件。这是因为它们都具有相同的签名（即所有陈述的集合+顶层和底层概念）。由于这种统一表示，两个或多个陈述共享的子公式的缩减只需要计算一次，并且已经存储在数据结构中供进一步应用使用。

用于根据给定公式创建BDD的算法在较大公式上表现不佳，因此可以使用最新的库来实例化BDD（https://github.com/sybila/biodivine-lib-bdd）。可以选择继续使用biodivine库或者切换回由adf-bdd实现的变体。这个库中实现的变体提供了已经完成的约简和记忆化技术，这是biodivine所没有的。此外，一些其他功能，如计数器模型计数，在biodivine中也不受支持。

注意，只有在选择朴素库时，导入和导出才能工作。

输入文件格式

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

and(x,y): conjunction
or(x,y): disjunctin
iff(x,Y): if and only if
xor(x,y): exclusive or
neg(x): classical negation
c(v): constant symbol “verum” - tautology/top
c(f): constant symbol “falsum” - inconsistency/bot

示例输入文件

s(a).
s(b).
s(c).
s(d).

ac(a,c(v)).
ac(b,or(a,b)).
ac(c,neg(b)).
ac(d,d).

使用示例

首先解析给定的ADF并排序语句，如果需要的话。

use adf_bdd::parser::AdfParser;
use adf_bdd::adf::Adf;
// use the above example as input
let input = "s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,or(a,b)).ac(c,neg(b)).ac(d,d).";
let parser = AdfParser::default();
match parser.parse()(&input) {
    Ok(_) => log::info!("[Done] parsing"),
    Err(e) => {
    log::error!(
        "Error during parsing:\n{} \n\n cannot continue, panic!",
        e
        );
        panic!("Parsing failed, see log for further details")
    }
}
// sort lexicographic
parser.varsort_lexi();

使用朴素/in-crate实现

// create Adf
let mut adf = Adf::from_parser(&parser);
// compute and print the complete models
let printer = adf.print_dictionary();
for model in adf.complete() {
    print!("{}", printer.print_interpretation(&model));
}

使用biodivine实现

// create Adf
let adf = adf_bdd::adfbiodivine::Adf::from_parser(&parser);
// compute and print the complete models
let printer = adf.print_dictionary();
for model in adf.complete() {
    print!("{}", printer.print_interpretation(&model));
}

使用混合方法实现

// create biodivine Adf
let badf = adf_bdd::adfbiodivine::Adf::from_parser(&parser);
// instantiate the internally used adf after the reduction done by biodivine
let mut adf = badf.hybrid_step();
// compute and print the complete models
let printer = adf.print_dictionary();
for model in adf.complete() {
    print!("{}", printer.print_interpretation(&model));
}

使用基于新NoGood的算法并利用新的带有通道的接口

use adf_bdd::parser::AdfParser;
use adf_bdd::adf::Adf;
use adf_bdd::adf::heuristics::Heuristic;
use adf_bdd::datatypes::{Term, adf::VarContainer};
// create a channel
let (s, r) = crossbeam_channel::unbounded();
let variables = VarContainer::default();
let variables_worker = variables.clone();
// spawn a solver thread
let solving = std::thread::spawn(move || {
   // use the above example as input
   let input = "s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,or(a,b)).ac(c,neg(b)).ac(d,d).";
   let parser = AdfParser::with_var_container(variables_worker);
   parser.parse()(&input).expect("parsing worked well");
   // use hybrid approach
   let mut adf = adf_bdd::adfbiodivine::Adf::from_parser(&parser).hybrid_step();
   // compute stable with the simple heuristic
   adf.stable_nogood_channel(Heuristic::Simple, s);
});
let printer = variables.print_dictionary();
// print results as they are computed
while let Ok(result) = r.recv() {
   print!("stable model: {:?} \n", result);
   // use dictionary
   print!("stable model with variable names: {}", printer.print_interpretation(&result));
#  assert_eq!(result, vec![Term(1),Term(1),Term(0),Term(0)]);
}
// waiting for the other thread to close
solving.join().unwrap();

致谢

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

所属单位

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

免责声明

在此托管的内容与德累斯顿工业大学不建立任何正式或法律关系。