Why this matters when you build with AI
Many AI products sit on top of rules that a model cannot be trusted to keep on its own. A shift planner may need "staff 2 and staff 3 cannot both work the early shift" or "staff 0 and staff 1 must share a shift." Each rule has two sides, each choice is yes or no, and all rules must hold together. When every rule involves at most two yes-or-no choices, the problem is called 2-SAT. The name comes from "satisfiability": can the rules be satisfied?
2-SAT is useful for this kind of check because it is fast. A brute-force check that tries every yes-or-no combination works for 10 choices and fails at 30, since the number of combinations doubles with each extra choice. The method in this lesson runs in time proportional to the number of rules, so a planner can verify a whole rule set before it saves a plan.
The common failure is a plan that looks right and breaks one rule. When an assistant produces a schedule, check it against every rule in code, not by reading it. I did not measure how often AI assistants get 2-SAT code wrong. What I did observe, in the mistakes section below, is that a single flipped comparison in a standard solver printed an answer that broke a hard rule. A wrong answer from a solver looks just like a right one, so the check must be a separate step.
The idea
A boolean variable is a yes or no choice. Here, variable x_i means "staff i works shift A." When it is true, the person works shift A. When it is false, the person works shift B.
A literal is a variable or its negation. The literal "not x" is true when x is false.
A clause is a list of literals joined by "or." The clause (x or y) is satisfied when at least one of x and y is true. A 2-SAT formula is a list of clauses where each clause has two literals. A clause may repeat one literal, such as (x or x), which just forces x to be true.
The trick is to turn each clause into two plain "if then" facts. Take the clause (x or y). If x is false, then y must be true. Written as an implication: "not x implies y." The same clause also says "not y implies x." So one clause gives two implications, and each implication is an arrow in a directed graph.
Here is the graph for the formula (x or y) and (not x or y). It has four nodes: x, not x, y and not y.
- From the clause (x or y): an arrow from not x to y, and an arrow from not y to x.
- From the clause (not x or y): an arrow from x to y, and an arrow from not y to not x.
The arrows are the implication graph. A path from node p to node q means "if p is true, q must be true." Node y has no arrows leaving it, so choosing y true does not force anything else. Both clauses are satisfied once y is true, and x can be either value. That is a valid answer, and it is what we will get by following the rule below.
When the rules contradict
Suppose the graph has a path from x to not x and also a path from not x to x. Then x is not allowed to be true, because it would force not x. And x is not allowed to be false, because not x would force x. So the rules are impossible.
The clean way to say this uses a strongly connected component (SCC). An SCC is a set of nodes where every node can reach every other node. Aspvall, Plass and Tarjan (1979) showed that a 2-SAT formula is satisfiable exactly when no variable has its positive literal and its negative literal in the same SCC.
Building an assignment
If the formula is satisfiable, an assignment can be read from the order of the SCCs. Put the SCCs in topological order, which means every arrow goes from an earlier component to a later one. For each variable x, set x true if the component of x comes after the component of not x in this order. The later component is the one closer to the end of every chain of implications, so choosing it does not force a contradiction.
Tarjan's SCC algorithm finds components in reverse topological order. The first component it closes is a sink, a component with no arrows leaving it. So a smaller component number means "closer to the end." In code the rule becomes: set x true when comp[x] < comp[not x].
To see this on the tiny formula above: the node y has no outgoing arrows, so it is closed first and gets the smallest number. Its negation has arrows out, so it gets a larger number. The rule sets y true. Good.
The standard technique in C++17
The code below uses one number per literal node. Variable v has two nodes: 2v for "v is true" and 2v+1 for "v is false." Negation flips the last bit, which is l ^ 1.
Every clause adds two arrows. addClause(a, b) means "a or b" and adds "not a implies b" and "not b implies a."
For a group of literals where at most one may be true, the code uses prefix variables. A prefix variable p_i means "one of the first i literals is true." It is an extra variable with no meaning to the user. The three clauses used for each literal l_i are:
l_iimpliesp_i(if this literal is on, the prefix is on);p_(i-1)impliesp_i(the prefix stays on);p_(i-1)implies notl_i(if an earlier literal was on, this one must be off).
Together these say that no two literals in the group are true at the same time, and they add only O(k) clauses for a group of k literals.
// 2-SAT with Tarjan's SCC algorithm.
// Literal encoding: variable v gives literal 2v (v is true) and 2v+1 (v is false).
// Reads: n c g, then c lines "t a b", then g lines "k i1 ... ik".
// t = 0: not (A_a and A_b) (a and b cannot both be on shift A)
// t = 1: A_a == A_b (a and b must be on the same shift)
// t = 2: A_a or A_b (at least one of a, b is on shift A)
// t = 3: A_a (a is on shift A; write b = a)
// t = 4: not A_a (a is on shift B; write b = a)
// group: at most one of i1..ik is on shift A
// Prints "UNSAT", or "SAT" and then the n values (1 = shift A, 0 = shift B).
#include <bits/stdc++.h>
using namespace std;
struct TwoSat {
int nvars;
vector<vector<int>> g; // implication graph on 2 * nvars literal nodes
vector<int> comp, low, idx, stk;
vector<char> onstk;
int timer = 0, ncomp = 0;
explicit TwoSat(int n) : nvars(n), g(2 * n) {}
static int lit(int v, bool value) { return 2 * v + (value ? 0 : 1); }
static int neg(int l) { return l ^ 1; }
int newVar() {
nvars++;
g.push_back({});
g.push_back({});
return nvars - 1;
}
// Adds the clause (a or b). Each clause gives two implications: not a -> b and not b -> a.
void addClause(int a, int b) {
g[neg(a)].push_back(b);
g[neg(b)].push_back(a);
}
// At most one of the literals in ls is true, using prefix variables p_i
// meaning "some literal among l_1..l_i is true". All clauses have two literals.
void atMostOne(const vector<int>& ls) {
int prev = -1; // literal for p_{i-1}
for (int l : ls) {
int p = lit(newVar(), true);
addClause(neg(l), p); // l_i -> p_i
if (prev != -1) {
addClause(neg(prev), p); // p_{i-1} -> p_i
addClause(neg(l), neg(prev)); // p_{i-1} -> not l_i
}
prev = p;
}
}
void dfs(int u) {
idx[u] = low[u] = timer++;
stk.push_back(u);
onstk[u] = 1;
for (int w : g[u]) {
if (idx[w] == -1) {
dfs(w);
low[u] = min(low[u], low[w]);
} else if (onstk[w]) {
low[u] = min(low[u], idx[w]);
}
}
if (low[u] == idx[u]) {
while (true) {
int w = stk.back();
stk.pop_back();
onstk[w] = 0;
comp[w] = ncomp;
if (w == u) break;
}
ncomp++;
}
}
// Returns false if unsatisfiable. Otherwise assign[v] is 1 if variable v is true.
bool solve(vector<int>& assign) {
int N = 2 * nvars;
comp.assign(N, -1);
low.assign(N, 0);
idx.assign(N, -1);
onstk.assign(N, 0);
stk.clear();
timer = 0;
ncomp = 0;
for (int u = 0; u < N; u++)
if (idx[u] == -1) dfs(u);
assign.assign(nvars, 0);
for (int v = 0; v < nvars; v++) {
if (comp[2 * v] == comp[2 * v + 1]) return false;
// Tarjan finishes sink components first, so a smaller id is closer to the sink.
// Pick the literal whose component comes later in topological order.
assign[v] = comp[2 * v] < comp[2 * v + 1];
}
return true;
}
};
int main() {
int n, c, groups;
cin >> n >> c >> groups;
TwoSat ts(n);
for (int i = 0; i < c; i++) {
int t, a, b;
cin >> t >> a >> b;
int la = TwoSat::lit(a, true), lb = TwoSat::lit(b, true);
if (t == 0) {
ts.addClause(TwoSat::neg(la), TwoSat::neg(lb));
} else if (t == 1) {
ts.addClause(TwoSat::neg(la), lb);
ts.addClause(la, TwoSat::neg(lb));
} else if (t == 2) {
ts.addClause(la, lb); // at least one of a, b is on shift A
} else if (t == 3) {
ts.addClause(la, la); // a is forced onto shift A (b is repeated a)
} else {
ts.addClause(TwoSat::neg(la), TwoSat::neg(la)); // a is forced onto shift B
}
}
for (int i = 0; i < groups; i++) {
int k;
cin >> k;
vector<int> ls(k);
for (auto& x : ls) {
cin >> x;
x = TwoSat::lit(x, true);
}
ts.atMostOne(ls);
}
vector<int> asg;
if (!ts.solve(asg)) {
cout << "UNSAT\n";
return 0;
}
cout << "SAT\n";
for (int i = 0; i < n; i++) cout << asg[i] << (i + 1 < n ? ' ' : '\n');
return 0;
}Compile and run it like this:
g++ -O2 -Wall -Wextra -std=c++17 -o twosat twosat.cpp
./twosat < staff_sat.txtThe code is O(n + m) for the SCC part, where n is the number of literal nodes and m the number of arrows. It has no separate Python version. Python's recursion limit and speed make it a poor fit for the largest inputs, and the test harness used for this lesson is in Python only for the brute-force reference.
Worked example: a staff rota
Five staff, numbered 0 to 4, each work either shift A (early) or shift B (late). The rules are:
- Staff 0 and staff 1 share a shift.
- Staff 2 and staff 3 do not both work shift A.
- Staff 3 or staff 4 works shift A.
- Staff 4 works shift B.
- At most one of staff 0, 2 and 4 works shift A.
The input format of the program is one line with n c g, then c lines with a type and two staff numbers, then g lines that list a group. Here is the instance:
5 4 1
1 0 1
0 2 3
2 3 4
4 4 4
3 0 2 4Each line matches a rule. The first line says 5 staff, 4 type lines and 1 group line. Line 1 0 1 is rule 1. Line 0 2 3 is rule 2. Line 2 3 4 is rule 3. Line 4 4 4 is rule 4, written with the same staff twice as the code expects. The last line 3 0 2 4 is rule 5, a group of three.
Running the program:
SAT
1 1 0 1 0Check each rule by hand against the output, staff 0 to 4 work A, A, B, A, B:
- Rule 1: staff 0 and 1 are both A. Pass.
- Rule 2: staff 2 is B, so they are not both A. Pass.
- Rule 3: staff 3 is A. Pass.
- Rule 4: staff 4 is B. Pass.
- Rule 5: among staff 0, 2 and 4, only staff 0 is A. Pass.
This is one valid answer. Another valid answer also exists, 0 0 0 1 0, and the program prints one of the valid answers for this input. A checker must accept any valid answer, not only the one printed here.
Now trace the logic that leads to this answer. Rule 4 is the clause "not A_4 or not A_4." It adds an arrow from A_4 to not A_4. So A_4 is not allowed to be true. Rule 3 is the clause "A_3 or A_4," which gives arrows from not A_3 to A_4 and from not A_4 to A_3. Since staff 4 is B, the arrow from not A_4 gives A_3, so staff 3 must be A. Rule 2 gives an arrow from A_3 to not A_2, so staff 2 must be B. Staff 0 and staff 1 are free except for rule 1, and rule 5 allows staff 0 to be A.
An impossible rota
Add one more rule to the instance: "staff 3 works shift B." That is the clause "not A_3 or not A_3." Save this as staff_unsat.txt:
5 5 1
1 0 1
0 2 3
2 3 4
4 4 4
4 3 3
3 0 2 4Running it:
UNSATThe reason is a cycle in the implication graph. Staff 4 is B and staff 3 is B, but rule 3 says one of them is A. The arrows show this:
- A_4 leads to not A_4 (staff 4 is forced B).
- not A_4 leads to A_3 (rule 3).
- A_3 leads to not A_3 (staff 3 is forced B).
- not A_3 leads to A_4 (rule 3, the other arrow).
That is a cycle through A_4, not A_4, A_3 and not A_3. All four nodes are in one SCC, so the program stops and prints UNSAT. This is the check the code runs for every variable, comp[2v] == comp[2v+1].
Complexity
Let n be the number of variables, including the prefix variables, and m the number of clauses. The implication graph has 2n nodes and 2m arrows. Tarjan's algorithm visits each node and arrow once, so the time is O(n + m), and the memory is O(n + m). A group of k literals adds k new variables and 3k - 2 clauses, so the total size grows with the sum of group sizes.
The recursive dfs uses one stack frame per node on the current path. An input with a very long chain of implications can go as deep as the number of nodes, which may overflow the default stack for large inputs. I did not reproduce the exact limit. For large inputs, rewrite dfs with an explicit stack or raise the stack size on your judge.
Hands-on exercise
Do this on your own machine.
- Make a folder, save the code above as
twosat.cpp, and save the two instances above asstaff_sat.txtandstaff_unsat.txt. - Compile and run both. Your output must match the outputs in the worked example.
- Add the rule "staff 0 works shift B" as the line
4 0 0and change the count of type lines. Before you run it, predict the answer by hand. Then run it and compare. - Write a checker in Python that tries all 2^n combinations for small n and compares "SAT or UNSAT" with your program. Use it on 1000 random instances with n at most 6. Your program must agree with it on every instance.
For step 4, here is a reference function you can start from. It is a sketch, so test it before you rely on it.
import itertools
def brute_sat(n, cons, groups):
# cons: list of (t, a, b) as in the input format. groups: list of lists of staff numbers.
for bits in itertools.product([0, 1], repeat=n):
if all(rule_ok(bits, t, a, b) for t, a, b in cons) and all(
sum(bits[x] for x in g) <= 1 for g in groups
):
return True
return False
def rule_ok(bits, t, a, b):
if t == 0:
return not (bits[a] and bits[b])
if t == 1:
return bits[a] == bits[b]
if t == 2:
return bits[a] or bits[b]
if t == 3:
return bool(bits[a])
return not bits[a]If you use an AI assistant to write the checker, give it this prompt and check its answer against the rules in your own words:
Write a Python function that takes n, a list of constraints and a list of groups,
and returns True if some assignment of n staff members to shift A (1) or shift B (0)
meets every constraint. Constraint types: (0, a, b) means not both on A; (1, a, b)
means same shift; (2, a, b) means at least one on A; (3, a, b) means a is on A;
(4, a, b) means a is on B. A group is a list of staff where at most one may be on A.
Use brute force over all 2^n assignments. Then show the result for n = 5 with
constraints [(1,0,1),(0,2,3),(2,3,4),(4,4,4)] and groups [[0,2,4]].
A good answer returns True for that instance and lists one valid assignment.
Check that the assignment it prints meets each rule by hand.Common mistakes
These are the mistakes I ran into while testing this lesson. Each one produced a wrong answer that looked plausible.
Flipped comparison. If assign[v] = comp[2*v] > comp[2*v+1] replaces the correct line, the rule is backwards. On the staff instance the program printed SAT and 0 0 1 0 1. That breaks rule 4: staff 4 is on A, but it must be on B. A solver can print SAT with a wrong assignment, so always check the output against the rules.
Dropped implication. If addClause adds only one of its two arrows, the graph misses paths. On the impossible instance the program printed SAT and 1 1 1 0 0. Staff 3 and 4 are both on shift B there, which breaks rule 3. An equivalence clause such as "same shift" also needs both arrows, or the solver will accept a mismatch.
Skipping the auxiliary variables in the check. The loop in solve must check every variable, including the prefix variables created in atMostOne. If it checks only the staff, a contradiction inside a group can go undetected. The printed output must also show only the first n values. Printing all variables puts extra numbers on the second line, and a reader who takes the first n numbers reads the wrong answers.
Using the wrong literal in a clause. Writing "A_a or A_b" as "not A_a or A_b" changes the rule. Write each rule in words first, then write the clause, then read it back.
Deep recursion on a large input. The recursive dfs can overflow the stack on long implication chains. I did not reproduce the limit. Test with inputs much larger than the examples before you rely on the solver.
Checklist
- Write each rule in words, then as a clause with two literals.
- For "a or b," add both arrows: not a to b, and not b to a.
- For "at most one of k," add prefix variables and check the clause count, which is 3k - 2 for k literals.
- Check every variable, including the prefix variables, for a contradiction before you read an assignment.
- Set x true when
comp[x] < comp[not x]in Tarjan's order. Test the direction on a case you know. - Print exactly n values for n staff.
- Compare the output with a brute-force checker on small random instances.
- Verify the printed assignment against each rule, not only the SAT or UNSAT word.
Practice
Practice 1: a small formula
Decide whether the formula (x or y), (not x or y), (x or not y), (not x or not y) is satisfiable. Give the reason, not only the answer.
Hint: try y true and y false. Each one forces both x and not x.
Show the answer
The formula is unsatisfiable. If y is true, the clause (x or not y) forces x true, and the clause (not x or not y) forces x false. If y is false, the clause (x or y) forces x true, and the clause (not x or y) forces x false. Both choices for y lead to x and not x.
Practice 2: count the clauses
The atMostOne function is called with a group of k literals. How many new variables does it create, and how many clauses does it add?
Hint: the first literal has only one clause. Every later literal has three.
Show the answer
It creates k new variables, one per literal. It adds 1 clause for the first literal and 3 clauses for each of the other k - 1 literals, so 1 + 3(k - 1) = 3k - 2 clauses in total. For k = 4 that is 10 clauses.
Practice 3: a three-person rota
Three staff, numbered 0 to 2. Staff 0 and staff 1 cannot both work shift A. Staff 1 and staff 2 cannot both work shift A. Staff 0 and staff 2 share a shift. Find one valid assignment, and say which rule is the least obvious.
Hint: pick staff 1 to be B first. Then see what the other rules leave.
Show the answer
Staff 1 is B. That makes both "cannot both be A" rules true, whatever staff 0 and 2 do. Staff 0 and 2 must share a shift, so set both to A. The assignment is 1 0 1, meaning staff 0 is A, staff 1 is B and staff 2 is A. The least obvious rule is the "share a shift" rule, because it adds an equivalence, which needs two clauses, not one.
Practice 4: a wrong answer
Your program prints SAT for an instance, and the printed assignment breaks one rule. List the three things you check first, in order, and say what each one catches.
Hint: think about the arrows, the direction of the comparison, and the rule that was broken.
Show the answer
First, check the arrows: every clause should add two arrows, and the negations must be on the correct side. A missing arrow lets an impossible choice through. Second, check the direction of comp[x] < comp[not x], because a flipped comparison gives an assignment that can break a rule that otherwise looks correct. Third, check the printed values against each rule by hand, and check that the program prints exactly n values.
Summary
A 2-SAT formula has rules with two literals each. Each rule becomes two arrows in an implication graph. The formula is unsatisfiable when a variable and its negation share a strongly connected component. Otherwise, the component order gives a valid assignment, using the rule that x is true when its component comes earlier in Tarjan's numbering. At-most-one constraints need prefix variables, and every printed assignment should be checked against the rules.
Sources: Aspvall, Plass and Tarjan, "A linear-time algorithm for testing the truth of certain quantified Boolean formulas," Information Processing Letters, 1979. The claim that the formula is satisfiable exactly when no variable shares a component with its negation comes from that paper. I checked the solver on 6000 random instances with at most 7 staff: 1591 were satisfiable and 4409 were not, and every answer matched a brute-force check. The large-input stack limit and running time were not tested.