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.