Kissat SAT Solver

栏目: IT技术 · 发布时间: 1周前

来源: fmv.jku.at

内容简介:The Kissat SAT solver is a condensed and improved reimplementation ofCaDiCaL in C.It has improved data structures, better scheduling of inprocessing, optimized algorithms and implementation.The solver is not incremental yet, but can be used as a library.

本文转载自:http://fmv.jku.at/kissat/,本站转载出于传递更多信息之目的,版权归原作者或者来源机构所有。

The Kissat SAT solver is a condensed and improved reimplementation ofCaDiCaL in C.

It has improved data structures, better scheduling of inprocessing, optimized algorithms and implementation.

The solver is not incremental yet, but can be used as a library.

News

Kissat won first place in the main track of the SAT Competition 2020 and first place on unsatisfiable instances.

SAT Competition Winners

In order to show that SAT solving improved considerably in recent years, particularly also with Kissat in 2020, we collectedwinners of the SAT Competition from 2002 to 2020 and fixed and ported them to be compatabile with modern compilers.

Then we were running those "all-time winners" on our cluster on the competition instances from 2011, 2019 and 2020, more precisely on the 300 instances from the SAT Competition 2011 application track , the 400 instances from the SAT Race 2019 and the 400 instances from SAT Competition 2020 main track .

Here are plots showing the number of instances solved within a certain time limit, thus in essence the runtime cumulative distribution function (higher is better).

Kissat SAT Solver Kissat SAT Solver Kissat SAT Solver

Note, the SAT Competition 2011 application track had only 300 instances, while the other two benchmarks sets from 2019 and 2020 consist of 400 apparently much harder instances each.

Our cluster has two Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz CPUs and 128 GB of main memory on each node, thus is slightly slower, but comparable to the StarExec cluster used in the competition. As time limit we used 5000 seconds as it is now common in the competition. Main memory was limited to 8 GB for 2011 and 2019 to utilize our cluster best. For 2020 we increased the limit to 32 GB, which allowed all solvers to stay below the memory limit (the organizers announced a 24 GB memory limit originally but actually used 128 GB).

Download

The latest version is available on GitHub at https://github.com/arminbiere/kissat

The following source code submitted to the SAT Competition 2020 won first place in the main track and first place on the unsatisfiable instances of the main track:

[ kissat-sc2020-039805f2.tar.xz ]

The code has an MIT license.

Resources

See the following SAT Competition 2020 system description for more details:

Armin Biere, Katalin Fazekas, Mathias Fleury, Maximillian Heisinger.

CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling Entering the SAT Competition 2020 .

To appear in Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions .

[paper |bibtex |kissat |cadical | paracooba |plingeling |treengeling ]

There was also a related talk at POS'20 :

Armin Biere and Mathias Fleury.

Chasing Target Phases

11th Workshop on Pragmatics of SAT (POS'20)

Cyberspace, July 3, 2020.

[slides [ video |experiments ]


以上所述就是小编给大家介绍的《Kissat SAT Solver》,希望对大家有所帮助,如果大家有任何疑问请给我留言,小编会及时回复大家的。在此也非常感谢大家对 码农网 的支持!

关注码农网公众号

关注我们,获取更多IT资讯^_^


为你推荐:

查看所有标签

本站部分资源来源于网络,本站转载出于传递更多信息之目的,版权归原作者或者来源机构所有,如转载稿涉及版权问题,请联系我们

sat solver sat-solvers ceres-solver ms-solver-foundation
Spring 3.x企业应用开发实战

Spring 3.x企业应用开发实战

陈雄华 / 电子工业出版社 / 2012-2-1 / 90.00元

内容简介 Spring 3.0是Spring在积蓄了3年之久后,隆重推出的一个重大升级版本,进一步加强了Spring作为Java领域第一开源平台的翘楚地位。 Spring 3.0引入了众多Java开发者翘首以盼的新功能和新特性,如OXM、校验及格式化框架、REST风格的Web编程模型等。这些新功能实用性强、易用性高,可大幅降低Java应用,特别是Java Web应用开发的难度,同时有效......一起来看看 《Spring 3.x企业应用开发实战》 这本书的介绍吧!

JSON 在线解析
JSON 在线解析

在线 JSON 格式化工具

Markdown 在线编辑器
Markdown 在线编辑器

Markdown 在线编辑器

HEX HSV 转换工具
HEX HSV 转换工具

HEX HSV 互换工具