Episciences.org
Not a member yet
6707 research outputs found
Sort by
Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
No full textQBF solvers implementing the QCDCL paradigm are powerful algorithms thatsuccessfully tackle many computationally complex applications. However, ourtheoretical understanding of the strength and limitations of these QCDCLsolvers is very limited. In this paper we suggest to formally model QCDCL solvers as proof systems. Wedefine different policies that can be used for decision heuristics and unitpropagation and give rise to a number of sound and complete QBF proof systems(and hence new QCDCL algorithms). With respect to the standard policies used inpractical QCDCL solving, we show that the corresponding QCDCL proof system isincomparable (via exponential separations) to Q-resolution, the classical QBFresolution system used in the literature. This is in stark contrast to thepropositional setting where CDCL and resolution are known to be p-equivalent. This raises the question what formulas are hard for standard QCDCL, sinceQ-resolution lower bounds do not necessarily apply to QCDCL as we show here. Inanswer to this question we prove several lower bounds for QCDCL, includingexponential lower bounds for a large class of random QBFs. We also introduce a strengthening of the decision heuristic used in classicalQCDCL, which does not necessarily decide variables in order of the prefix, butstill allows to learn asserting clauses. We show that with this decisionpolicy, QCDCL can be exponentially faster on some formulas. We further exhibit a QCDCL proof system that is p-equivalent to Q-resolution.In comparison to classical QCDCL, this new QCDCL version adapts both decisionand unit propagation policies
Group-theoretic Johnson classes and a non-hyperelliptic curve with torsion Ceresa class
No full textLet l be a prime and G a pro-l group with torsion-free abelianization. Weproduce group-theoretic analogues of the Johnson/Morita cocycle for G -- in thecase of surface groups, these cocycles appear to refine existing constructionswhen l=2. We apply this to the pro-l etale fundamental groups of smooth curvesto obtain Galois-cohomological analogues, and discuss their relationship towork of Hain and Matsumoto in the case the curve is proper. We analyze many ofthe fundamental properties of these classes and use them to give an example ofa non-hyperelliptic curve whose Ceresa class has torsion image under the l-adicAbel-Jacobi map.Comment: 18 pages, final versio
Relation between understandings of linear algebra concepts in the embodied world and in the symbolic world
No full textFor the use of embodied notions in teaching linear algebra, some studies indicate that it is helpful, whereas other studies indicate that it could be problematic or become an obstacle. Hence, additional research is needed. This study is focused on linear (in)dependence and basis, and investigates the relation between their understandings in the embodied and symbolic worlds. We also examine whether students' conceptions in the embodied world can be improved by the instruction emphasizing geometric images, as our previous studies identified some limitations of students' understanding in the embodied world. To address these issues, we designed four tasks aiming to assess students' conceptions of linear (in)dependence, basis, and dimension, and also designed linear algebra lessons emphasizing geometric images of these concepts. These tasks were conducted during the lessons and the data of 38 engineering students was collected. The analysis for the data showed that conceptions in the embodied world was positively associated with conceptions in the symbolic world; however, students' conceptions in the embodied world were not sufficiently improved by the geometric instruction implemented in this study
Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties
No full textAlgorithms for computing congruence closure of ground equations overuninterpreted symbols and interpreted symbols satisfying associativity andcommutativity (AC) properties are proposed. The algorithms are based on aframework for computing a congruence closure by abstracting nonflat terms byconstants as proposed first in Kapur's congruence closure algorithm (RTA97).The framework is general, flexible, and has been extended also to developcongruence closure algorithms for the cases when associative-commutativefunction symbols can have additional properties including idempotency,nilpotency, identities, cancellativity and group properties as well as theirvarious combinations. Algorithms are modular; their correctness and terminationproofs are simple, exploiting modularity. Unlike earlier algorithms, theproposed algorithms neither rely on complex AC compatible well-foundedorderings on nonvariable terms nor need to use the associative-commutativeunification and extension rules in completion for generating canonical rewritesystems for congruence closures. They are particularly suited for integratinginto the Satisfiability modulo Theories (SMT) solvers. A new way to viewGroebner basis algorithm for polynomial ideals with integer coefficients as acombination of the congruence closures over the AC symbol * with the identity 1and the congruence closure over an Abelian group with + is outlined
A case study on parametric verification of failure detectors
No full textPartial synchrony is a model of computation in many distributed algorithmsand modern blockchains. These algorithms are typically parameterized in thenumber of participants, and their correctness requires the existence of boundson message delays and on the relative speed of processes after reaching GlobalStabilization Time. These characteristics make partially synchronous algorithmsparameterized in the number of processes, and parametric in time bounds, whichrender automated verification of partially synchronous algorithms challenging.In this paper, we present a case study on formal verification of both safetyand liveness of the Chandra and Toueg failure detector that is based on partialsynchrony. To this end, we first introduce and formalize the class of symmetricpoint-to-point algorithms that contains the failure detector. Second, we showthat these symmetric point-to-point algorithms have a cutoff, and the cutoffresults hold in three models of computation: synchrony, asynchrony, and partialsynchrony. As a result, one can verify them by model checking small instances,but the verification problem stays parametric in time. Next, we specify thefailure detector and the partial synchrony assumptions in three frameworks:TLA+, IVy, and counter automata. Importantly, we tune our modeling to use thestrength of each method: (1) We are using counters to encode message bufferswith counter automata, (2) we are using first-order relations to encode messagebuffers in IVy, and (3) we are using both approaches in TLA+. By running thetools for TLA+ and counter automata, we demonstrate safety for fixed timebounds. By running IVy, we prove safety for arbitrary time bounds. Moreover, weshow how to verify liveness of the failure detector by reducing theverification problem to safety verification. Thus, both properties are verifiedby developing inductive invariants with IVy
Bidirectional Runtime Enforcement of First-Order Branching-Time Properties
No full textRuntime enforcement is a dynamic analysis technique that instruments amonitor with a system in order to ensure its correctness as specified by someproperty. This paper explores bidirectional enforcement strategies forproperties describing the input and output behaviour of a system. We develop anoperational framework for bidirectional enforcement and use it to study theenforceability of the safety fragment of Hennessy-Milner logic with recursion(sHML). We provide an automated synthesis function that generates correctmonitors from sHML formulas, and show that this logic is enforceable via aspecific type of bidirectional enforcement monitors called action disablingmonitors
Families of stable 3-folds in positive characteristic
No full textWe show that flat families of stable 3-folds do not lead to proper modulispaces in any characteristic . As a byproduct, we obtain log canonical4-fold pairs, whose log canonical centers are not weakly normal
Smoothability of relative stable maps to stacky curves
No full textUsing log geometry, we study smoothability of genus zero twisted stable mapsto stacky curves relative to a collection of marked points. One application isto smoothing semi-log canonical fibered surfaces with marked singular fibers.Comment: 22 pages, final versio
Review of Ralf Lüfter, The Ethics of Economic Responsibility
No full textRalf Lüfter, The Ethics of Economic Responsibility, Routledge, 202
Are Cultural Insights Worthy in Political Economy?: Review of Cultural Values in Political Economy, edited by J.P. Singh
No full textCultural Values in Political Economy, edited by J.P. Singh, Stanford, California: Stanford University Press, 2020, 248 p., e-boo