Problem Solving By Proving Satisfiability
Shashank K. Mehta · Proceedings of SPIE, the International Society for Optical Engineering/Proceedings of SPIE · 1989
The satisfiability problem is shown to be a formulation suitable for problems in planning, scheduling, solid modeling, etc. which cannot be solved by the unsatisfiability formulation (logic programming). A reduction procedure is developed, to prove the satisfiability, using a geometrical interpretation of the logical expression to be satified. The procedure is shown to be applicable to the first-order clauses too.