Flemming Nielson and Helmut Seidl. Succinct Solvers. , volume 01-12 of Forschungsbericht, 2001. Universität Trier, Mathematik/Informatik.
We develope a solver algorithm which allows to efficiently compute the optimal model of a very expressive fragment of predicate logic. The succinct formulation of the algorithm is due to the disciplined use of continuation and demoisation. This facilitates giving a precise characterization of the behaviour of the solver and to develop a complexity calculation which allows to obtain its formal complexity. Practical evaluation on a control-flow analysis on the ambient calculus shows a good match between theory and practise.