Programming in Propositional Logic or Reductions: Back to the Roots (Satisfiability)
Hermann Stamm-Wilbrandt · 1993
In this paper, NP-complete and polynomial solvable problems are reduced to the SATISFIABILITY problem. We call this process "programming" in propositional logic. On the one hand, the programs (propositional formulas) derived by this process build a rich pool of easy and hard (non-random) formulas for SATISFIABILITY-solving heuristics. On the other hand, the implementations (programs) give rise to new heuristics for solving SATISFIABILITY. Contents 1 Introduction 1 2 Useful formulas 2 3 Useful techniques 3 3.1 Removing terms of the form ": : : =) V ::: : : :" : : : : : : : : : : : : : : : : : : : : : 3 3.2 Removing terms of the form ": : : W ::: V ::: (: : :)" : : : : : : : : : : : : : : : : : : : : 3 3.3 Removing terms of the form ": : : () : : :" : : : : : : : : : : : : : : : : : : : : : : : 3 4 Different Reductions 4 4.1 Problems from P : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 4 4.1.1 SHORTEST PATH / SAT : : : : : : : : : : : : : : : : : :...