{"content":[{"text":"cannot be simulated by the proposed modiﬁed algorithm (Section 4) which \n is the only approach to lift the existing simulation algorithm.","bbox":{"left":0.181134,"top":0.162609,"width":0.6349349999999999,"height":0.03335000000000002}},{"text":"2.","bbox":{"left":0.181134,"top":0.220491,"width":0.017092999999999997,"height":0.015110000000000012}},{"text":"Deﬁnitions","bbox":{"left":0.209244,"top":0.220491,"width":0.103905,"height":0.015110000000000012}},{"text":"In this note we assume that QBFs are in closed prenex form i.e., we \n consider the form Q1X1...QkXk.ψ, where Xi are pairwise disjoint sets of \n variables; Qi ∈ {∃, ∀} and Qi ̸= Qi+1. The propositional part ψ of a QBF is \n called the matrix which should be in CNF (Conjunctive Normal Form) and \n the rest is the preﬁx Q. A clause is a disjunction of literals and a CNF is a \n conjunction of clauses. We denote the empty clause by ⊥. If a variable x is \n in the set Xi, we say that x is at level i and write lv(x) = i. Note that only \n variables are in preﬁx, so given a literal l if x=var(l),then quantiﬁer of l is \n same as that of x. Given a literal ℓ with quantiﬁer Qi and a literal k with \n quantiﬁer Qj, we write ℓ≤Qk if i ≤ j (we say that ℓ occurs left of k). \n Informally, a proof system is a function f which maps proofs to theorems \n (or contradictions). A proof system f simulates another proof system g (i.e., \n f ≤p g) if every g-proof of a theorem (or contradiction) can be eﬃciently \n translated into an f-proof of the same theorem. Proof systems f and g are \n said to be incomparable, if none of them can simulate the other. \n One of the main approach to QBF-solving is through expansion of quan- \n tiﬁers. Several expansion-based QBF proof systems have been developed, \n for example, ∀Exp+Res [3]. This calculus downloads the axioms by dropping \n all universal literals in a clause and annotating the existential literals by an \n assignment to all universal variables which occur to left of that variable. It \n (C1∨xτ) (C2∨xτ)) \n also allows the following resolution step: , where C1 and C2 \n (C1∨C2) \n are clauses, xτ is a literal, and (C1 ∨ C2) is the resolvent. \n The IR-calc proof system [4] has been developed as an extension of the \n ∀Exp+Res. Here, in the axiom steps, the existential variables are only anno- \n tated with ∀ variables which are on its left and belong to the same clause. The \n following instantiation step is also introduced: inst(σ, C) = {xτ[σ] | xτ ∈ C} \n where, σ is a partial assignment to the universal variables and for every \n ∀ variable ℓ to the left of x, τ[σ] returns τ(ℓ) if ℓ ∈ dom(τ) else σ(ℓ) if \n ℓ ∈ dom(σ). The resolution step remains the same. \n QRAT Proof System [5]: We need the following deﬁnitions: \n Deﬁnition 1 ([5]). Clause C is an Asymmetric Tautology (AT) w.r.t. to \n CNF ψ iﬀ ψ ⊢1 C. (Alternatively can be checked if ⊥ ∈ unit-propagation(ψ∪ \n C)). Unit propagation(⊢1) simplies a CNF by repeating the following: If","bbox":{"left":0.181134,"top":0.24881,"width":0.634968,"height":0.614481}},{"text":"2","bbox":{"left":0.493789,"top":0.875215,"width":0.00955199999999995,"height":0.015109999999999957}}],"images_bbox":[],"images_bbox_not_text_overlap":[]}