1SAT

1SAT is the decision problem of determining satisfiability for formulas in which each clause contains exactly one literal, i.e., a conjunction of unit clauses. Such a formula specifies a set of constraints where each constraint requires a particular variable to be true or false. Examples of clauses are x and ¬y; a formula might require x to be true and y to be false simultaneously.

The problem is in P and, in fact, can be solved in linear time in the size of the input. A formula is satisfiable if and only if no variable is forced to be both true and false by the set of unit clauses. If a variable appears only as x or only as ¬x, it may be assigned accordingly; variables not appearing at all are unconstrained and can be set arbitrarily.

A standard algorithm processes the list of unit clauses one by one. It maintains a mapping from each variable to a assigned value (true or false). For each literal:

- if the literal is x, the algorithm requires x to be true; if x was previously assigned false, the formula is unsatisfiable; otherwise x is recorded as true.

- if the literal is ¬x, the algorithm requires x to be false; if x was previously assigned true, the formula is unsatisfiable; otherwise x is recorded as false.

Duplicate literals and repeated constraints are harmless. If the end of the input is reached without a conflict, the formula is satisfiable; any unassigned variables may be given arbitrary truth values.

1SAT is a special case of CNF-SAT and a trivial subset of 2-SAT. It illustrates unit propagation in a very simple setting and is often cited as an example of a problem that remains easy even as SAT-related problems become hard.