iascar (基于任何时间精炼的增量答案集计数器)

iascar 是一个针对在假设下频繁计数的命题模型计数器。计数器在 平滑确定性可分解否定范式 (sd-DNNFs) 或所谓的 压缩计数图 (CCGs) 上运行。

更多背景信息请参阅 https://doi.org/10.48550/arXiv.2311.07233。

安装 & 构建

• 使用 cargo 安装 iascar cargo install iascar
• 默认情况下，iascar 以并行方式运行，以进行任何时间精炼的增量计数；要避免并行执行，克隆此仓库并使用 cargo build --release --features seq

快速入门

1. 下载 lp2*-tools 和 c2d
2. 在 build_nnf.sh 中设置相应工具的路径，该脚本为支持的模型 (*.sm.*) 和答案集 (*.as.*) 建立cnfs和nnfs

• 使用以下命令从答案集编码的nnf中获得CCG：

iascar -com -lp example.lp -cnf example.lp.as.cnf -nnf example.lp.as.cnf.nnf > example.as.ccg

• 使用以下命令从支持的模型编码的nnf中获得CCG：

iascar -com -lp example.lp -cnf example.lp.sm.cnf -nnf example.lp.sm.cnf.nnf > example.sm.ccg

• 使用以下命令计数答案集：

iascar -ccg -in example.as.ccg
c o a=[]
s SATISFIABLE
c s log10-estimate 0.7781512503836436
c s exact arb int 6

• 使用以下命令计数假设 -9 和 10 下的答案集：

iascar -ccg -in example.as.ccg -a -9 10
c o a=[-9, 10]
s SATISFIABLE
c s log10-estimate 0.3010299956639812
c s exact arb int 2

• 使用基于编码的不可支持约束的任何时间精炼和未界定的交替深度计数答案集：

iascar -car -ccg example.sm.ccg -ucs exmaple.ucs -dep 0
c o d=1 n=1 a=[]  # depth d, number of unsupported constraints n, assumptions a
c o +par          # runs in parallel
c o 0 0.95        # overall log10-count of input ccg
c o 1.00-         # amount of unsupported constraints taken into consideration is 100% (1.00)
                  # and counting stopped on exclusion (-)
s SATISFIABLE
c s log10-estimate 0.7781512503836436
c s exact arb int 6

• 使用枚举计数答案集
  • iascar 使用 clingo，因此允许 clingo 参数，例如，使用 --supp-models 计数支持模型。特别是提供一个整数来声明要计数的最大答案集数。 0 代表无界。如果您不提供整数，iascar 将计数最多1个答案集
  • 将 % 预先附加到假设中，其中 l 代表一个正字面量，而 ~l 代表一个负字面量

iascar -enum -in examples/example.lp 0 %a %~f
c ["0"]
c ["a", "~f"]
s SATISFIABLE
c s exact arb int 1

• 基于答案集程序，使用 -nnf -in nnf_path 来计数 nnfs
• 使用任意 nnfs 来计数 -nnfarb -in nnf_path