2024/06/03 by Eugene Goldberg, Goldberg, Eugene
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Neural Networks and Applications
paper · pdf · doi:10.48550/arxiv.2406.01307
openalex publication_date 2024/06/03 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Earlier, we introduced Partial Quantifier Elimination (PQE). It is a generalization of regular quantifier elimination where one can take a part of the formula out of the scope of quantifiers. We apply PQE to CNF formulas of propositional logic with existential quantifiers. The appeal of PQE is that many problems like equivalence checking and model checking can be solved in terms of PQE and the latter can be very efficient. The main flaw of current PQE solvers is that they do not reuse learned information. The problem here is that these PQE solvers are based on the notion of clause redundancy and the latter is a structural rather than semantic property. In this paper, we provide two important theoretical results that enable reusing the information learned by a PQE solver. Such reusing can dramatically boost the efficiency of PQE like conflict clause learning boosts SAT solving.