How often can a clause cause a conflict?

Question

This question is about DPLL+CDCL algorithms. How often can a clause cause a conflict?

I want to use a specific algorithm. Assume a DPLL+CDCL SAT solver using a fixed variable order. Variables and unit clauses are processed from highest order to lowest order. Positive literals are processed before negative literals. For example, if there are multiple unit clauses to be processed then the unit clause with the highest order variable is processed first. If there is both a positive and negative unit clause with this highest order variable then the positive literal is processed first.

One decision variable is set at a time and then all unit clauses are processed one at a time until a conflict is found. When a conflict is found a new learned clause is created. Unlike most CDCL solvers which use first implication learned clauses, assume this solver always creates a learned clause using decision variables.

Since the algorithm processes variables one at a time, any clause that causes a conflict must have been a unit clause before the conflict. Since all unit clauses are processed after every decision variable is set, conflicts can only be caused by processing unit clauses, not by setting a decision variable. This is why I specify the order for processing unit clauses.

By design, when a decision variable is chosen and given a value, all higher order variables must have been assigned a value either as decision variables or because of processing unit clauses. This means the last variable in the unit clause that causes the conflict must be lower order than the decision variable.

When a clause causes a conflict, a new learned clause will be created. All of the variables in this new learned clause must be higher than the lowest order variable is the first (conflicted) clause.

Can I say that a clause can not cause a conflict more than N times, where N is the number of variables in the instance? If not, why not?

Answer 1

This isn’t a great answer. However, it does put an upper bound on how many times a clause can cause a conflict.

Assume a DPLL+CDCL SAT solver using a fixed variable order. Variables and unit clauses are processed from highest order to lowest order. Positive literals are processed before negative literals.

A decision variable is a variable that is assigned a value by the algorithm as opposed to being assigned a value by a unit clause.

The next decision variable is always the highest order unassigned variable. All higher order variables above the current decision variable have been assigned a value. This means all remaining clauses consist of variables lower order or equal to the current decision variable. Also, all remaining clauses have at least two variables since all unit clauses were processed before a new decision variable was chosen.

If more than one conflict is found when a unit clause is processed then a learned clause is created for each conflict (empty clause). The algorithm does not restart and does not delete learned clauses. All learned clauses are derived from the decision variables, not first implication. The decision variable that causes a conflict will always be the lowest order variable in the learned clause.

Since a learned clause is created when a conflict is found, my question is equivalent to asking how many learned clauses can be created from a specific conflict clause.

Let $D$ be the decision level that causes the conflict in the selected clause. The decision level counts how many decision variables have been processed. All unit clauses and conflicts can be associated with a specific decision level.

Assume the worst case where the second lowest order variable in the conflict clause is equal to the decision variable. Also assume all variables higher order than the current decision variables are also decision variables.

The maximum number of learned clauses made from the $D$ highest order variables is $2^D$.

This assumes every learned clause uses all $D$ variables. If we have enough large learned clauses they could reduce to smaller learned clauses. For example, the learned clauses $(x \lor y \lor z)(x \lor y \lor \bar z)$ can be reduced to $(x \lor y)$.

The size of the learned clauses determines how many there can be. Let $S$ be the size of the largest learned clause. Then the maximum number of learned clauses created for a single conflict clause would be $O(D^S)$ where $D$ is the decision level that causes the conflict and $S$ is the size of the largest learned clause.

Smaller learned clauses reduce the number of times a clause can cause a conflict.