Branching programs are a model for representing Boolean
functions. For general branching programs, the
satisfiability and nonequivalence tests are NP-complete.
For read-once branching programs, which can test each
variable at most once in each computation, the satisfiability
test is trivial and there is also a probabilistic polynomial
time test of nonequivalence of two diagrams by a result
of Blum, Chandra and Wegman (1980).

We generalize the satisfiability test and the probabilistic
nonequivalence test for syntactic (1,+k)-branching programs.
The algorithms work in time (cn/k)^k times a polynomial
in the input size, where c is an absolute constant. This
is better than the exhaustive search whenever k=o(n).

The restriction leading to syntactic (1,+k)-branching programs
is that for every path from the source to the 1-sink, there are
at most k variables that are read more than once. Let us point
out that even (1,+1)-branching programs are strictly more
powerfull than read-once branching programs. There are functions
with polynomial size (1,+1)-branching programs such that every
read-once branching program for them is of exponential size.