We observed that Conjunctive Normal Form (CNF) encodings of structured SAT instances often have a set of consecutive clauses defined over a small number of Boolean variables. To exploit the pattern, we propose a transformation of CNF to an alternative representation, Conjunctive Minterm Canonical Form (CMCF). The transformation is a two-step process: CNF clauses are first partitioned into disjoint subsets such that each subset contains CNF clauses with shared Boolean variables. CNF clauses in each subset are then replaced by Minterm Canonical Form (i.e., partial solutions), which is found by enumeration. We show empirically that a simple Stochastic Local Search (SLS) solver based on CMCF can consistently achieve a higher success rate using fewer evaluations than the SLS solver WalkSAT on two representative classes of structured SAT problems.

The space-time (s-t) algebra provides a mathematical model for communication and computation using values encoded as events in discretized linear (Newtonian) time. Consequently, the input-output behavior of s-t algebra and implemented functions are consistent with the flow of time. The s-t algebra and functions are formally defined. A network design framework for s-t functions is described, and the design of temporal neural networks, a form of spiking neural networks, is discussed as an extended case study. Finally, the relationship with Allen's interval algebra is briefly discussed.