Since geometric resolution relies heavily on constraint solving,
the constraint solver is currently the most sophisticated part of Geo III.
The implementation is probably efficient enough for stand-alone use,
outside of geometric resolution. In order to make this possible,
the constraint solver can be download independently.
The implementation is in portable C++(11).
The solver reads input from a specified file, and prints output into stdout, either
UNSAT, or SAT and a satisfying substitution. It can be called with
option -cnf, which will cause it to transform the problem to CNF (Dimacs format)
without trying to solve it.
The input format is similar to DIMACS format for first-order logic, it is described in Section 7 of this article, which also contains a description of the matching algorithm used.
These are the sources.
In order to run the solver, unzip and untar. If you are lucky, you
can type ./solver gcsp_examples/summer2016/demod06.dim and watch the solver find
an interpretation.
Otherwise, type touch Makefile, type
make and hope that
the resulting executable works. You need a reasonably
new version of g++, because the solver uses C++-2014.
Subdirectory gcsp_examples contains examples.
The following input formats are possible
./solver Reads input from stdin, and writes a solution or ‘UNSAT’ to stdout.
./solver %filename Reads input from filename, and writes a solution or ‘UNSAT’ to stdout.
./solver -cnf Reads input from stdin, and writes conversion to CNF to stdout.
./solver -cnf %inputfile Reads input from %filename and writes CNF-conversion to stdout.
The following should work:
./solver -cnf gcsp_examples/summer2016/demod06.dim | minisat,
if you have minisat installed.