Algorithms / Cnf Modeling
Least You Need to Know: CNF Modeling, Clauses, and Constraint Encoding
Constraint problems are often made algorithmic by encoding decisions as Boolean variables and requirements as clauses. In conjunctive normal form (CNF), the whole formula is an AND of clauses, and each clause is an OR of literals. Modeling skill means turning real constraints into that structure cleanly.
The least you need to know
- A literal is a variable or its negation.
- A CNF formula is a conjunction (AND) of clauses, where each clause is a disjunction (OR) of literals.
- A satisfying assignment makes every clause true.
- Constraint modeling chooses variables whose truth values represent meaningful decisions.
- At-least-one and at-most-one requirements are common CNF encoding patterns.
Key notation
literal
a Boolean variable or its negation
clause
an OR of literals
CNF
an AND of clauses
Tiny worked example
- Let `x_{i,j}` mean 'student `i` is assigned to slot `j`'.
- An at-least-one clause can require each student to get some slot.
- Pairwise at-most-one clauses can forbid a student from getting two different slots.
- Satisfying assignments then correspond to legal schedules under the modeled constraints.
Common mistakes
- Students often confuse the outer AND over clauses with the inner OR inside a clause.
- A formula is satisfiable only if every clause can be made true simultaneously.
- Good SAT modeling starts with meaningful variables, not with clauses first.
How to recognize this kind of problem
- The prompt describes yes/no decisions plus hard logical constraints.
- You can name Boolean variables whose truth values encode candidate choices.
- The requirements naturally split into must-hold clauses.