Partial merge from kind-backend branch, including Minisat and CNF work to