Sat4J:逻辑代数与优化问题最先进的求解程序

sat4j

Sat4j 是一个用来解决布尔可满足问题和最优化问题的工具库。它可以解决可满足问题极大可满足问题伪布尔问题极小不可满足子集问题。Java自带的求解器不能最快地解决这些问题(一个SAT 求解程序在Java中比在C++中要慢3.25倍),但是为了满足全能性、健壮性和用户友好性,遵循Java的设计方案和代码规范(源码静态分析检查)。这个工具库使用了强大的设计模式,设计很灵活。Sat4j是开源的,拿到了商业友好的EPL许可和学术友好的LGPL许可

想知道Sat4j的作用,你可以看看Sat4j研究案例 (初稿)。

多年以来,Sat4j应用于广大的研究团队,尤其在软件开发中,它多次出现在约束程序设计、AI或者软件验证课程中(查看引用Sat4j系统描述的全部文件/查看提及Sat4j的全部文件/查看所有提到Sat4j的网页)。

产品概述

SAT4J Core

  • SAT求解器有轻量级的程序设计约束。Eclipse或者Equinox 3.4以上版本依赖于OSGI bundle:org.sat4j.core.
  • Maven声明:
  • 输入格式:Dimacs CNF 或 AIG
  • API:访问Java API文档

SAT4J SAT

  • Java的SAT工具包。提供了SAT4J核心的一个命令行接口,可以轻易地检测到各种SAT求解器配置。
  • Maven 声明:
  • 输入格式: Dimacs CNF 或 AIG
  • API:访问JavaAPI文档
  • 依赖:SAT4J Core、Apache Jakarta Commons (BeanUtils, CLI)

SAT4J Pseudo

  • 伪布尔结算器。Eclipse或者Equinox 3.4以上版本依赖于OSGI bundle: org.sat4j.pb
  • Maven 声明:
  • 输入格式:PB evaluation格式 
  • API:访问JavaAPI文档
  • 依赖:SAT4J Core

SAT4J Maxsat

  • 极大可满足解算器建立在伪布尔最优化问题的简化的基础上
  • Maven 声明:
  • 输入格式:Max SAT evaluation格式 
  • API:访问JavaAPI文档
  • 依赖:SAT4J Core, SAT4J PB, Apache Jakarta Commons

SAT4J CSP

  • CSP解算器建立在SAT转移的基础上
  • Maven 声明:
  • 输入格式:CSP competition XML格式
  • API:访问JavaAPI文档
  • 依赖:SAT4J Core, Rhino

Sudoku Demo

  • 基于SAT的数独发生器和结算器。由Ivor Spence贡献。也可作为在线小应用使用。
  • 输入格式:绝大多数数独在线格式
  • 依赖:SAT4J Core。作为独立的完整安装包(包含SAT4J core)

文档

求解器的结构最近已经被发布在JSAT系统描述中:Daniel LeBerre,Anne Parrain.Sat4j文库.可满足性期刊2.2发行版,《布尔建模和计算》,2010,7期,系统描述,59-64

一个开始向导目前正在开发中。欢迎反馈。

SAT4J @ Objectweb上有一个维基风格的技术文档。如果有问题可以用OW2 Jira Trackers反映你的问题和性能请求,也可以通过我们的论坛或者给sat4j.org发送请求帮助邮件联系我们。

如果你想知道在这个文库中找到关于求解器更详细的性能,可以把求解器的描述提交到各种竞赛和评估中:

开贴列出各种SAT4J项目的依赖包会有一些帮助。

一些帮助链接

官方网站:http://www.sat4j.org/
开源地址:svn://svn.forge.objectweb.org/svnroot/sat4j/maven/trunk

打赏支持我整理更多优质资源,谢谢!

打赏编辑

打赏支持我整理更多优质资源,谢谢!

任选一种支付方式

1 收藏

资源整理者简介:百焱

选最难走的路 个人主页 · 贡献了1个资源 · 19 ·     


直接登录

推荐关注

按分类快速查找

关于资源导航
  • 伯乐在线资源导航收录优秀的工具资源。内容覆盖开发、设计、产品和管理等IT互联网行业相关的领域。目前已经收录 1440 项工具资源。
    推送伯乐头条热点内容微信号:jobbole 分享干货的技术类微信号:iProgrammer