A computerized method and system for solving non-linear Boolean equations is
disclosed
comprising at least partially solving a Boolean function; developing at least one
inference regarding said Boolean function and saving said inference to a state
machine; and accessing said inference from said state machine to develop at least
one heuristic for determining whether said Boolean function is satisfiable.
