[Edited for clarity] The most widely used definition in the research literature is the one that requires exactly k distinct variables per clause, and no duplicate clauses. If you relax the distinct ...

Start with a good survey paper. It's easy to attack the subject piecemeal and get confused by different names in the literature for the same techniques and the same name used for different techniques....

Let $m$ be the number of pigeons and $n$ be the number of holes. Let the propositional variables $B_{i,0}$ ... $B_{i,log(n)}$ encode the binary representation of $j-1$ if the $i$th pigeon is put into ...

If all XOR relationships between variables in CNF formulas could be detected in polynomial time, then this would allow the solution of UNAMBIGUOUS-SAT in polynomial time. By the Valiant–Vazirani ...

What you're describing is called subsumption; it is a standard CNF simplification technique for SAT solvers. None of the operations involved is worse than quadratic to either the number of variables ...

Pure literal elimination over base clauses is effectively deleting those clauses from the formula, an action which cannot be encoded in a RUP proof since such proofs only encode clause additions. But ...

Starting with the transition system for DPLL in definition 1 in the paper, add a state corresponding to the condition: $M \models F$ and no $l$ that appears in $F$ is undefined in $M$. The transition ...
Solving a Sudoku puzzle is equivalent to deciding whether there is a valid graph vertex coloring using $k$ colors, where $k = 9$ in your $3 \times 3$ Sudoku instance. The graph coloring problem is ...