Solving SAT via Positive Supercompilation (
from to on 02 Feb 00:09

A supercompiler is a program transformer of a certain type. The usual way of thinking about program transformation is in terms of some set of rules which preserve the functional meaning of the program, and a step-by-step application of these rules to the initial program. … The concept of a supercompiler is a product of cybernetic thinking. A program is seen as a machine. To make sense of it, one must observe its operation. So a supercompiler does not transform the program by steps; it controls and observes (SUPERvises) the running of the machine that is represented by the program; let us call this machine M1. In observing the operation of M1, the supercompiler COMPILES a program which describes the activities of M1, but it makes shortcuts and whatever clever tricks it knows in order to produce the same effect as M1, but faster. The goal of the supercompiler is to make the definition of this program (machine) M2 self-sufficient. When this is acheived, it outputs M2 in some intermediate language L_sup and simply throws away the (unchanged) machine M1.

- Valentin Turchin