寻求类似Sat4j的Kissat/Glucose集成库及CNF测试方法

一、Java环境下类Sat4j式的Kissat/Glucose集成库 #

• Kissat的Java绑定：使用kissat-java，这是官方提供的JNI绑定，可通过Maven或Gradle引入依赖，直接通过Java接口调用Kissat的求解功能，用法和Sat4j类似，无需自行编写JNI桥接代码。
• Glucose的Java封装：可以使用glucose-java第三方封装库，或者在代码托管平台搜索基于JNI封装Glucose的开源项目，这些库会将Glucose的核心求解能力暴露为Java API，支持CNF加载、求解调用等操作。
• Sat4j扩展版本：社区存在部分Sat4j的fork项目，已经集成了Glucose求解器，可直接复用Sat4j的调用方式切换到Glucose。

二、用CNF文件测试Kissat和Glucose的方法 #

命令行快速测试 #

1. 编译可执行文件
   • Kissat：克隆源码后执行make命令，生成kissat二进制程序。
   • Glucose：克隆源码进入build目录，执行make生成glucose或glucose-syrup可执行文件。
2. 执行测试
   准备好CNF格式的测试文件（如test.cnf），在终端运行：
   • Kissat测试：./kissat test.cnf
   • Glucose测试：./glucose test.cnf
     执行后会输出sat（问题可满足）或unsat（问题不可满足），若为sat还会附带变量的可行赋值。

代码调用测试 #

• Kissat（Java绑定）：通过Kissat.loadCnf("test.cnf")加载CNF文件，调用solve()方法获取求解结果及变量赋值。
• Glucose（Java封装）：使用封装库提供的GlucoseSolver.loadCnf(filePath)方法加载文件，调用求解接口即可得到结果。

内容的提问来源于stack exchange，提问作者Anh