A simple logic solver performing the DPLL and Resolution algorithm written in Java.
Source code and compiled jar-file can be found on my github page: https://github.com/shamanDevel/FormelSolver
I wrote this tiny program in my first semester of the computer science bachelor to help me with the homework in discrete math. It’s not perfect, it is slow, it is buggy, but it works.
Was it worth it? I don’t know.
It took me a few hours to build this program, so time saving was not the reason.
But: It helped me a lot to learn and truly understand how DPLL and Resolution work.
Furthermore, every time I hold a tutorial for first semester students, I show them this program to motivate them to write such a thing as well and understand the algorithms. It has not worked yet 😉 .
I provide this code “as is”. It only serves educational purpose to demonstrate how easily such a solver can be written.
All labels and messages are in german, sorry for that.
Examples:
DPLL:
Resolution:
