SAT solvers!!

problem definition in a nutshell

SAT is a NP-complete problem also called "satisfiability problem". It is most often presented in the form of a set of boolean clauses, each of those being a disjunction of literals. A literal is either a proposition or its negation. The problem goal is to find whether it exists a valuation for those boolean literals such that all clauses are true, and, in this case, to give such a valuation. In other words, can we give each proposition a truth value such that all clauses have at least one true literal?

A simple example is:

a or (not b)

b or c

(not a) or (not c)

(not c)

which is satisfiable by the valuation a=1, b=1, c=0

Dimacs syntax

There exists a simple, straighfoward standard format used to facilitate reading of a problem by a solver.

It is composed of:

Another example:

c a very personal comment on this problem

c talking about clauses and literals

p 3 2

1 2 3 0

2 -3 0

It represents the logical problem

x1 or x2 or x3

x2 or (not x3)


A list of a few problem (quite) simple on which to test a SAT-solver, in Dimacs format.

A short history of my interests in SAT:

2019: minisat-ml

2018-2020: batsat

2014-2020: Msat

2011: SAT solver in java

I have been working on a (relatively) efficient SAT-solver written in Java. It implements the DPLL algorithm, with the following features:

Some lacking features are: