Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Formal Methods in System Design
Published in: Formal Methods in System Design 2/2014

01-10-2014

Quantifier elimination by dependency sequents

Authors: Eugene Goldberg, Panagiotis Manolios

Published in: Formal Methods in System Design | Issue 2/2014

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We consider the problem of existential quantifier elimination for Boolean CNF formulas. We present a new method for solving this problem called derivation of dependency-sequents (DDS). A dependency-sequent (D-sequent) is used to record that a set of variables is redundant under a partial assignment. We introduce the join operation that produces new D-sequents from existing ones. We show that DDS is compositional, i.e., if our input formula is a conjunction of independent formulas, DDS automatically recognizes and exploits this information. We introduce an algorithm based on DDS and present experimental results demonstrating its potential.
next article Scalable reachability analysis via automated dynamic netlist-based hint generation

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Appendix
Available only for authorised users
Footnotes
1
In this paper, we consider D-sequents presented at FMCAD-12 [17] that state redundancy of quantified variables. At FMCAD-13 [19], we introduced D-sequents stating the redundancy of clauses containing quantified variables. Formally, D-sequents based on variable redundancy are just a special case of those based on clause redundancy. However, there is an important difference that justifies a special attention to D-sequents based on variable redundancy. The set \(X\) of quantified variables in formula \(\exists {X} [F]\) remains the same while the set of clauses containing variables of \(X\) may grow exponentially in \(|X|\). If a QE-algorithm using D-sequents based on clause redundancy “gets lost”, it may generate a large number of irrelevant clauses whose redundancy it will have to prove. QE-algorithms based on variable redundancy do not have this problem.
 
2
In [17], we used the notion of virtual redundancy to address the following problem. The fact that \(\exists {X} [F_{\varvec{s}}] \equiv \exists {X} [F_{\varvec{s}} \setminus (F_{\varvec{s}})^Z]\) does not imply that \(\exists {X} [F_{\varvec{q}}] \equiv \exists {X} [F_{\varvec{q}} \setminus (F_{\varvec{q}})^Z]\) where \(\varvec{s} \subset \varvec{q}\). That is redundancy of variables \(Z\) in subspace \(\varvec{s}\) specified by Definition 6 does not imply such redundancy in subspace \(\varvec{q}\) contained in subspace \(\varvec{s}\). The notion of virtual redundancy solves this paradox by weakening Definition 6. Namely, variables of \(Z\) are redundant in \(\varvec{q}\) even if \(\exists {X} [F_{\varvec{q}}] \not \equiv \exists {X} [F_{\varvec{q}} \setminus (F_{\varvec{q}})^Z]\) but \(\exists {X} [F_{\varvec{s}}] \equiv \exists {X} [F_{\varvec{s}} \setminus (F_{\varvec{s}})^Z]\) for some \(\varvec{s}\) such that \(\varvec{s} \subset \varvec{q}\). In this paper, we solve the problem above by using scoped redundancy i.e. by strengthening Definition 6. The trick is that we forbid to assign variables of scope \(W\). Then (see Lemma 2 of the appendix), redundancy of \(Z\) with scope \(W\) in subspace \(\varvec{q}\) where \(W \cap Vars (\varvec{s})=\emptyset \) implies redundancy of \(Z\) in any subspace \(\varvec{q}\) where \(\varvec{s} \subset \varvec{q}\) if \(W \cap Vars (\varvec{q}) = \emptyset \).
 
3
The description of this case given in [17] says that if \(S_1\) is symmetric in \(v\) it remains in \(\varOmega \) untouched. It is an error because, as we mentioned above, the set of D-sequent produced for subspace \(\varvec{q}\) may turn out to be uncomposable.
 
Literature
1.
Abdulla P, Bjesse P, Eén N (2000) symbolic reachability analysis based on sAT-solvers. In: Proceedings of the 6th international conference on tools and algorithms for construction and analysis of systems, TACAs’00, pp 411–425
2.
Ayari A, Basin D (2002) Qubos: deciding quantified boolean logic using propositional satisfiability solvers. In: Proceedings of 4th international conference on formal methods in computer-aided design, vol 2517 of LNCS, FMCAD’02, pp 187–201
3.
Biere A (2004) Resolve and expand. In: Procedings of the seventh international conference on theory and applications of satisfiability testing, SAT’04, pp 59–70
4.
Biere A (2008) Picosat essentials. J Satisf Boolean Model Comput 4(2–4):75–97MATH
5.
Bradley AR (2011) Sat-based model checking without unrolling. In: Proceedings of the 12th international conference on verification, model checking, and abstract interpretation, VMCAI’11, pp 70–87
6.
Brauer J, King A, Kriener J (2011) Existential quantification as incremental sat. In: Proceedings of the 23rd international conference on computer aided verification, CAV’11, Springer-Verlag, pp 191–207
7.
Bryant R (1986) Graph-based algorithms for Boolean function manipulation. IEEE Trans Comput C–35(8):677–691CrossRef
8.
Chauhan P, Clarke E, Jha S, Kukula J, Veith H, Wang D (2001) Using combinatorial optimization methods for quantification scheduling. In: Proceedings of the 11th IFIP WG 10.5 advanced research working conference on correct hardware design and verification methods, CHARME ’01, pp 293–309
9.
Clarke E, Emerson A (1982) Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Proceedings of logic of programs, Workshop, pp 52–71
10.
Clarke E, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge
11.
12.
13.
14.
Ganai M, Gupta A, Ashar P (2004) Efficient sat-based unbounded symbolic model checking using circuit cofactoring. In: Proceedings of the 2004 IEEE/ACM international conference on computer-aided design, ICCAD’04, pp 510–517
15.
Goldberg E (2009) Boundary points and resolution. In: Proceedings of theory and applications of satisfiability testing, 12th international conference, SAT’09, pp 147–160
16.
Goldberg E, Manolios P (2011) Sat-solving based on boundary point elimination. In: Proceedings of 6th international Haifa Verification Conference, pp 93–111
17.
Goldberg E, Manolios P (2012) Quantifier elimination by dependency sequents. In: Proceedings of formal methods in computer-aided design, FMCAD’12, pp 34–44
18.
Goldberg E, Manolios P (2012) Removal of quantifiers by elimination of boundary points. Technical Report. arXiv:​1204.​1746v2 [cs.LO], Northeastern University
19.
Goldberg E, Manolios P (2013) Quantifier elimination via clause redudnancy. In: Proceedings of formal methods in computer-aided design, FMCAD’13, pp 85–92
20.
Jiang R (2009) Quantifier elimination via functional composition. In: Proceedings of the 21st international conference on computer aided verification, CAV’09, pp 383–397
21.
Jin H, Somenzi F (2005) Prime clauses for fast enumeration of satisfying assignments to boolean circuits. In: Proceedings of the 42nd annual design automation conference, DAC’05, pp 750–753
22.
23.
Marques-Silva J, Sakallah K (1996) Grasp: a new search algorithm for satisfiability. In: Proceedings of the 1996 IEEE/ACM international conference on computer-aided design, ICCAD’96, pp 220–227
24.
25.
McMillan K (2002) Applying sat methods in unbounded symbolic model checking. In: Proceedings of the 14th international conference on computer aided verification, CAV’02, pp 250–264
26.
McMillan K (2003) Interpolation and sat-based model checking. In: Proceedings of computer aided verification, 15th international conference, CAV’03, Springer, pp 1–13
27.
Moskewicz M, Madigan C, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient sat solver. In: Proceedings of the 38th annual design automation conference, DAC’01, pp 530–535
28.
29.
Williams P, Biere A, Clarke E, Gupta A (2000) Combining decision diagrams and sat procedures for efficient symbolic model checking. In: Proceedings of the 12th international conference on computer aided verification, CAV’00, pp 124–138
30.
31.
32.
Metadata
Title
Quantifier elimination by dependency sequents
Authors
Eugene Goldberg
Panagiotis Manolios
Publication date
01-10-2014
Publisher
Springer US
Published in
Formal Methods in System Design / Issue 2/2014
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-014-0214-z

Other articles of this Issue 2/2014

Formal Methods in System Design 2/2014 Go to the issue

OriginalPaper

Deciding floating-point logic with abstract conflict driven clause learning

OriginalPaper

Verification of Galois field based circuits by formal reasoning based on computational algebraic geometry

OriginalPaper

Quantifier-free encoding of invariants for hybrid systems

OriginalPaper

Scalable reachability analysis via automated dynamic netlist-based hint generation

OriginalPaper

Verifying global start-up for a Möbius ring-oscillator

OriginalPaper

Budget-bounded model-checking pushdown systems

Premium Partner

    Image Credits