SAT Knowledge Base

A Boolean variable has only two possible values: true or false. SAT solvers usually write variables as positive integers, so variable 1 means x1, variable 2 means x2, and so on.

A full assignment gives every variable a value. A partial assignment gives values to only some variables and leaves the rest undecided.

The most common operators are NOT, AND, and OR. From these, one can express implication, equivalence, exclusive-or, at-most-one constraints, and circuit gates.

Example: a implies b is equivalent to NOT a OR b.

A formula is a tree or circuit of Boolean operations. A constraint system is a collection of rules that must all hold. CNF expresses this as a list of clauses that must all be satisfied.

In 1971, Stephen Cook showed that Boolean satisfiability captures the difficulty of every problem in NP. Leonid Levin independently developed closely related ideas. This became known as the Cook-Levin theorem.

A problem in NP is one where a proposed solution can be checked efficiently. SAT is NP-complete because any NP verification process can be encoded as a Boolean formula whose satisfying assignment represents a valid witness.

The theory did not remain abstract. Decades of solver engineering turned SAT into a practical tool for verification, planning, synthesis, automated reasoning, and benchmark-driven research.

• A finite set of Boolean variables, each assigned either true or false.
• A formula built from variables, negation, AND, OR, and sometimes other derived operators.
• In practical solver pipelines, the formula is usually converted into CNF before solving.

• SAT means at least one assignment satisfies the formula.
• A SAT answer normally includes a model, also called an assignment.
• UNSAT means no assignment satisfies the formula.
• A rigorous UNSAT answer should include a proof artifact that can be checked independently.

A formula with n variables has 2^n possible assignments. For 20 variables, that is about one million assignments. For 100 variables, brute force is already astronomically large.

If someone gives a proposed SAT assignment, checking it is straightforward: evaluate each clause. This is why SAT is in NP. The hard part is finding an assignment, or proving none exists.

NP-completeness is a worst-case statement. Many real SAT instances are easy because they contain structure. Others are extremely hard even with modern solvers.

Directly expanding formulas into CNF can become exponentially large. Tseitin transformation avoids that by introducing auxiliary variables for subformulas, producing an equisatisfiable CNF of roughly linear size.

Original subformula:
y <-> (a OR b)

CNF clauses:
(-y OR a OR b)
(y OR -a)
(y OR -b)

Meaning:
If y is true, at least one of a or b must be true.
If a is true, y may be true.
If b is true, y may be true.
Together, these clauses preserve y = (a OR b).

Many applications need statements like "at most one", "exactly one", or "at least k". These can be encoded using pairwise clauses, sequential counters, sorting networks, cardinality networks, or binary encodings.

The best encoding depends on size, propagation strength, and how the solver will use the constraint.

General SAT can use clauses of arbitrary size. 3-SAT restricts clauses to three literals while preserving NP-completeness. This makes it a clean research target and a useful benchmark family.

Long clause:
(a OR b OR c OR d OR e)

One 3-SAT style conversion with auxiliary variables t1 and t2:
(a OR b OR t1)
(NOT t1 OR c OR t2)
(NOT t2 OR d OR e)

The auxiliary variables let the chain carry the remaining choice forward.

Real-world SAT instances are not always pure 3-SAT. Many applications produce mixed clause sizes, but they can still be represented in DIMACS CNF and processed by modern solvers.

A platform can accept general CNF while still emphasizing 3-SAT as a canonical family. Many industrial files are mixed CNF because mixed clause size is more compact and solver-friendly.

For SAT, the solver provides an assignment. Verification is direct: plug the assignment into every clause and check that each clause has at least one true literal.

v 1 2 0
c x1 = true, x2 = true

A SAT answer may include only assigned variables, or it may include all variables. A verifier should treat unassigned variables carefully and validate the assignment against the exact instance file.

For UNSAT, there is no assignment to check. The solver must provide a proof that the formula cannot be satisfied. Common proof formats include DRAT, LRAT, FRAT, and related variants.

Independent proof checking matters because it separates trust in the answer from trust in the solver that produced it.

Without a proof, an UNSAT claim is just a claim. With a proof, a verifier can replay the logical derivation and confirm that contradiction follows from the original CNF.

The Davis-Putnam-Logemann-Loveland procedure searches by choosing a variable assignment, propagating forced consequences, and backtracking when a contradiction is found.

Clauses:
(x1)
(NOT x1 OR x2)
(NOT x2 OR x3)

Step 1: (x1) forces x1 = true
Step 2: (NOT x1 OR x2) now forces x2 = true
Step 3: (NOT x2 OR x3) now forces x3 = true

This chain is unit propagation.

Conflict-driven clause learning extends DPLL by analyzing conflicts and adding learned clauses. A learned clause records why a branch failed and prunes similar branches later.

Solvers rely on variable selection, watched literals, restarts, phase saving, clause deletion, and preprocessing. These engineering choices often decide performance on difficult instances.

• Propagate all currently forced assignments.
• If a conflict appears, analyze it and learn a clause.
• Backjump to a useful earlier decision level.
• If no conflict appears and variables remain, choose a branching variable.
• If all variables are assigned without conflict, return SAT.
• If conflict occurs at decision level zero, return UNSAT.

Suppose decisions A and B forced implications that eventually made a clause false. Conflict analysis finds a compact reason: a learned clause saying "not all of these causes can happen together."

The learned clause is added to the formula. It is logically implied by the original formula, so it does not change satisfiability, but it prevents repeated failure.

Solvers are complex and optimized. A proof checker is usually smaller and more focused. For UNSAT results, a proof checker confirms that the submitted proof derives a contradiction from the original formula.

This is especially important in open markets and scientific datasets: the verifier should not have to trust a solver executable, a participant, or a server. It should be able to verify the artifact.

• DRAT is widely used and supported by classic proof-checking tools.
• LRAT is more explicit, which can make checking simpler and more deterministic.
• FRAT is designed as a flexible proof trace format and can be elaborated into checkable forms.
• Proof pipelines depend on the solver and checker pair used by the verifier.

MaxSAT asks for an assignment that maximizes the number or weight of satisfied clauses. It is used when not all constraints can be satisfied or when soft constraints have different priorities.

Satisfiability modulo theories extends SAT with theories such as arithmetic, arrays, strings, or bit-vectors. An SMT solver combines Boolean search with theory-specific reasoning.

Quantified Boolean formulas add existential and universal quantifiers. QBF can express game-like and adversarial reasoning that plain SAT cannot represent directly.

Constraint satisfaction and CP-SAT systems support higher-level variables and constraints, often compiling parts of the problem into SAT-style reasoning internally.

Pseudo-Boolean constraints use linear inequalities over Boolean variables, such as 2x1 + 3x2 >= 4. These can sometimes be encoded into SAT or solved with specialized methods.

ASP is a logic programming paradigm for combinatorial search. It overlaps with SAT in spirit but uses different modeling abstractions and semantics.

MiniSAT helped define the modern minimal CDCL solver interface. Glucose, Lingeling, CaDiCaL, and Kissat represent major lines of engineering around learned clauses, restarts, and preprocessing.

CryptoMiniSat supports features useful for some structured instances, including XOR-aware reasoning and proof-related workflows. Different solvers can behave very differently on the same formula.

DRAT, LRAT, and FRAT proof pipelines require matching checker tooling. A robust verification workflow should record the proof type, checker version, and exact instance digest.

• Use valid DIMACS CNF syntax.
• Keep comments useful but avoid private information.
• Record how the instance was generated when possible.
• Keep original and standardized versions distinguishable.

• Track variable count, clause count, generator, domain, and benchmark family.
• Use content hashes to detect exact duplicates.
• Use standardized forms to reduce formatting-only duplicates.
• Keep provenance separate from the mathematical instance when needed.

• For SAT, check every clause under the submitted assignment.
• For UNSAT, check the proof against the original formula.
• Store answer artifacts with digests.
• Treat solver output as untrusted until verification succeeds.

For the example with clauses (x1 OR x2), (NOT x1 OR x2), and (x1 OR NOT x2), the assignment x1=true, x2=true satisfies all clauses.

Clause 1 is true because x1 is true. Clause 2 is true because x2 is true. Clause 3 is true because x1 is true. Therefore the whole formula is SAT.

Standardization removes formatting differences that do not change the mathematical instance. This helps detect duplicates when one file has extra spaces, comments, or a different clause order.

3SAT also computes a variable-renamed structure fingerprint with a bidirectional variable mapping. When search finds a solved instance through this structure fingerprint, the downloaded answer bundle is transformed back into the query file's variable numbering.

For SAT, the verifier checks the assignment against the instance. For UNSAT, it selects the correct proof checker for the submitted proof type and verifies that the proof derives contradiction from the original formula.