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?