qcdcl
Congratulations to the authors of the #IJCAI2022 distinguished papers
The IJCAI distinguished paper awards recognise some of the best papers presented at the conference each year. This year, three articles were named as distinguished papers. The winners were selected by the associate programme committee chairs, the programme and general chairs, and the president of EurAI. Abstract: The metric distortion framework posits that n voters and m candidates are jointly embedded in a metric space such that voters rank candidates that are closer to them higher. A voting rule's purpose is to pick a candidate with minimum total distance to the voters, given only the rankings, but not the actual distances.
- Personal > Honors (0.56)
- Research Report > New Finding (0.53)
Dependency Learning for QBF
Peitl, Tomáš, Slivovsky, Friedrich, Szeider, Stefan
Quantified Boolean Formulas (QBFs) can be used to succinctly encode problems from domains such as formal verification, planning, and synthesis. One of the main approaches to QBF solving is Quantified Conflict Driven Clause Learning (QCDCL). By default, QCDCL assigns variables in the order of their appearance in the quantifier prefix so as to account for dependencies among variables. Dependency schemes can be used to relax this restriction and exploit independence among variables in certain cases, but only at the cost of nontrivial interferences with the proof system underlying QCDCL. We introduce dependency learning, a new technique for exploiting variable independence within QCDCL that allows solvers to learn variable dependencies on the fly. The resulting version of QCDCL enjoys improved propagation and increased flexibility in choosing variables for branching while retaining ordinary (long-distance) Q-resolution as its underlying proof system. We show that dependency learning can achieve exponential speedups over ordinary QCDCL. Experiments on standard benchmark sets demonstrate the effectiveness of this technique.
- North America > United States > Texas > Travis County > Austin (0.14)
- Europe > Austria > Vienna (0.14)
- Europe > France > Nouvelle-Aquitaine > Gironde > Bordeaux (0.04)
- (12 more...)
- Information Technology > Artificial Intelligence > Representation & Reasoning > Logic & Formal Reasoning (0.68)
- Information Technology > Artificial Intelligence > Machine Learning > Computational Learning Theory (0.48)
- Information Technology > Artificial Intelligence > Representation & Reasoning > Constraint-Based Reasoning (0.46)