这是命令 anldp，可以使用我们的多个免费在线工作站之一在 OnWorks 免费托管服务提供商中运行，例如 Ubuntu Online、Fedora Online、Windows 在线模拟器或 MAC OS 在线模拟器
程序：
您的姓名
anldp - Davis-Putnam 命题可满足性程序的实现
概要
安德普 [选项] 输入文件 > 输出文件
商品描述
本手册页简要记录了 安德普 命令。
安德普 是命题的戴维斯-普特南过程的实现
可满足性问题。 安德普 公开所使用的程序 mace2(1)确定
可满足性。 安德普 也可以在一阶逻辑中使用相等和 a 的语句
域大小 n 然后搜索尺寸的模型 n. 一阶模型搜索代码
将语句转换为命题从句集，使得一阶
语句具有大小模型 n 当且仅当命题从句是
令人满意的。 然后将命题集提供给 Davis-Putnam 代码； 任何
找到的命题模型可以转化为一阶模型
声明。 一阶模型搜索程序只接受扁平化的语句
没有功能符号的关系从句形式。
配置
-s 执行包容。 （包含始终在单元预处理期间执行。）
-p 打印找到的模型。
-m n 停止时 n找到第 th 个模型。
-t n 停止后 n 秒。
-k n 最多分配 n 用于存储子句的千字节。
-x n 拟群实验 n.
-B 文件
备份分配到文件。
-b n 备份作业每 n 秒。
-R 文件
从文件恢复分配。 该文件通常只包含最后一行
一个备份文件。 其他输入，特别是条款，必须完全按照
原始搜索。
-n n 此选项用于一阶模型搜索。 参数 n 指定
域大小，它的存在告诉程序读取一阶扁平化
关系输入从句而不是命题从句。
使用 onworks.net 服务在线使用 anldp