Skip to content

Instantly share code, notes, and snippets.

@WillyPillow

WillyPillow/lib.hpp

Last active December 12, 2019 10:02
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save WillyPillow/a5b4f12faefd66c7ce42690668c002b5 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save WillyPillow/a5b4f12faefd66c7ce42690668c002b5 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. WillyPillow revised this gist Dec 12, 2019. No changes.
  2. WillyPillow revised this gist Dec 12, 2019. No changes.
  3. WillyPillow revised this gist Dec 12, 2019. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion lib.hpp
    View file
    Original file line number Diff line number Diff line change
    @@ -50,6 +50,6 @@ bool Solve() {

    int GetResult(int id) { return 0; }

    #endif
    #endif // DIMACS

    } // namespace sat
  4. WillyPillow revised this gist Dec 12, 2019. 1 changed file with 2 additions and 1 deletion.
    3 changes: 2 additions & 1 deletion lib.hpp
    View file
    Original file line number Diff line number Diff line change
    @@ -2,6 +2,7 @@
    #include <cryptominisat5/cryptominisat.h>
    #else
    #include <fstream>
    #include <vector>
    #endif

    namespace sat {
    @@ -29,7 +30,7 @@ int GetResult(int id) {

    #else

    std::vector<std::vector<int> > clauses;
    std::vector<std::vector<int>> clauses;
    int n_vars;

    void Init(int n) { n_vars = n; }
  5. WillyPillow revised this gist Dec 10, 2019. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion lib.hpp
    View file
    Original file line number Diff line number Diff line change
    @@ -32,7 +32,7 @@ int GetResult(int id) {
    std::vector<std::vector<int> > clauses;
    int n_vars;

    void Init(int n) {}
    void Init(int n) { n_vars = n; }

    void AddClause(std::vector<int> v) { clauses.emplace_back(std::move(v)); }

  6. WillyPillow created this gist Dec 9, 2019.
    54 changes: 54 additions & 0 deletions lib.hpp
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,54 @@
    #ifndef DIMACS
    #include <cryptominisat5/cryptominisat.h>
    #else
    #include <fstream>
    #endif

    namespace sat {

    #ifndef DIMACS

    CMSat::SATSolver solver;
    std::vector<CMSat::Lit> lit_buf;

    void Init(int n) { solver.new_vars(n + 1); }

    void AddClause(std::vector<int> v) {
    lit_buf.clear();
    lit_buf.reserve(v.size());
    for (int x : v) lit_buf.emplace_back(abs(x), x < 0);
    solver.add_clause(lit_buf);
    }

    bool Solve() { return solver.solve() == CMSat::l_True; }

    int GetResult(int id) {
    auto r = solver.get_model()[id];
    return r == CMSat::l_True ? 1 : r == CMSat::l_False ? -1 : 0;
    }

    #else

    std::vector<std::vector<int> > clauses;
    int n_vars;

    void Init(int n) {}

    void AddClause(std::vector<int> v) { clauses.emplace_back(std::move(v)); }

    bool Solve() {
    std::fstream fs("out.dimacs", fs.trunc | fs.out);
    fs << "p cnf " << n_vars << ' ' << clauses.size() << '\n';
    for (auto &v : clauses) {
    for (auto x : v) fs << x << ' ';
    fs << "0\n";
    }
    fs.close();
    exit(0);
    }

    int GetResult(int id) { return 0; }

    #endif

    } // namespace sat