Incremental Inprocessing Rules beyond Resolution

Abstract

Formula simplification in the form of pre- and inprocessing is a crucial part of modern SAT solvers. While most inprocessing techniques focus on eliminating redundant clauses, significant performance improvements have recently been achieved with clause addition techniques. However, not all inprocessing techniques can be employed in incremental use cases. In particular, combining incremental reasoning with clause addition techniques based on more general redundancy properties in a sound and eficient way is an open challenge. In this paper, we extend the incremental inprocessing calculus for SAT solvers to facilitate some of these clause addition techniques and reason about the soundness and completeness of such systems. The resulting framework formally defines suficient conditions for eficiently implementing in incremental SAT solvers such beyond resolution techniques, including Bounded Variable Addition (BVA) and certain Blocked Clause Addition (BCA) steps.

Keywords

• eol>Incremental SAT
• Inprocessing
• Bounded Variable Addition

1. Introduction

Modern SAT solvers often implement a diverse repertoire of diferent inprocessing techniques in an efort to simplify the notoriously complex NP-complete decision problems they seek to solve. Most of these techniques focus on reducing the search space by eliminating certain redundant parts of the formula while preserving its satisfiability. Some notable examples include Blocked Clause Elimination (BCE) [ 1 ], Bounded Variable Elimination (BVE) [ 2 ], and Equivalent Literal Substitution (ELS) [ 3, 4, 5, 6 ]. In contrast to these techniques, other approaches focus on introducing redundant clauses and new variables in a way that preserves satisfiability, rather than eliminating them (see for example [ 7, 8, 9 ]). Such clause addition techniques gained renewed attention after SBVA-CaDiCaL [ 10 ] won the SAT Competition in 2023 [ 11 ]. This winner tool combined CaDiCaL, a modern state of the art SAT solver, with an eficient implementation of Bounded Variable Addition (BVA) [ 12 ] as a preprocessing technique. Beyond BVA, many other clause addition techniques, such as Blocked Clause Addition (BCA) [ 13 ] and reasoning over cardinality constraints [ 9 ] or decision diagrams [ 7 ], require a proof system based on some form of extended resolution [ 14, 15, 16 ] to certify. Nevertheless, an abstract framework that captures in a unified way and reasons about the usual inprocessing techniques of SAT solvers, including both clause addition and elimination techniques, was introduced by Järvisalo et al. in [ 17 ].

There are many use cases for SAT solvers, for example in model checking [ 18 ], or in sub-reasoning steps of MaxSAT [ 19 ] and Satisfiability modulo Theories (SMT) solvers [ 20, 21 ], where a sequence of similar SAT problems are solved rather than a single decision problem. Such use cases can greatly benefit from incremental SAT solving [ 22, 23 ] where the results of previous solver runs can be reused during reasoning, potentially avoiding much repeated work. However, in order to be able to reuse the previous solver steps, formula simplification in incremental SAT solvers requires additional care [ 24 ]. Nadel at al. [ 25 ] showed how to handle certain clause elimination techniques in incremental solvers. A refinement of the inprocessing rules for incremental use cases was introduced in [ 26 ], where all clause elimination techniques are supported, but only implied clauses can be learned. In this paper, we extend the incremental inprocessing rules of [ 26 ] so that clause addition techniques based on extended resolution [ 15, 16 ] are enabled. This extension allows to capture on an abstract level incremental inprocessing in the presence of a variety of clause addition techniques, including forms of BVA, BCA and extended resolution.

The paper is organized as follows: Section 2 provides an overview of the used notation and background, while Section 3 presents our new derivation rule that captures clause addition techniques based on more general redundancy properties and reasons about its correctness. In Section 4 we illustrate the use of the new calculus and Section 5 concludes the paper.

2. Preliminaries

Boolean Satisfiability We assume the standard semantics and syntax of propositional logic and its decision problem (SAT). Given a set of Boolean variables , a propositional formula over in conjunctive normal form is a conjunction of clauses, where each clause is a disjunction of literals and a literal is a Boolean variable or its negation. A (partial) truth assignment over a set of variables is a set of non-contradicting literals over . An assignment satisfies (resp. falsifies) a literal if ∈ (resp. ¬ ∈ ). If neither ∈ nor ¬ ∈ , then the literal is unassigned and the truth assignment is partial. A clause is satisfied by a truth assignment if at least one of its literals is satisfied. A truth assignment satisfies a CNF formula , noted as ( ) = ⊤, if it satisfies every clause of it. We use 1 ∘ 2 to denote the composition of truth assignments 1 and 2, i.e., ( 1 ∘ 2) ( ) = 1( 2( )). Note that if ( 1) ∩ ( 2) = ∅, then ( 1 ∘ 2) ( ) = 1( 2( )) = 2( 1( )) = ( 2 ∘ 1) ( ). Incremental SAT Instead of solving a single satisfiability problem, we are interested in solving a sequence of SAT formulae ⟨ 0, 1, . . . , ⟩ over a global variable set Γ ⊆ , where each formula extends the previous one with new clauses, i.e., starting from an initial SAT problem 0, for each phase = 0 . . . − 1 we have that +1 = ∧ Δ+1 over the variable set Γ. As each phase extends the previous formula with further clauses, if is unsatisfiable, then for all > is unsatisfiable as well. Incremental SAT solvers also support assumptions, literals temporarily assumed to be true in a given phase. In practice they are frozen variables [ 23, 24 ], thus we do not consider them explicitly in this paper.

Existentially Quantified SAT We further introduce Λ ⊆ , a (suficiently large) set of latent Boolean variables, s.t. Γ ∩ Λ = ∅. Given a SAT problem over = Γ ∪ Λ, we denote with ∃Λ ( ) the quantified Boolean formula (QBF) where all Λ-variables are existentially quantified, all Γ-variables are free and the formula matrix is . Further, we assume every truth assignment to be a total function over Λ and Γ, unless stated otherwise. For an introduction of standard QBF syntax and semantics, see for example [ 27 ], while here we define explicitly the most relevant related concepts that are used throughout this paper. Definition 1 (Projected satisfaction). Let be a truth assignment over Γ, we say that satisfies ∃Λ ( ) if there exists a truth assignment over Λ, such that ( ∘ ) ( ) = ⊤.

Definition 2 (Projected implication). Given a formula and a clause , both over variables Γ ∪ Λ, we say that Λ-implies , denoted as |=Λ , if all satisfying truth assignments (according to Def. 1 over Γ) of ∃Λ ( ) satisfy ∃Λ ( ∧ ) as well.

Definition 3 (Projected equivalence). Given formulas and over variables Γ ∪ Λ, we say that is logically equivalent to under Λ, denoted as ≡ Λ , if exactly the same truth assignments over Γ satisfy ∃Λ ( ) and ∃Λ ().

In other words, for all over Γ s.t. there exists over Λ with ( ∘ ) ( ) = ⊤, it holds that there exists also a ′ over Λ s.t. ( ∘ ′) () = ⊤. Note that and ′ can be diferent, but in certain cases they are the exact same truth assignment, as the following proposition shows. Proposition 4. Given a formula and a clause over Γ ∪ Λ, if |= , then both |= ∃Λ ( → ) and |=Λ holds.

The following proposition makes explicit the relation between projected equivalence and implication. Notice that projected equivalence and implication are both transitive properties, i.e., if ≡ Λ and ≡ Λ , then ≡ Λ (resp. if |=Λ and |=Λ , then |=Λ ).

Proposition 5. Given a formula and a clause over Γ ∪ Λ, |=Λ if ≡ Λ ∧ .

Though these definitions and propositions first may seem to be straightforward, they include several subtle details that were refined and exploited through a long line of previous research, see for example in [ 28, 29, 30, 31, 32, 33 ].

Incremental Inprocessing This paper extends the incremental inprocessing calculus that was introduced in [ 26 ] and later slightly refined in [ 34, Section 6.3]. To make the paper more self contained, here we sum up the most important terminology and notation with minor adjustments to our current concerns. Formula pre- and inprocessing steps are concerned about eficiently identifying redundant clauses (see Def. 7), that we define based on the most general redundancy property introduced in [ 35 ]. To make explicit the reason of found redundancies when it is necessary, we use the notion of witness labelled clauses (see Def. 6).

Definition 6 (Witness Labelled Clause [ 26 ]). A set of literals and a clause such that ∩ ̸= ∅ is called a witness labelled clause and written as ( : ).

Definition 7 (Redundancy [ 26, 35 ]). A witness labelled clause ( : ) is redundant w.r.t. a formula if () = ⊤ and |¬ |= |¬∘ . This is also denoted as ∧ ≡ .

As Def. 7 indicates, adding or removing redundant clauses is satisfiability preserving. Moreover, knowing the witness of removed redundant clauses allows to transform a solution of the simplified formula to a solution of the removed redundant clauses as well. Note that we use a stronger definition |¬ |= |¬∘ (essentially the same as in [ 36 ]) instead of the original version |¬ |= | [ 35 ] used in [ 26 ], as solution reconstruction otherwise requires larger witnesses, as the following example shows. Example 8 (Total Models and Variable Elimination). Consider the clauses ( ∨ ) ∧ (¬ ∨ ¬). Variable elimination on would find that both clauses are redundant. However, using only (resp. ¬) as a witness does not satisfy the original redundancy criteria. One could always extend the witness to set all variables of the clause, which however “taints” more literals than necessary ( cf. “clean condition” of Restore in Fig. 1).

Example 8 was observed in a formalization of (non-incremental) reconstruction in Isabelle as part of a Master thesis [ 37 ]. It is not a counterexample to incremental model reconstruction [ 26 ] (proofs remain correct and transfer to the stronger version) but it shows that the original redundancy criteria is not strong enough to cover the implementation in CaDiCaL. Practically it means that solution reconstruction needs to work with total assignments and has to assign all variables initially and not on-the-fly during the reconstruction procedure. Lemma 9 (Satisfying Redundant Clauses). Assume ≡ ∧ and let be a total assignment over Λ ∪ Γ s.t. ( ) = ⊤ and () = ⊥. Then, ( ∘ ) ( ∧ ) = ⊤.

Proof Sketch. Very similar to the original proof in [ 26 ], but the stronger ∘ = (where = ¬) holds and therefore vanishes everywhere in the proof.

Due to the refinement in Def. 7, hereafter we assume found models to be total. This change only makes proofs easier, because the assumption is stronger than in the original reconstruction. In practice, SAT solvers most often stop their search only once every variable was assigned without a conflict, thus this change does not have practical consequences. [ ] [ ∧ ]

Learn−

♯ ∧ [ ] [ ] · ( : ) ♭

Weaken+ [ ∧ ] [ ]

Forget ∧ [ ] [ ]

Drop [ ∧ ] ∧ [ ]

Strengthen ø [ ] · ( : ) · ′ ∧ [ ] · ′

Restore where ♯ is ∧ |= , ♭ is ∧ ≡ , ø is |= , is is clean w.r.t. ′ and ℐ is that vars(Δ) ⊆ Γ and each clause in Δ is clean w.r.t. . removed redundant clauses are stored. Given a sequence of incremental SAT problems ⟨ 0, 1, . . . , ⟩ over a set of variables Γ, the derivation starts from the initial state ∅ [ ∅ ] and the possible derivation rules, together with their corresponding side conditions defining when a rule is actually applicable, are shown in Fig. 1.

A clause can be removed from the irredundant clause database in two cases: (i) when it is implied by all the other clauses in , and in that case the clause can be completely deleted (see Drop), or (ii) when it is redundant w.r.t. (see Weaken+), and in that case it is moved to the end of the reconstruction stack. Reintroducing a clause from the reconstruction stack into via Restore requires to first restore all those clauses from the stack that could have not been removed from if was present. To recognize a superset of such clauses, we use the notion of clean clauses: Definition 10 (Clean Clauses [ 26 ]). A clause is clean w.r.t. a sequence of witness labelled clauses if for all ( : ) ∈ we have that ¬ ∩ = ∅.

Redundant clauses can be either deleted by Forget or moved to the irredundant set by Strengthen at any point of time. A new redundant clause can be learned by Learn− when it is implied by the formula ∧

(see ♯ ). Note that though this step captures learning clauses derived by resolution during a new phase + 1 starts from [

] by adding Δ+1 to . conflict analysis, it does not support clause addition techniques based on more general redundancies.

Rule AddClauses captures when users add new clauses to the problem (i.e., when a new solving phase starts). In that case, before applying AddClauses, all previously done relevant clause elimination steps must be undone (via Restore) relying again on the notion of clean clauses (see ℐ ). Further, in contrast to the original calculus, here we make explicit the set of variables on what the formulas are defined ( Γ). As we will discuss it later, this refinement of ℐ simplifies our reasoning but does not necessarily afect user experience. That is, it is not required to know ahead of time which variables will reoccur in clauses that are added later. In the next sections we will refer to derivation of state +1 [ +1 ] +1 from [ ] for each 0 ≤ < in each phase = 0, . . . , and of steps where

We use the following revised1 version of reconstruction function definition that captures solution reconstruction proposed by Järvisalo et al. [ 38 ] of inprocessing SAT solvers.

Definition 11 (Reconstruction Function [ 34 ]). Given a truth assignment and a witness labelled clause ( : ) the reconstruction function is defined as ℛ(:)( ) = {︃ ( ∘ ) if () = ⊤ otherwise. 1Christoph Scholl proposed this simplified version of the reconstruction function while working on [ 26 ]. [ ] [ ∧ (ℓ ∨ ) ] Σ

Extend where Σ is that ℓ ∈ Λ (and so ℓ ̸∈ Γ) and

ℓ ∧ ∧ ≡ ∧ ∧ ∧ (ℓ ∨ ) holds.

The reconstruction function for a sequence of witness labelled clauses is defined as ℛ = ℛ(1:1)· ...· (:) = ℛ(1:1) ∘ · · · ∘ ℛ (:).

ℛ = id and

Notice that from this definition, due to the associativity of function composition, it immediately follows that for a given truth assignment and a sequence of witness labelled clauses · ′ we have that ℛ · ′ ( ) = ℛ (ℛ ′ ( )), while in [ 26 ] it required an additional lemma.

The following lemma will help us to show the correctness of solution reconstruction in our extended calculus. For more details on the incremental inprocessing calculus and for a proof of this lemma, see [26, 34, Section 6.3].

Lemma 12 (Clean Reconstruction [ 26 ]). If a clause is clean w.r.t. a sequence of witness labelled clauses , then for all truth assignments with () = ⊤ we have that ℛ ( )() = ⊤.

3. Incremental Inprocessing with Blocked Clause Addition

While the original (non-incremental) inprocessing calculus of [ 17 ] allows learning arbitrary redundant clauses (based on RAT or even more general redundancy properties), the incremental extension of it supports only implied clauses to be learned via Learn− (see Fig. 1).

In Fig. 2 we introduce a new possible step, called Extend, that enables learning clauses based on a more general redundancy property but only in very specific cases: (1) the redundancy has to hold w.r.t. every part of the formula, including those clauses that are currently on the reconstruction stack, and (2) the redundancy has to be witnessed by a single latent literal. Though the requirements of Extend are very specific, it captures several clause addition techniques, such as BVA, BCA and extended resolution (see Sect. 4 for some examples). Note that these techniques could be simulated without Extend, by simply adding the learned clauses as user input via AddClauses. However, then the added clauses are part of the irredundant clause database (making it harder to eliminate them) and the reconstruction stack has to be first cleaned with Restore steps (see ℐ ). In contrast to that, Extend adds the new clauses as redundant (just as Learn− ) and no Restore steps are necessary before applying it. Preprocessing steps of users (and wrapping systems) can continue using AddClauses, while Extend captures the internal inprocessing steps that are witnessed by the internal latent variables. That is, latent variables are private and only help the reasoning of the SAT solver, while users can only use and reuse any of the Γ-variables. In practice, when users need a fresh variable, it has to be made sure that it is not used already as a latent variable internally in the solver.

Now we show that it is correct to combine Extend with the other steps of an incremental solver (see Fig. 1), as long as the latent variables remain unused by the user (see ℐ ). First, see that learning by Extend is satisfiability preserving and their solution is reconstructible.

Lemma 13. Assume ≡ ∧ ( ∨ ) and let be a total assignment over Γ ∪ Λ s.t. ( ) = ⊤ and ( ∨ ) = ⊥. Then, ( ∘ ) ( ∧ ( ∨ )) = ⊤.

Proof. Follows from Lemma 9 (note that is assumed to be total, as discussed at Example 8).

Allowing redundant but not implied clauses to be learned means that the redundant clauses are not logical consequences of the irredundant and eliminated ones any more. However, as the following lemmas show, a projected implication still holds in the new calculus. Lemma 14. If ≡ ∧ ( ∨ ) where ∈ Λ, then |=Λ ( ∨ ).

Proof. Assume = ( ∘ ) is a total assignment over Γ ∪ Λ s.t. ( ) = ⊤. Then either also ( ∘ ) ( ∧ ( ∨ )) = ⊤ holds, or by Lemma 13, we know that ( ∘ ( ∘ )) ( ∧ ( ∨ )) = ⊤. Thus, whenever there exists a truth assignment over Λ s.t. ( ∘ ) ( ) = ⊤, there exists a truth assignment ′ s.t. ( ∘ ′) ( ∧ ( ∨ )) = ⊤ by defining ′ either as or as ( ∘ ).

Lemma 15. Starting from the initial state, in any reachable state [ ] , the property ∧ |=Λ ∧ ∧ holds.

Proof. We prove it by induction on the length of the derivation. In the initial state the property trivially holds ( 00 = ∅ without Λ variables and both 00 and 00 are empty). Assuming that ∧ |=Λ holds, we show the induction step by a case distinction on the next applied rule. Rules Weaken+ and Restore only move a clause between and , AddClauses only strengthens ∧ , while Forget only weakens , thus in these cases the property is trivially maintained. With Drop a clause is removed from , but ∖ {} ≡ is ensured by ø . Rule Strengthen weakens by moving a clause of it to , thereby also strengthens ∧ , thus the property is maintained. When a clause is learned by Learn− from the inductive assumption we know that for any truth assignment over Γ if there exists a over Λ s.t. ( ∘ ) ( ∧ ) = ⊤, then there exists a ′ over Λ s.t. ( ∘ ′) ( ∧ ∧ ) = ⊤. Since ∧ ∧ |= (due to ♯ ), we know that ( ∘ ′) ( ∧ ∧ ∧ ) = ⊤ holds as well. When the new Extend rule is applied, one needs to show that ∧ |=Λ ∧ ∧ ∧(∨). Let be a truth assignment over Γ s.t. there exists a over Λ s.t. ( ∘ ) ( ∧ ) = ⊤. Then, from the ind. assumption follows that there also exists a truth assignment ′ s.t. ( ∘ ′) ( ∧ ∧ ) = ⊤ holds. And since ∧ ∧ |=Λ ( ∨ ) (due to Σ and Lemma 14), we know that then there exists as well a ′′ s.t. ( ∘ ′′) ( ∧ ∧ ∧ ( ∨ )) = ⊤.

From the projected implication established in Lemma 15, it can be shown that there is a projected equivalence maintained by every step of our calculus.

Lemma 16. In any derivation in our calculus starting from the initial state the property ∧ ≡ Λ +1 ∧ +1 holds in each phase = 0 . . . and for each with 0 ≤ < .

Proof. By induction over the transition, ignoring the indices and . Only rules Strengthen and Drop change the combined formula ∧ . However, Strengthen strengthens with an Λ-implied clause (due to Lemma 15), while Drop guarantees logical equivalence by ø .

Lemma 17. In any derivation starting from the initial state, if no input clauses contain latent variables then the property |=Λ 0 ∧ 0 ≡ Λ 1 ∧ 1 ≡ Λ · · · ≡ Λ ∧ holds.

Proof. Since the input clauses have no Λ-variables, for all 0 ≤ ≤ it holds that Δ ≡ ∃ Λ (Δ) and so for any formula , we have that ∃Λ ( ) ∧ Δ ≡ ∃ Λ ( ∧ Δ). Further, from Lemma 16 follows that 0 = 00 ∧ ≡ Λ · · · ≡ Λ 00 ∧ 00 . Now, by an inductive argument and by Lemma 16, we get that +1 = ∧ Δ+1 ≡ Λ ∧ ∧ Δ+1 = 0+1 ∧ 0+1 ≡ Λ · · · ≡ Λ ++11 ∧ ++11 .

As a corollary, we get that the learned clauses can be kept even after new clauses were added, as long as users are not using latent variables.

Corollary 18. If no input clauses contain latent variables then +1 |=Λ holds.

What remains to show is that solution reconstruction works as before in our extended calculus. For that, we use a refined definition of reconstruction property from [34, Sect. 6.3].

Definition 19 (Reconstruction Property [ 34 ]). A state [ ] satisfies the reconstruction property w.r.t. a formula if for all total truth assignment over Γ ∪ Λ satisfying , the result of the reconstruction function ℛ ( ) is a satisfying assignment of . Theorem 20. Starting from the initial state, in any reachable state [ ] , the reconstruction property holds w.r.t. .

Proof Sketch. Relying on our refined definitions and lemmas (Def. 11, Lemma 12, and Lemma 9), it can be shown by induction that every step (including Extend) maintains the property. The proof remains technically the same as in [ 34 ] (see in Appendix). ≡ ∧ holds.

Putting everything together, we get our final lemma showing that the incremental calculus with Extend is correct.

Theorem 21 (Correctness). Starting from the initial state, in any reachable state [ ] , the property Proof. If ∧ is satisfiable, then is also satisfiable due to Thm. 20. From Lemma 15 follows that if ∧ is unsatisfiable, then is unsatisfiable as well, and then, due to Lemma 17, must be unsatisfiable too.

4. Discussion

The following example illustrates how our extended calculus can capture BCA and thereby for example BVA or other forms of extended resolution.

Example 22. Let 0 = ( ∨ ) ∧ ( ∨ ) ∧ ( ∨ ) ∧ ( ∨ ) be the first formula to be solved. Once all clauses are added (via AddClauses), the derivation starts with 0 [ ∅ ] . Assume that the solver decides to introduce a new latent variable , with the definition ( ↔ (¬ ∨ ¬)). For that, it needs to add (in an arbitrary order) the following three blocked clauses: {( ∨ ), ( ∨ ), (¬ ∨ ¬ ∨ ¬)}. Since , ¬ ̸∈ 0 and the reconstruction stack is empty, we can see that each clause fulfils Σ hence applying Extend thrice can lead to a state 0 [ ( ∨ ) ∧ ( ∨ ) ∧ (¬ ∨ ¬ ∨ ¬) ] . Now, the clauses ( ∨ ¬) and ( ∨ ¬) are both implied and so can be learned via Learn− . With Strengthen the solver can move some of the learned clauses, leading to a state 0 ∧ ( ∨ ) ∧ ( ∨ ) ∧ ( ∨ ¬) ∧ ( ∨ ¬) [ (¬ ∨ ¬ ∨ ¬) ] . Now Drop can be used to drop all clauses of 0 and Forget can also remove the remaining redundant definition clause. As a result, we get ( ∨ ) ∧ ( ∨ ) ∧ ( ∨ ¬) ∧ ( ∨ ¬) [ ∅ ] . At that point, since the reconstruction stack is empty, arbitrary -free clauses can be added via AddClauses.

Here the solver fully defined the meaning of the new latent variable (by learning three blocked clauses), but in theory it would have been correct to learn only some of these clauses.

A further interesting insight is that our calculus ensures that the solved formula remains satisfiability equivalent and solution reconstruction gives a model to the original problem. However, as the next example shows, the final value of the latent variables is not defined.

Example 23. Assume that we start with a formula consisting of a single unit clause, i.e., 0 = () and so the initial state is {} [ ∅ ] . Assume, the solver uses Weaken+ to remove the only clause of the formula, ending in the state ∅ [ ∅ ] ( : ). Then, the solver can learn via Extend the clause ( ∨ ¬) witnessed by , where ∈ Λ, yielding the state ∅ [ {( ∨ ¬)} ] ( : ). Now, by Strengthen, the clause can be moved to the irredundant set, resulting in the state {( ∨ ¬)} [ ∅ ] ( : ). Then, starting from the initial solution = {¬, ¬}, solution reconstruction results in a model of the input formula = {¬, }. However, while that the solution satisfies 0, it falsifies the clause learnt by Extend.

This result is not too surprising, as our extended calculus is based on projected implication, i.e., we only claim that there exists an extension of the solution to the latent variables, while the actual value of these variables is not considered. Similarly, the original non-incremental calculus of [ 17 ] does not guarantee that clauses added by the solver are satisfied after solution reconstruction.

5. Conclusion and Future Work

The main motivation behind this paper was our intention to implement and combine BVA with the incremental features of CaDiCaL [ 39 ]. Though intuitively this should work without much complications, we had to establish in theory that our implementation is actually correct. Thus, here we introduced an extension of the incremental inprocessing calculus [ 26 ] with a new rule that allows learning in certain cases based on more general redundancies.

The new framework supports only single witness literals, extending it to more general witnesses, that is necessary to capture super-blocked clauses [ 13 ] and other PR-based techniques [ 35, 40, 41 ], remains future work. Further, note that our calculus captures only the internal inprocessing steps of the solver and does not allow users to interfere with it. A more general learning mechanism (as it is available in the non-incremental inprocessing calculus [ 17 ]) remains intriguing future work.

Acknowledgments

This work was supported in part by the Austrian Science Fund (FWF) under project T-1306, the state of Baden-Württemberg through bwHPC, the German Research Foundation (DFG) through grant INST 35/1597-1 FUGG, and by a gift from Intel Corporation.

Declaration on Generative AI

During preparation, the authors used DeepL and Mistral-AI to check the grammar and spelling of this work. After using these tools and services, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content.

A. Proof of Theorem 20

Theorem 20. Starting from the initial state, in any reachable state [ ] , the reconstruction property holds w.r.t. .

Proof. In the initial state , = 0, 00 = 0, 00 = , and so for any total satisfying assignment of 0, ℛ( )( 0) = ( 0) = ⊤. Assume that in a state of a phase (where 0 ≤ < and 0 ≤ ≤ ), the reconstruction property w.r.t. holds, i.e., for all complete assignment over Γ ∪ Λ if ( ) = ⊤, then ℛ ( )( ) = ⊤. Now, we need to show that for any total if ( +1) = ⊤ holds, then ℛ +1 ( )( ) = ⊤ holds as well. Note that is not changed by any steps of the calculus (AddClauses starts a new phase and is increased). Rules Learn− , Forget, and Extend do not change nor , thus the property remains true. In case of rule Drop, it follows from ø , that if ( +1) = ⊤ then ( +1 ∧ ) = ⊤ as well, thus ℛ +1 ( )( ) = ⊤ holds by induction, and similarly for Strengthen with +1 = ∧ .

For Weaken+, consider a total truth assignment ′ over Γ ∪ Λ s.t. ′( +1) = ′( ∖ ) = ⊤. If ′() = ⊤, then ′( ) = ⊤, thus ℛ ( ′)( ) = ⊤ by induction. Further, in that case from Def. 11 follows that ℛ +1 ( ′) = ℛ · (:)( ′) = ℛ ( ′) since ′() = ⊤. If ′() ̸= ⊤, then ′() = ⊥ as ′ is total. From ♭ , Lemma 12, and Lemma 9 follows that ( ′ ∘ ) ( ) = ⊤ and so by induction ( ′ ∘ is still total over Γ ∪ Λ), ℛ ( ′ ∘ )( ) = ⊤ where ℛ ( ′ ∘ ) = ℛ · (:)( ′) since ′() ̸= ⊤. Thus, ℛ · (:)( ′)( ) = ℛ +1 ( ′)( ) = ⊤.

Assume Restore is applied, where = · ( : ) · ′. Then for any ′ s.t. ′( +1) = ⊤ we have that ′() = ⊤ and ′( ) = ⊤ since +1 = ∧ . Further, from Def. 11 follows that ℛ +1 ( ′) = ℛ · ′ ( ′) = ℛ (ℛ ′ ( ′)). As is clean w.r.t. ′ (by ), from Lemma 12 follows that ℛ ′ ( ′)() = ⊤, thus ℛ (ℛ ′ ( ′)) = ℛ · (:)(ℛ ′ ( ′)) = ℛ · (:)· ′ ( ′) (again by Def. 11), which is actually ℛ ( ′) where by induction the property holds.

When a new phase starts via AddClauses (i.e., 0 ≤ < and = ), formula is extended with a set of clauses Δ+1. Let ′ be a total assignment over Γ ∪ Λ s.t. ′( ∧ Δ+1) = ′( 0+1) = ⊤. Note that ℛ 0+1 ( ′) = ℛ ( ′) as AddClauses does not change the reconstruction stack. By the inductive assumption we have that ℛ ( ′)( ) = ⊤. Further, as +1 = ∧ Δ+1, where each clause of Δ+1 is clean w.r.t. (by ℐ ), from Lemma 12 follows that ℛ ( ′)(Δ+1) = ℛ 0+1 ( ′)(Δ+1) = ⊤ as well. Thus, ℛ ( ′)( ∧ Δ+1) = ℛ 0+1 ( ′)( +1) = ⊤.

References

[1] M. Järvisalo , A. Biere , M. Heule , Blocked clause elimination , in: J. Esparza , R. Majumdar (Eds.), Tools and Algorithms for the Construction and Analysis of Systems , 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010 , Paphos, Cyprus, March 20 -28, 2010 . Proceedings, volume 6015 of Lecture Notes in Computer Science, Springer, 2010 , pp. 129 - 144 . doi: 10 .1007/978-3- 642 -12002-2\_ 10 .

[2] N. Eén , A. Biere , Efective preprocessing in SAT through variable and clause elimination , in: F. Bacchus, T. Walsh (Eds.), Theory and Applications of Satisfiability Testing , 8th International Conference, SAT 2005, St . Andrews, UK , June 19-23, 2005 , Proceedings, volume 3569 of Lecture Notes in Computer Science, Springer, 2005 , pp. 61 - 75 . doi: 10 .1007/11499107\_5.

[3] B. Aspvall , M. F. Plass , R. E. Tarjan , A linear-time algorithm for testing the truth of certain quantified Boolean formulas , Inf. Process. Lett. 8 ( 1979 ) 121 - 123 . doi: 10 .1016/ 0020 - 0190 ( 79 ) 90002 - 4 .

[4] A. Van Gelder , Y. K. Tsuji , Satisfiability testing with more reasoning and less guessing , in: D. S. Johnson, M. A. Trick (Eds.), Cliques, Coloring, and Satisfiability , Proceedings of a DIMACS Workshop , New Brunswick, New Jersey, USA, October 11 - 13 , 1993 , volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science , DIMACS/AMS, 1993 , pp. 559 - 586 .

[5] C. M. Li , Integrating equivalency reasoning into Davis-Putnam procedure , in: H. A. Kautz , B. W. Porter (Eds.), Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on on Innovative Applications of Artificial Intelligence, July 30 - August 3 , 2000 , Austin, Texas, USA., AAAI Press / The MIT Press, 2000 , pp. 291 - 296 .

[6] A. del Val , Simplifying binary propositional theories into connected components twice as fast , in: R. Nieuwenhuis , A . Voronkov (Eds.), Logic for Programming , Artificial Intelligence, and Reasoning , 8th International Conference, LPAR 2001, Havana, Cuba, December 3- 7 , 2001 , Proceedings, volume 2250 of Lecture Notes in Computer Science, Springer, 2001 , pp. 392 - 406 . doi: 10 .1007/3-540-45653-8_ 27 .

[7] R. E. Bryant , M. J. H. Heule , Generating extended resolution proofs with a bdd-based SAT solver , ACM Trans. Comput. Log . 24 ( 2023 ) 31 : 1 - 31 : 28 .

[8] J. E. Reeves , M. J. H. Heule , R. E. Bryant , Preprocessing of propagation redundant clauses , J. Autom. Reason . 67 ( 2023 ) 31 .

[9] J. E. Reeves , M. J. H. Heule , R. E. Bryant , From clauses to klauses, in: CAV (1) , volume 14681 of Lecture Notes in Computer Science, Springer, 2024 , pp. 110 - 132 .

[10] A. Haberlandt , H. Green , SBVA-CaDiCaL and SBVA-Kissat: Structured bounded variable addition , in: T. Balyo, N. Froleyks , M. J. H. Heule , M. Iser , M. Järvisalo , M. Suda (Eds.), Proc. of SAT Competition 2023 - Solver and Benchmark Descriptions , volume B- 2023 -1 of Department of Computer Science Report Series B, University of Helsinki, 2023 , p. 18 .

[11] T. Balyo , M. J. H. Heule , M. Iser , M. Järvisalo , M. Suda (Eds.), Proceedings of SAT Competition 2023 : Solver, Benchmark and Proof Checker Descriptions , Department of Computer Science Series of Publications B, Department of Computer Science, University of Helsinki, Finland, 2023 .

[12] N. Manthey , M. Heule , A. Biere , Automated reencoding of boolean formulas , in: A. Biere , A. Nahir , T. E. J. Vos (Eds.), Hardware and Software: Verification and Testing - 8th International Haifa Verification Conference, HVC 2012 , Haifa, Israel, November 6- 8 , 2012 . Revised Selected Papers , volume 7857 of Lecture Notes in Computer Science, Springer, 2012 , pp. 102 - 117 . URL: https://doi.org/10.1007/978-3- 642 -39611-3_ 14 . doi: 10 .1007/978-3- 642 -39611-3\_ 14 .

[13] B. Kiesl , M. Seidl , H. Tompits , A. Biere , Super-blocked clauses , in: IJCAR , volume 9706 of Lecture Notes in Computer Science, Springer, 2016 , pp. 45 - 61 .

[14] G. S. Tseitin , On the Complexity of Derivation in Propositional Calculus , Springer Berlin Heidelberg, Berlin, Heidelberg, 1983 , pp. 466 - 483 . URL: https://doi.org/10.1007/978-3- 642 -81955-1_ 28 . doi: 10 . 1007/978-3- 642 -81955-1_ 28 .

[15] O. Kullmann , On a generalization of extended resolution , Discret. Appl. Math. 96-97 ( 1999 ) 149 - 176 .

[16] G. Audemard , G. Katsirelos , L. Simon , A restriction of extended resolution for clause learning SAT solvers , in: AAAI, AAAI Press, 2010 , pp. 15 - 20 .

[17] M. Järvisalo , M. Heule , A. Biere , Inprocessing rules , in: B. Gramlich , D. Miller , U. Sattler (Eds.), Proc. of Automated Reasoning - 6th International Joint Conference, IJCAR 2012 , volume 7364 of LNCS , Springer, 2012 , pp. 355 - 370 . URL: https://doi.org/10.1007/978-3- 642 -31365-3_ 28 . doi: 10 . 1007/978-3- 642 -31365-3_ 28 .

[18] A. Biere , D. Kröning , Sat-based model checking , in: Handbook of Model Checking , Springer, 2018 , pp. 277 - 303 .

[19] F. Bacchus , M. Järvisalo , R. Martins , Maximum satisfiability , in: Handbook of Satisfiability , volume 336 of Frontiers in Artificial Intelligence and Applications , IOS Press, 2021 , pp. 929 - 991 .

[20] R. Nieuwenhuis , A. Oliveras , C. Tinelli , Solving SAT and SAT modulo theories: From an abstract davis-putnam-logemann-loveland procedure to dpll(T ) , J. ACM 53 ( 2006 ) 937 - 977 .

[21] C. W. Barrett , R. Sebastiani , S. A. Seshia , C. Tinelli , Satisfiability modulo theories , in: Handbook of Satisfiability , volume 336 of Frontiers in Artificial Intelligence and Applications , IOS Press, 2021 , pp. 1267 - 1329 .

[22] N. Eén , N. Sörensson , An extensible sat-solver , in: SAT , volume 2919 of Lecture Notes in Computer Science, Springer, 2003 , pp. 502 - 518 .

[23] N. Eén , N. Sörensson , Temporal induction by incremental SAT solving, in: BMC@CAV , volume 89 of Electronic Notes in Theoretical Computer Science, Elsevier, 2003 , pp. 543 - 560 .

[24] S. Kupferschmid , M. Lewis , T. Schubert , B. Becker , Incremental preprocessing methods for use in BMC, Formal Methods Syst . Des. 39 ( 2011 ) 185 - 204 .

[25] A. Nadel , V. Ryvchin , O. Strichman, Preprocessing in incremental SAT, in: A . Cimatti , R. Sebastiani (Eds.), Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012 . Proceedings, volume 7317 of Lecture Notes in Computer Science, Springer, 2012 , pp. 256 - 269 . URL: https://doi.org/10.1007/978-3- 642 -31612-8_ 20 . doi: 10 .1007/ 978-3- 642 -31612-8\_ 20 .

[26] K. Fazekas , A. Biere , C. Scholl, Incremental inprocessing in SAT solving , in: M. Janota , I. Lynce (Eds.), Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019 , Lisbon, Portugal, July 9- 12 , 2019 , Proceedings, volume 11628 of Lecture Notes in Computer Science, Springer, 2019 , pp. 136 - 154 . URL: https://doi.org/10.1007/978-3- 030 -24258- 9 _9. doi: 10 . 1007/978-3- 030 -24258-9\_9.

[27] O. Beyersdorf , M. Janota , F. Lonsing , M. Seidl , Quantified boolean formulas , in: Handbook of Satisfiability , volume 336 of Frontiers in Artificial Intelligence and Applications , IOS Press, 2021 , pp. 1177 - 1221 .

[28] K. Fazekas , M. Seidl , A. Biere , A duality-aware calculus for quantified boolean formulas , in: J. H. Davenport , V. Negru , T. Ida , T. Jebelean , D. Petcu , S. M. Watt , D. Zaharie (Eds.), 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2016 , Timisoara, Romania, September 24-27 , 2016 , IEEE, 2016 , pp. 181 - 186 . URL: https://doi.org/10.1109/SYNASC. 2016 . 038 . doi: 10 .1109/SYNASC. 2016 . 038 .

[29] D. Fried , A. Nadel , R. Sebastiani , Y. Shalmon , Entailing generalization boosts enumeration , in: SAT , volume 305 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik , 2024 , pp. 13 : 1 - 13 : 14 .

[30] S. Möhle , R. Sebastiani , A. Biere , Four flavors of entailment , in: SAT, volume 12178 of Lecture Notes in Computer Science, Springer, 2020 , pp. 62 - 71 .

[31] G. Spallitta , R. Sebastiani , A. Biere , Disjoint projected enumeration for SAT and SMT without blocking clauses , CoRR abs/2410 .18707 ( 2024 ).

[32] R. Sebastiani , Are you satisfied by this partial assignment? , CoRR abs/ 2003 .04225 ( 2020 ). URL: https://arxiv.org/abs/ 2003 .04225. arXiv: 2003 .04225.

[33] S. Möhle , R. Sebastiani , A. Biere , On enumerating short projected models, Discret . Appl. Math. 361 ( 2025 ) 412 - 439 .

[34] K. Fazekas , On SAT-based Solution Methods for Computational Problems , Ph.D. thesis, Informatik, Johannes Kepler University Linz, 2020 .

[35] M. J. H. Heule , B. Kiesl , A. Biere , Strong extension-free proof systems , J. Autom. Reason . 64 ( 2020 ) 533 - 554 .

[36] J. Berg , B. Bogaerts , J. Nordström , A. Oertel , D. Vandesande , Certified core-guided maxsat solving , in: CADE , volume 14132 of Lecture Notes in Computer Science, Springer, 2023 , pp. 1 - 22 .

[37] K. Wagner , Formalization of the Inprocessing Rules and the Reconstruction Stack in Isabelle, Master's thesis , University of Freiburg, Freiburg, Germany, 2023 .

[38] M. Järvisalo , A. Biere , Reconstructing solutions after blocked clause elimination , in: SAT , volume 6175 of LNCS , Springer, 2010 , pp. 340 - 345 .

[39] A. Biere , T. Faller , K. Fazekas , M. Fleury , N. Froleyks , F. Pollitt , Cadical 2 .0, in: A. Gurfinkel , V. Ganesh (Eds.), Computer Aided Verification - 36th International Conference, CAV 2024 , Montreal, QC, Canada, July 24-27 , 2024 , Proceedings, Part I , volume 14681 of LNCS , Springer, 2024 , pp. 133 - 152 . doi: 10 .1007/978-3- 031 -65627-9\_7.

[40] B. Kiesl , A. Rebola-Pardo , M. J. H. Heule , A. Biere , Simulating strong practical proof systems with extended resolution , J. Autom. Reason . 64 ( 2020 ) 1247 - 1267 .

[41] L. A. Barnett , A. Biere , Non-clausal redundancy properties , in: A. Platzer , G. Sutclife (Eds.), Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15 , 2021 , Proceedings, volume 12699 of Lecture Notes in Computer Science, Springer, 2021 , pp. 252 - 272 . doi: 10 .1007/978-3- 030 -79876-5_ 15 .