该库可用于满足CNF/DNF满意的分配，服从给定的文本加权权函数，并投影到给定的采样集上。
waps的Python项目详细描述
waps采样器
加权和投影取样器waps在符合由文字加权权重函数定义的权重分布的采样集上生成样本。它通过使用cnf的编译的确定性可分解否定范式（d-dnnf）来操作。它期望dimacs格式的cnf和d-dnnf与C2D compiler生成的格式相同。是基于我们在TACAS-2019会议上发表的题为“加权和预测抽样”的论文。
安装
sudo apt-get install graphviz sudo apt-get install libgmp-dev sudo apt-get install libmpfr-dev sudo apt-get install libmpc-dev pip install -r requirements.txt wget -P bin/ http://www.cril.univ-artois.fr/KC/ressources/d4 chmod u+x bin/d4
目前，D4 compiler和Dsharp_PCompile（针对我们的用例进行了修改，请参阅“pccompile”过程）作为将cnf编译为d-dnnf的默认过程。任何其他编译器只要稍加修改就可以轻松使用。
运行waps
您可以使用waps目录中的“waps.py”python脚本运行waps。一个简单的调用如下：
python3 waps.py <cnffile>
通过运行可以找到参数的用法说明和默认值
python3 waps.py -h
重量格式
waps支持在cnf中提供权重，而不是在文件中单独提供。文本的权重在[0，inf]中，由以“w”开头的行指定，文本和权重由空格分隔。稍后，waps将其规范化，使weight（l）+weight（-l）=1，其中l是一个文本。虽然应该指定正文本和负文本的权重，但如果只指定了正文本的权重，WAPS则假定它是规范化的，并将负文本的权重指定为1-权重（L）。默认情况下，如果cnf或weightfile中没有给定每个文本的值，则每个文本的权重都设置为0.5。
指定采样集
waps支持在cnf中提供采样集。它由以“c ind”开头、以空格分隔的变量索引和以0结尾的行指定。如果未提供采样集，则默认情况下，公式中指定的每个变量都假定为采样集的一部分。
输出格式
默认情况下，输出样本存储在samples.txt中。输出的每一行由一个序列号的样本和一个投射在样本集上的令人满意的赋值组成。令人满意的任务由被空间分隔的文字组成。注意，将random assignment（--randsign）设置为0可能会导致每行中的部分赋值。在这种情况下，可以将未分配的采样变量选择为true或false。
此外，waps可以为输入nnf输出d-dnnf的图形表示。在这个d-d nnf中，leaves由文本组成，内部节点可以是或（'o'）或和（'a'）节点，正如nnf所期望的那样。但是，在我们的表示中，内部节点也包含两个用空格分隔的数字。第二个给出了注释。第一种，仅用于区分个别或和节点，没有其他含义。
基准
基准可以找到here。
python用法
waps也是pypi上的一个库，可以通过pip安装。
sudo apt-get install graphviz sudo apt-get install libgmp-dev sudo apt-get install libmpfr-dev sudo apt-get install libmpc-dev wget https://github.com/meelgroup/WAPS/master/bin/Dsharp_PCompile wget http://www.cril.univ-artois.fr/kc/ressources/d4 chmod u+x Dsharp_PCompile chmod u+x d4 sudo mv Dsharp_PCompile /usr/local/bin/ sudo mv d4 /usr/local/bin/ pip install waps
请重新加载shell，以便可以通过路径访问二进制文件。
典型用法如下：
fromwapsimportsamplersampler=sampler(cnfFile="toy.cnf")sampler.compile()sampler.parse()sampler.annotate()samples=sampler.sample()print(list(samples))
有关使用情况的详细信息，请访问：
fromwapsimportsamplerhelp(sampler)
问题、问题、错误等。
请点击顶部的“问题”和create a new issue。所有问题都会得到迅速的回应。
如何引用
@inproceedings{GSRM19,
author={Gupta, Rahul and Sharma, Shubham and Roy, Subhajit and Meel, Kuldeep S.},
title={WAPS: Weighted and Projected Sampling},
booktitle={Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
month={4},
year={2019},
code={https://github.com/meelgroup/WAPS},
abstract={Previous work on applying Knowledge compilation has focused on uniform sampling over all the variables. Since the constraints are written in high level languages such as Verilog, the popular CNF encoding schemes as Tseitin encoding introduces additional auxiliary variables. The resulting CNF formulas are not equivalent but equisatisfiable. In particular, for a formula $G$ specified in high level language we obtain a CNF formula F such that $G (X) = \exists Y F(X,Y)$. This makes one wonder if it is possible to extend Knowledge compilation based techniques to sample over a subset of variables. Furthermore, languages such as Verilog allow specification of weights to user-defined constraints, so there is a need to sample according to the posterior distribution. In this paper, we provide affirmative question to the above two questions: We propose KUS that samples over user defined subset of variables from posterior distribution for a given prior distribution defined over product spaces.},
}
贡献者
- 拉胡尔古普塔（grahul@iitk.ac.in）
- 舒巴姆·夏尔玛（smsharma@iitk.ac.in）
- 亚哈吉特罗伊（subhajit@iitk.ac.in）
- kuldeep meel（meel@comp.nus.edu.sg）
欢迎加入QQ群-->： 979659372
