blocking clauses

Concept

Blocking clauses are clauses added to a propositional formula to rule out previously enumerated solutions (typically models or partial models), commonly used in AllSAT/enumeration and SAT-based witness generation. They enable exponential reductions in the number of generated models but can increase memory consumption and slow unit propagation. Related but distinct notions include blocked clauses (a syntactic redundancy notion in SAT/QBF/DQBF) and blocking clauses used in uniform witness generators such as UniGen.

First seen 7/26/2026

Last seen 7/26/2026

Evidence 2 chunks

Wiki v1

WIKI

Definition and Purpose

In propositional satisfiability (SAT), a blocking clause is a clause added to a working formula in order to rule out a solution (model, or partial model) that has already been found, so that the solver or enumerator does not produce the same solution again. A basic algorithm for enumerating disjoint propositional models (disjoint AllSAT) is built on adding blocking clauses incrementally after each found model.

Blocking clauses can act on partial models, which gives them the potential to reduce the number of generated models exponentially compared to blocking clauses over full models. However, the same accumulation that makes them powerful has well-known drawbacks:

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

1 connections

UniGen ← uses 95% 1e

UniGen's BSAT implementation uses blocking clauses restricted to the independent support variables.

LINKED ENTITIES

1 links

UniGen USES Extracted graph relationship

CITATIONS

6 sources

6 citations — click to expand

[1] A basic disjoint-AllSAT algorithm adds blocking clauses incrementally to rule out previously found models. Disjoint Partial Enumeration without Blocking Clauses

[2] Blocking clauses can reduce the number of generated models exponentially by handling partial models, but accumulating many blocking clauses increases memory consumption and drastically slows down unit propagation. Disjoint Partial Enumeration without Blocking Clauses

[3] UniGen's improved efficiency over UniWit stems in part from shorter blocking clauses (and xor-clauses) that use only variables from the independent support. Balancing Scalability and Uniformity in SAT Witness Generator

[4] On benchmark 'tutorial3', UniWit's BSAT calls with large blocking clauses timed out, while UniGen's calls succeeded due to short blocking clauses over the independent support. Balancing Scalability and Uniformity in SAT Witness Generator

[5] UniGen amortizes the cost of finding a good value of m over multiple samples, while UniWit requires more than 20,000 seconds on average per witness on benchmark 's953a_3_2'. Balancing Scalability and Uniformity in SAT Witness Generator

[6] Blocked clauses (a related redundancy notion in propositional logic) are defined by a syntactic criterion that guarantees they are redundant, and the notion has been lifted to first-order logic. Blocked Clauses in First-Order Logic