Satisfiability in the theory of lists

In this post I will present a program for checking the satisfiability of formulae in the list theory, that I developed as a project for a course in program verification.
For example the formula

atom(x) ^ x=cons(y,z)

is clearly unsatisfiable - here "^" means "AND".

It uses the Nelson-Oppen congruence closure algorithm, as described in this book and in this article.
The only requirement is a Java Runtime Environment.

Under UNIX the program can be started with ./listsat. You'll see that the program complains for missing options. If you pass the name of a (well formed) file containing a formula it prints something like:

Loading formula from file: ../random/r3.txt
Loaded after 0.265 secs

Formula contains 95 positive literals, 48 negative literals, 57 atoms (200 total).
Constructing initial DAG...
DAG constructed - time: 0.093
DAG has 921 nodes.
Starting Congruence Closure algorithm...

 ========== ========== ========== ========== ========== ========== [60/200]
 ========== ========== ========== =====*

CC algorithm ended - time: 0.685

Formula is UNSATISFIABLE
Last processed literal: g(h(x,y,f(x,t(x))),f(z,g(y,y)))!=y.



If you want to start the graphical interface pass the option -g.

The ListSAT main window

Here you can generate a random formula

The dialog for running the benchmarks.

The archive with sources and binaries.

The JAR-only archive.

An introductory article (in Italian).