This is a FAQ related to the programming language SABR, which can be found at sabrlang.org
1) It seems far removed from the problem, using a language to write out a problem to be solved by a satisfiability solver rather than solved by the compiler itself. Why do it that way?
The satisfiability problem is an ongoing field of research and there are continual advancements in distributed and machine learning based Conjunctive Normal Form (CNF) solvers, and there will likely be greater discoveries in the future. Many are already using satisfiability solvers to solve problems in spatial and temporal logic. However, although the problem of restating some problem as a CNF will undergo improvements, these improvements may be less significant than the progress made in CNF solvers. As the solvers improve, it will be possible to just hook in a new CNF solver, and it will suddenly solve the problem faster. If, for example, a neural network algorithm been used to solve the SABR language problem, this type of effortless advancement would not be possible.
2) Where does SABR fit in relation to other language?
SABR is a domain specific language that fits in the discrete spatial and temporal representation niche of the constraint programming niche, which is a pretty small piece of the overall programming pie, and can’t even claim to have a monopoly on that. However, SABR does have the potential to cause people to think differently about the problems they face and how they can be solved.
3) Is the language expected to grow much in the future?
The language is stripped down by design because it is expected that the problems fed to it will be complicated enough that bells and whistles would hurt performance too much. One of the design goals was that the language should have at or under an n-squared relationship between the size of the program and the size of the CNF so that users will get a sense of when their programs may be becoming unmanageable for the CNF solver. Although frequently more constraint can speed up CNF solving, CNF size is still a fair heuristic to use for time to solve. As an added bonus, since SABR has this property it can be used to show that a problem class is NP easy.
The addition of a SABR Python library could in the future have features like integer programming, tiling for bin packing, model checking, Computational Tree Logic (CTL) and Linear Temporal Logic (LTL). Computer languages, like computer software, often suffer from feature creep (i.e. Duke Neukem Forever syndrome). It has been said that all software inevitably evolves up to and beyond the point it includes an email server and it is arguably gratuitous that Prolog can be used to write a webserver. So instead of adding features using the language syntax, greater utility may be gained from adding features to a library which uses SABR.
4) Any other future use cases?
SABR could be used for program verification and model checking, potentially to analyze assembly or byte code. Could also be used with machine learning, distributed computing, and GPU based CNF solvers. Constraint solving is a multifaceted area, so there are lots of opportunities to explore.