Skip to content


Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Spatial and Action Based Resolver
C C++ Python
branch: master
Failed to load latest commit information.
core add lock to trans allowing TransLock keyword to force at least one tr…
doc doc
module make adrift compute clearer
parser add lock to trans allowing TransLock keyword to force at least one tr…
test add conway game of life example to tests
utils correct compiler warnings
.gitignore correct compiler warnings
LICENSE Change walkthrough URL in readme file reduce clutter add lock to trans allowing TransLock keyword to force at least one tr…



SABR (Spatial and Action Based Resolver) is a constraint programming language designed with an emphasis on spatial and temporal logic.

Programs compile to CNF (Conjunctive Normal Form), which is then solved by a CNF solver.

The goal of the language is to make representing operations research problems not just possible, but also intuitive and the solving of these problems efficient.

From a theoretical perspective, the language can also be used to prove a problem is NP-Easy and to verify properties about automata and systems that can be modeled as automata such as circuits and programs.


SABR is installed using

Build SABR and the CNF solver:

python build

For more commands:

python help


To run SABR, provide an optional flag, the number of stages to use, and the input source path. The solution can be found in result.txt.


./sabr 20 test/Simple/simple.tb

For more commands:

./sabr --help


Testing can be done with

Runs all tests:

python all

For more commands:

python help 


Let's see what the traditional river crossing puzzle looks like in SABR. A more detailed walkthrough is also available.

Sym { west east }

# each cell on the board can be any symbol
Board { cabbage goat wolf sailor }
Start { west west west west }
End { east east east east }

# transitions for object Crew
# sailor can take one passenger east or west
Trans SailEast:Crew { west west => east east }
Trans SailWest:Crew { east east => west west }

# describe object Crew's cells
DesObj Goat:Crew { sailor goat }
DesObj Cabbage:Crew { sailor cabbage }
DesObj Wolf:Crew { sailor wolf }
DesObj Alone:Crew { sailor sailor }

# options for object Watch, at least one must match
# sailor needs to be watching these two if they are together
Opt Watch { side side side }
Opt Watch { !side !side side }
Opt Watch { !side side !side }

DesObj Watch { sailor goat cabbage }
DesObj Watch { sailor wolf goat }

Running ./sabr 10 source.tb shows us the answer to the puzzle in result.txt (


For more documentation check /doc/LANGUAGE. Simple python module can be found at /module/


Something went wrong with that request. Please try again.