Program
Verification
Book

PV4 ⊧ Sat4jproduces a satisfiability result for a formula

Java library for boolean satisfaction and optimization problems. It can solve SAT, MAXSAT, Pseudo-Boolean and Minimally Unsatisfiable Subset (MUS) problems.

Application domain/field

SAT-based solvers
MaxSAT problems
Optimization problems

Type of tool

Java library that provides access to SAT-related technologies.

Expected input

Format:

DIMACS, or Aralia formula?

Expected output

UNSATISFIABLE if it is unsatisfiable
SATISFIABLE if satisfiable
it may cause an exception if e.g. a timeout occurs

Java Mathematical optimization SAT

Links

Project page: https://sat4j.org/
Repository: https://gitlab.ow2.org/sat4j/sat4j/
- Last commit date: 9 April 2022
- Last commit date: (Last release was on 14 December 2020)

Related papers

On Dedicated CDCL Strategies for PB Solvers (SAT '21)
On Weakening Strategies for PB Solvers (SAT '20)
https://content.iospress.com/articles/journal-on-satisfiability-boolean-modeling-and-computation/sat190098 (Journal on Satisfiability, Boolean Modeling and Computation '12)

Last publication date

2 July 2021

ProVerB specific

Markdown description: view/edit
Contained in the ProVerB22 dataset (paper + artefact)

ProVerB is a part of SLEBoK. Last updated: February 2023.