TwoSat

2-SAT Solver

struct TwoSat {

bool[] vars;

struct Edge;

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

bool solve();

this(size_t n);

}

Constructors

this this(size_t n)

Members

Functions

addClause void addClause(size_t a, bool expectedA, size_t b, bool expectedB): Clause (vars[a] == aExpect) || (vars[b] == bExpect)
solve bool solve(): Solve 2-SAT

Structs

Edge struct Edge: Undocumented in source.

Variables

vars bool[] vars;: assigned variable

Examples

// 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);

TwoSat

Constructors

Members

Functions

Structs

Variables

Examples

Meta

Source