Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching
We present a new method to find conflicting instances of quantified formulas in the context of SMT solving. Our method splits the search for such instances in two parts. In the first part, E-matching is used to find candidate instances of the quantified formulas. In principle, any existing incremental E-matching technique can be used for this part. The incrementality avoids duplicating work for every small change of the E-graph. Together with the candidate instance, E-matching also provides an existing node in the E-graph corresponding to every term in this instance. In the second part, these nodes are used to evaluate the candidate instance, i. e., without creating new terms. The evaluation can be done in constant time per instance. Our method detects conflicting instances and unit instances (unit instances are clauses that propagate new literals). This makes our method suitable for a tight integration into the DPLL(T) framework, very much in the style of an additional theory solver.
Tue 19 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:30 - 19:30: Decision ProceduresVMCAI at VMCAI Chair(s): Alexander J. SummersUniversity of British Columbia | |||
18:30 - 18:45 Talk | Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories VMCAI Martin BrombergerMPI-INF, Alberto FioriMax Planck Institute for Informatics, Christoph WeidenbachMPI-INF Media Attached | ||
18:45 - 19:00 Talk | Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching VMCAI Media Attached | ||
19:00 - 19:15 Talk | On Pre- and Inprocessing for Weighted MaxSAT VMCAI Tobias PaxianUniversity of Freiburg, Pascal RaiolaUniversity of Freiburg, Bernd BeckerAlbert-Ludwigs-University Freiburg Media Attached | ||
19:15 - 19:30 Talk | Compositional Satisfiability Solving in Separation Logic VMCAI Quang Loc LeUniversity College London, UK Media Attached |