Preprocessing (and Inprocessing)
Matti Järvisalo · 2014
Inprocessing Characterize inprocessing deduction as transition systems State φ [ ρ ]σ ◮ φ: current “irredundant” clauses ◮ ρ: current “redundant” clauses ⋆ φ and φ ∧ ρ satisfiability-equivalent ⋆ Need not be φ |= ρ ◮ σ : sequence of literal-clause pairs l :C (for solution reconstruction) M. Jarvisalo (HIIT & UH) Preprocessing Jan 20, 2014 38 / 46 Abstract Inprocessing Characterize inprocessing deduction as transition systems State φ [ ρ ]σ ◮ φ: current “irredundant” clauses ◮ ρ: current “redundant” clauses ⋆ φ and φ ∧ ρ satisfiability-equivalent ⋆ Need not be φ |= ρ ◮ σ : sequence of literal-clause pairs l :C (for solution reconstruction)Inprocessing Characterize inprocessing deduction as transition systems State φ [ ρ ]σ ◮ φ: current “irredundant” clauses ◮ ρ: current “redundant” clauses ⋆ φ and φ ∧ ρ satisfiability-equivalent ⋆ Need not be φ |= ρ ◮ σ : sequence of literal-clause pairs l :C (for solution reconstruction) M. Jarvisalo (HIIT & UH) Preprocessing Jan 20, 2014 38 / 46