  The logical connectives typically found in programming languages are similar
to their mathematical counterparts, yet different due to their short-circuit
behaviour -- when evaluating them, the second argument is only evaluated if the
first argument is not sufficient to determine the result. Combined with the
possibility of side-effects, this creates a different type of logic called
Short Circuit Logic. A greater theoretical understanding of this logic can lead
to more efficient programming and faster program execution.
  In this thesis, formula satisfiability in the context of Short Circuit Logic
is discussed. A formal definition of evaluation based on valuation algebras is
presented, alongside an alternative definition based on valuation paths. The
accompanying satisfiability and `path-satisfiability' are then proven to be
equivalent, and an implementation of path-satisfiability is given. Although
five types of valuation algebras can be discerned, there are only three
corresponding types of valuation paths. From this, conclusions are drawn about
satisfiability and side-effects; the manner in which side-effects alter truth
values is relevant when analysing satisfiability, but the side-effects
themselves are not.
