AA.cpp

#include <cstdint>
#include <fstream>
#include <sstream>
#include <unordered_set>
#include <vector>

using Literal = int;
using Clause = std::vector<Literal>;
using Solution = std::unordered_set<Literal>;

struct PartialSet {
    std::unordered_set<Literal> literals;
    std::unordered_set<int> unassigned;
};

enum class IsClauseSatisfiedResult {
    No,
    Yes,
    UndefinedYet,
};

IsClauseSatisfiedResult is_clause_satisfied(const Clause& clause, const std::unordered_set<Literal>& literals)
{
    for (Literal clause_literal : clause) {
        if (literals.find(-clause_literal) == literals.end()) {
            if (literals.find(clause_literal) != literals.end())
                return IsClauseSatisfiedResult::Yes;
            return IsClauseSatisfiedResult::UndefinedYet;
        }
    }

    return IsClauseSatisfiedResult::No;
}

Literal is_clause_unitary(const Clause& clause, const PartialSet& partial_set)
{
    int undefined_literal = 0;
    for (Literal clause_literal : clause) {
        // The clause is already satisfied by a literal of the partial set.
        if (partial_set.literals.find(clause_literal) != partial_set.literals.end())
            return 0;

        // The literal is already defined by the partial set.
        if (partial_set.literals.find(-clause_literal) != partial_set.literals.end())
            continue;

        // There are more undefined literals. The clause is not unitary.
        if (undefined_literal != 0)
            return 0;

        undefined_literal = clause_literal;
    }

    // The value of 'undefined_literal' is 0 if the clause is not unitary.
    return undefined_literal;
}

bool check_and_remove_clauses(std::unordered_set<uint32_t>& clauses_indices,
                              PartialSet& partial_set,
                              const std::vector<Clause>& clauses)
{
    for (auto it = clauses_indices.begin(); it != clauses_indices.end();) {
        size_t clause_index = *it;

        switch (is_clause_satisfied(clauses[clause_index], partial_set.literals)) {
            case IsClauseSatisfiedResult::No:
                return false;
            case IsClauseSatisfiedResult::Yes:
                it = clauses_indices.erase(it);
                break;
            case IsClauseSatisfiedResult::UndefinedYet:
                ++it;
                break;
        }
    }

    return true;
}

void dpll(std::unordered_set<uint32_t> clauses_indices,
    PartialSet& partial_set,
    const std::vector<Clause>& clauses,
    Solution& out_solution)
{
    if (!check_and_remove_clauses(clauses_indices, partial_set, clauses))
        return;

    while (true) {
        Literal undefined_literal = 0;
        int clause_index = 0;

        for (int index : clauses_indices) {
            undefined_literal = is_clause_unitary(clauses[index], partial_set);
            if (undefined_literal != 0) {
                clause_index = index;
                break;
            }
        }

        // There are no more unitary clauses.
        if (undefined_literal == 0)
            break;

        // Add the literal to the partial set as we know it is mandatory in order to satisfy
        // at least one clause.
        partial_set.literals.insert(undefined_literal);
        partial_set.unassigned.erase(std::abs(undefined_literal));

        // The unitary clause will always be satisfied.
        clauses_indices.erase(clause_index);

        if (!check_and_remove_clauses(clauses_indices, partial_set, clauses))
            return;
    }

    if (partial_set.unassigned.size() == 0) {
        out_solution = partial_set.literals;
        return;
    }

    int unassigned_variable = *partial_set.unassigned.begin();
    partial_set.unassigned.erase(unassigned_variable);

    {
        PartialSet new_partial_set = partial_set;
        new_partial_set.literals.insert(unassigned_variable);
        dpll(clauses_indices, new_partial_set, clauses, out_solution);
        if (out_solution.size() > 0)
            return;
    }

    {
        PartialSet new_partial_set = partial_set;
        new_partial_set.literals.insert(-unassigned_variable);
        dpll(clauses_indices, new_partial_set, clauses, out_solution);
        if (out_solution.size() > 0)
            return;
    }

    return;
}

Solution dpll(uint32_t variable_count, const std::vector<Clause>& clauses)
{
    std::unordered_set<uint32_t> clauses_indices;
    for (uint32_t clause_index = 0; clause_index < clauses.size(); ++clause_index)
        clauses_indices.insert(clause_index);
    
    PartialSet empty_partial_set;
    empty_partial_set.unassigned.reserve(variable_count);
    for (int variable = 1; variable <= static_cast<int>(variable_count); ++variable)
        empty_partial_set.unassigned.insert(variable);

    Solution solution;
    dpll(clauses_indices, empty_partial_set, clauses, solution);
    return solution;
}

struct ParseResult {
    uint32_t variable_count;
    std::vector<Clause> clauses;
};

ParseResult parse_expression_from_file(const std::string& filepath)
{
    std::ifstream input(filepath);
    ParseResult parse_result;

    uint32_t expected_clause_count = 0;
    uint32_t parsed_clause_count = 0;

    std::string line;
    while (std::getline(input, line)) {
        // Skip over comments or empty lines.
        if (line.empty() || line[0] == 'c')
            continue;

        if (line[0] == 'p') {
            std::stringstream stream(line);
            std::string p, cnf;
            stream >> p >> cnf;

            uint32_t n, m;
            stream >> n >> m;
            parse_result.variable_count = n;
            expected_clause_count = m;
            parse_result.clauses.reserve(expected_clause_count);
            continue;
        }

        if (parsed_clause_count >= expected_clause_count)
            break;
        ++parsed_clause_count;

        parse_result.clauses.emplace_back();
        Clause& clause = parse_result.clauses.back();

        std::stringstream stream(line);
        Literal literal;
        stream >> literal;
        while (literal != 0) {
            clause.push_back(literal);
            stream >> literal;
        }
    }

    return parse_result;
}

int main(int argc, char** argv)
{
    if (argc != 3)
        return 0;

    // NOTE: This order is defined by the automatic checker.
    //       The input file is the first argument, and the output file is the second argument.
    const std::string input_file = argv[1];
    const std::string output_file = argv[2];

    ParseResult parse_result = parse_expression_from_file(input_file);
    Solution solution = dpll(parse_result.variable_count, parse_result.clauses);

    std::ofstream output(output_file);

    if (solution.empty()) {
        output << "s UNSATISFIABLE" << '\n';
    }
    else {
        output << "s SATISFIABLE" << '\n';
        output << "v ";
        for (Literal l : solution)
            output << l << ' ';
        output << '\n';
    }

    return 0;
}