Reference request for Unit Clause Based SAT Reduction Rules

Question

I tested my XSAT solver using the 4 pigeons in 3 holes problem converted to XSAT. The pigeon hole instance I give below had 108 variables and 88 clauses after being converted to monotone XSAT. My solver quickly proved the instance was unsatisfiable. While converting the proof back to SAT I realized some of the reductions rules the solver used work for both XSAT and SAT.

My question is if these unit clause propagation based reduction rules are well known. If so, are there any references I can look at?

I will use the SAT version of the XSAT solver proof to show how the reduction rules work.

The 4 pigeons $(A,B,C,D)$ in 3 holes $(1,2,3)$ SAT instance has 12 variables. $A1$ is true if and only if pigeon $A$ is in hole $1$. $D3$ is true only if pigeon $D$ is in hole $3$.

Clauses enforcing every pigeon is in a hole:

$(A1 \lor A2 \lor A3) (B1 \lor B2 \lor B3) (C1 \lor C2 \lor C3) (D1 \lor D2 \lor D3)$

Clauses enforcing no hole has more than one pigeon:

$(\overline {A1} \lor \overline {B1}) (\overline {A1} \lor \overline {C1}) (\overline {A1} \lor \overline {D1}) (\overline {B1} \lor \overline {C1}) (\overline {B1} \lor \overline {D1}) (\overline {C1} \lor \overline {D1})$ $(\overline {A2} \lor \overline {B2}) (\overline {A2} \lor \overline {C2}) (\overline {A2} \lor \overline {D2}) (\overline {B2} \lor \overline {C2}) (\overline {B2} \lor \overline {D2}) (\overline {C2} \lor \overline {D2})$ $(\overline {A3} \lor \overline {B3}) (\overline {A3} \lor \overline {C3}) (\overline {A3} \lor \overline {D3}) (\overline {B3} \lor \overline {C3}) (\overline {B3} \lor \overline {D3}) (\overline {C3} \lor \overline {D3})$

My XSAT solver looks for “Conflict Clusters” which has a very specific meaning in my solver. The SAT reduction rules I am about to describe work for any cluster of SAT clauses, even a “cluster” that has a single clause.

Every clause cluster has a set of satisfying assignments. Call these cluster assignments.

The reduction starts by applying each cluster assignment to the entire instance and performing unit clause propagation. The cluster assignment is “blocked” if unit clause propagation leads to a contradiction. Otherwise, the cluster assignment is unblocked.

For example, the clause $(A1 \lor A2 \lor A3)$ from above has 7 cluster assignments. 4 of these clause assignments lead to contradiction and are blocked. For example, assume $A1$, $A2$, and $A3$ are true. Unit clause propagation causes a contradiction because of:

$(\overline {A1} \lor \overline {B1}) (\overline {A2} \lor \overline {B2}) (\overline {A3} \lor \overline {B3}) (B1 \lor B2 \lor B3)$

The only unblocked cluster assignments are $A1 \overline {A2} \overline {A3}$, $\overline {A1} A2 \overline {A3}$, and $\overline {A1} \overline {A2} A3$.

Reduction Rules:

1. If $A$ is true in every unblocked cluster assignment then $A$ must be true in any satisfying assignment for the instance. Set $A$ to true and reduce the instance.
2. If $A$ is false in every unblocked assignment set $A$ to false and reduce the instance.
3. If $A = B$ in every unblocked assignment replace all occurrences of $B$ with $A$ and all occurrences of $\bar B$ with $\bar A$. Reduce the instance.
4. If $A \neq B$ in every unblocked assignment replace all occurrences of $B$ with $\bar A$ and all occurrences of $\bar B$ with $A$. Reduce the instance.
5. If rule 3 does not apply and in every unblocked assignment $B$ is always true when $A$ is true then $A \rightarrow B$. Add the clause $(\bar A \lor B)$ to the instance. Reduce the instance.
6. If rule 4 does not apply and in every unblocked assignment $B$ is always false when $A$ is true then $A \rightarrow \bar B$. Add the clause $(\bar A \lor \bar B)$ to the instance. Reduce the instance.
7. If a clause assignment is blocked then invert the assignment, put the inverted literals into a clause, and add the learned clause to the instance. Reduce the instance.
8. If all clause assignments are blocked then the instance is unsatisfiable.

All eight rules can be derived from rule 7.

Applying rule 6 to the cluster assignments for $(A1 \lor A2 \lor A3)$ creates:

$(\overline {A1} \lor \overline {A2}) (\overline {A1} \lor \overline {A3}) (\overline {A2} \lor \overline {A3})$

Rule 7 creates these 4 clauses which are all subsumed by the clauses from rule 6:

$(\overline {A1} \lor \overline {A2} \lor \overline {A3}) (A1 \lor \overline {A2} \lor \overline {A3}) (\overline {A1} \lor A2 \lor \overline {A3}) (\overline {A1} \lor \overline {A2} \lor A3)$

Now consider this seven clause cluster.

$(A1 \lor A2 \lor A3) (\overline {A1} \lor \overline {A2}) (\overline {A1} \lor \overline {A3}) (\overline {A2} \lor \overline {A3})$

$(\overline {A1} \lor \overline {B1}) (\overline {A2} \lor \overline {C2}) (\overline {A3} \lor \overline {D3})$

This cluster has 12 cluster assignments. Each of the three assignments for $(A1 \lor A2 \lor A3) (\overline {A1} \lor \overline {A2}) (\overline {A1} \lor \overline {A3}) (\overline {A2} \lor \overline {A3})$ has 4 variations for a total of 12.

All 12 cluster assignments are blocked proving the instance is unsatisfiable.

For example, assume $A1$ is true and all of the other cluster variables are false.

Unit clause propagation causes $C1$ and $D1$ to be false because of $(\overline {A1} \lor \overline {C1}) (\overline {A1} \lor \overline {D1})$. Since cluster variables $C2$ and $D3$ are also false this forces $D2$ and $C3$ to be true because of $(C1 \lor C2 \lor C3) (D1 \lor D2 \lor D3)$.

Having $A1$, $D2$, and $C3$ true causes a contradiction: $(\overline {A1} \lor \overline {B1}) (\overline {B2} \lor \overline {D2}) (\overline {B3} \lor \overline {C3}) (B1 \lor B2 \lor B3)$

Are these unit clause propagation based reduction rules well known? Are there any references I could read?

I think these rules would make a good pre-processor for a SAT solver. Doing unit clause propagation on all seven assignments for each clause could reduce variables, add short learned clauses, and maybe even prove the instance is unsatisfiable.