dunkelheit reference

dkh.twosat

  • TwoSat

    Declaration

    struct TwoSat;

    2-SAT Solver

    Examples

    1. // Solve (x0 v x1) ^ (~x0 v x2) ^ (~x1 v ~x2) auto sat = TwoSat(3); sat.addClause(0, true, 1, true); // (vars[0] == true || vars[1] == true) sat.addClause(0, false, 2, true); // (vars[0] == false || vars[2] == true) sat.addClause(1, false, 2, false); // (vars[1] == false || vars[2] == false) assert(sat.solve() == true); auto vars = sat.vars; assert(vars[0] == true || vars[1] == true); assert(vars[0] == false || vars[2] == true); assert(vars[1] == false || vars[2] == false);

    • vars

      Declaration

      bool[] vars;

      assigned variable

    • addClause

      Declaration

      void addClause(size_t a, bool expectedA, size_t b, bool expectedB);

      Clause (vars[a] == expectedA) || (vars[b] == expectedB)

    • solve

      Declaration

      bool solve();

      Solve 2-SAT

      Return Value

      satisfiable or not

    • this

      Declaration

      this(size_t n);

      Parameters

      size_t n

      # of variables