sat.zok

// Check whether `model` evaluates `phi` to true.
// `phi` must be in 3-CNF.
// The length of `model` is the max number of distinct variables in the formula.
// The length of `phi` is the max number of clauses in the formula.
// A literal `x` in `phi` represents variable `x / 2` with positive polarity if
// `x` is even, and negative polarity if `x` is odd.

struct Clause {
	u32[3] literals
}

def main(private bool[5] model, Clause[2] phi):
	bool sat = true
	for u32 i in 0..2 do
		bool satClause = false
		for u32 j in 0..3 do
			u32 lit = phi[i].literals[j]
			u32 var = lit / 2
			bool polarity = (lit & 1) == 0
			satClause = satClause || (model[var] == polarity)
		endfor
		sat = sat && satClause
	endfor
	assert(sat)
	return

/*
(x0 \/ x1 \/ x2) /\ (x2 /\ x3 /\ x4)
Model example:
x0 = true
x1 = true
x2 = true
x3 = true
x4 = true

Witness encoding:
1 1 1 1 1 (model)
0 2 4 4 6 8 (phi)
*/

/*
(x0 \/ !x1 \/ x2) /\ (x2 /\ !x3 /\ x4)
Model example:
x0 = false
x1 = false
x2 = false
x3 = false
x4 = false

Witness encoding:
0 0 0 0 0 (model)
0 3 4 4 7 8 (phi)
*/