这是命令 depqbf,可以使用我们的多个免费在线工作站之一在 OnWorks 免费托管服务提供商中运行,例如 Ubuntu Online、Fedora Online、Windows 在线模拟器或 MAC OS 在线模拟器
程序:
您的姓名
depqbf - 量化布尔公式的求解器
概要
部门负责人 [选项 ...] [民[文件]
商品描述
部门负责人 是 prenex 中量化布尔公式 (QBF) 的基于搜索的求解器
合取范式。 基于 DPLL 算法的 QBF 冲突驱动
子句和解决方案驱动的立方体学习。 通过分析公式的结构,DepQBF
试图识别自变量。 除了其他好处,这通常
增加决策的自由度。 另请参阅 DepQBF 0.1 的 JSAT 系统说明
来自 QBFEVAL'10 的参考资料和想法的简要概述。
部门负责人 以 QDIMACS 格式读取 QBF 公式。 如果 文件 没有给出,它从
标准输入。 它符合QBFEVAL'10 要求的输入/输出标准。
配置
部门负责人 接受以下选项:
-H, - 帮帮我
打印使用信息。
- 版
印刷版。
--漂亮的印刷品
只解析和打印公式。
-v 逐步增加详细程度。
民 可选:NUM 秒后超时。
文件 可选:从 FILE 读取输入。
退出 状态
如果作为输入给出的 QBF 公式可满足,则退出状态为 10,如果满足则为 20
不满意; 任何其他退出代码都表明公式未解决。
使用 onworks.net 服务在线使用 depqbf