The Sat4j library, release 2.2

By Daniel Le Berre, Anne Parrain. Journal on Satisfiability, Boolean Modeling and Computation, 2010

624 citations recorded by the source corpus.

Sat4j is a mature, open source library of SAT-based solvers in Java. It provides a modular SAT solver architecture designed to work with generic constraints. Such architecture is used to provide SAT, MaxSat and pseudo-boolean and solvers for lightweight constraint programming. Those solvers have been evaluated regularly in the corresponding international competitive events. The library has been adopted by several academic softwares and the widely used Eclipse platform, which relies on a pseudo-boolean solver from Sat4j for its plugins dependencies management since June 2008.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/037a3faa61f4ea56c33f2325d9a0daf09c304a06

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Software

Citations in the corpus

Core-Boosted Linear Search for Incomplete MaxSAT (2019, background): “SAT-based MaxSAT solvers can be roughly partitioned into linear [28, 29], core-guided [4, 25, 41, 8, 44, 41], and implicit hitting-set-based [21, 45] algorithms.”
Techniques Inspired by Local Search for Incomplete MaxSAT and the Linear Algorithm: Varying Resolution and Solution-Guided Search (2019, methodology): “The linear MaxSAT solvers fall into this category and approaches diﬀer in the way the upper bounding constraint is handled: SAT4J [18] uses linear propagators, a technique from constraint programming to avoid explicitly encoding the constraint into Boolean formula, while QMaxSAT [17] and…”