Sat unit_propagate()

in include/poac/core/sat.hpp [108:135]

• 22 lines of code
• 7 McCabe index (conditional complexity)

    Sat unit_propagate(std::vector<std::vector<int>>& clauses, std::vector<int>& literals) {
        bool unit_clause_found = true;
        while (unit_clause_found) {
            unit_clause_found = false;

            for (auto itr = clauses.begin(); itr != clauses.end(); ++itr) {
                if (itr->size() == 1) { // unit clause ({3}, {5}, ...)
                    unit_clause_found = true;

                    // 0 - if true, 1 - if false, set the literal
                    literals[literal_to_index(*itr->begin())] = *itr->begin() < 0;

                    const int index = literal_to_index(*itr->begin());
                    Sat result = delete_set_literal(clauses, index, literals[index]);
                    if (result == Sat::satisfied || result == Sat::unsatisfied) {
                        return result;
                    }
                    // 今回のdeleteで，別のunit caluseができているかもしれないので，もう一度先頭からループし直す
                    break;
                }
                else if (itr->empty()) {
                    // the formula is unsatisfiable in this branch
                    return Sat::unsatisfied;
                }
            }
        }
        return Sat::normal;
    }