# 1: Seeking Practical CDCL Insights from Theoretical SAT Benchmarks ## Authors Jan Elffers, Jesús Giráldez-Cru, Stephan Gocht, Jakob Nordström, Laurent Simon ## Abstract Over the last decades Boolean satisfiability (SAT) solvers based on conflict-driven clause learning (CDCL) have developed to the point where they can handle formulas with millions of variables. Yet a deeper understanding of how these solvers can be so successful has remained elusive. In this work we shed light on CDCL performance by using theoretical benchmarks, which have the attractive fea- tures of being a) scalable, b) extremal with respect to different proof search parameters, and c) theoretically easy in the sense of having short proofs in the resolution proof system underlying CDCL. This allows for a systematic study of solver heuristics and how efficiently they search for proofs. We report results from extensive experiments on a wide range of benchmarks. Our findings include several examples where theory predicts and explains CDCL behaviour, but also raise a number of intriguing ques- tions for further study. ## MD5: 4bd2d08e1e54a463eade5726e2f17616 ## Links * * * ## 2: An Effective Learnt Clause Minimization Approach for CDCL SAT Solvers ∗ ## Authors Mao Luo 1 , Chu-Min Li 2† , Fan Xiao 1 , Felip Manyà 3 , Zhipeng Lü 1† ## Abstract Learnt clauses in CDCL SAT solvers often contain redundant literals. This may have a negative impact on performance because redundant literals may deteriorate both the effectiveness of Boolean constraint propagation and the quality of subse- quent learnt clauses. To overcome this drawback, we define a new inprocessing SAT approach which eliminates redundant literals from learnt clauses by applying Boolean constraint propagation. Learnt clause minimization is activated before the SAT solver triggers some selected restarts, and affects only some learnt clauses during the search pro- cess. Moreover, we conducted an empirical eval- uation on instances coming from the hard combi- natorial and application categories of recent SAT competitions. The results show that a remark- able number of additional instances are solved when the approach is incorporated into five of the best performing CDCL SAT solvers (Glucose, TC Glucose, COMiniSatPS, MapleCOMSPS and MapleCOMSPS LRB). ## MD5: 074e7641e545063ce4cfdbf8f6ae3964 ## Links * * # 3: Encoding and Solving Problems in Effectively Propositional Logic ## Authors Juan Antonio Navarro-Pérez ## Abstract Solving problems by translating them to propositional satisfiability checking has been found recently as a very successful approach in many application domains. Highly optimised satisfiability solvers have been used to find solutions of difficult problems. Unfortunately, this approach does not always scale when either parameters or the size of the problem description start to grow. Translations of real-world problems tend to create large formulae, whose size is dominated by slightly different copies of subformulae which had to be replicated many times. This thesis investigates the alternative of using the language of effectively propositional logic, which is a decidable fragment of first-order logic, as a formalism to describe problems from applications in a much more succinct and natural way. At the same time, this would allow to face scalability issues by the use of reasoning techniques that work at a higher level of abstraction. After a brief overview of existing propositional and effectively propositional solving techniques, some new ideas are discussed on how the encoding of problems affects the difficulty of solving them. Then, supporting the thesis hypothesis, a pair of case studies are developed where problems from planning and model checking are encoded using effectively propositional formulae. Incidentally, the products of these case studies provide a rich and diverse set of benchmarks for implementors of reasoning tools. The thesis also explores possible approaches to efficiently solve the generated formulae, either by instantiation methods or directly by reasoning at the effectively propositional level. The work presented should be of value to communities solving problems in planning and verification, who are provided with an alternative method to apply in their domain, and to implementors of effectively propositional systems, to whom a set of relevant benchmarks is provided. The encoding techniques may also be of interest to a wider audience trying to apply automated deduction methods in other research areas. ## MD5: cf6db93d20b8a8732cdb7227c68949b4 ## Links * * # 4: Secure and Anonymous Communications Over Delay Tolerant Networks ## Authors SPIRIDON BAKIRAS, ERALD TROJA, XIAOHUA XU AND JULIANO FISCHER NAVES ## Abstract Today’s society has a fundamental need for security and anonymity. Well suited, real-life scenarios such as whistleblower reports, intelligence service operations, and the ability to communicate within oppressive governments, call for such fundamental needs. The contribution and focus of this paper is the study of anonymous communications in the context of Delay Tolerant Networks (DTNs). Current literature achieves anonymity via mechanisms that are built around the onion routing paradigm which, unfortunately, is vulnerable to malicious nodes. Instead, our work introduces a novel message forwarding algorithm that delivers messages, from source to destination, via a random walk process. As such, our protocol does not list the intermediate nodes along the route’s path and, therefore, enhances significantly the anonymity of the underlying communications. We propose two different approaches for encrypting the exchanged messages. The first one is based solely on public key cryptosystems and is, thus, suitable for short, SMS-style messaging. The second one is a hybrid solution that combines both public and symmetric key cryptography and is targeted towards large multimedia messages, such as images or video. Through extensive simulation experiments, we show that our proposed anonymous routing protocol achieves high message delivery rates, while using modest computational resources on the mobile devices. ## MD5: 7ff4ca34831b5257eba6942052974870 ## Links * * # 5: Mail reloaded: Censorship-resistant highlatency mail communication ## Authors Joakim Grebenö ## Abstract There is a theory which states that if ever anyone discovers exactly what the Universe is for and why it is here, it will instantly disappear and be replaced by something even more bizarre and inexplicable. There is another theory mentioned, which states that this has already happened. 1 ## MD5: f449e5f16e644b5e3ff4b6595a3af9d8 ## Links * * # 6: The BBP Algorithm for Pi ## Authors David H. Bailey ## Abstract The “Bailey-Borwein-Plouffe” (BBP) algorithm for π is based on the BBP formula for π, which was discovered in 1995 and published in 1996 ## MD5: 2c24c0f5b49aff6846901f14ffe6d2cf ## Links * * # 7: Efficient Conflict Driven Learning in a Boolean Satisfiability Solver ## Authors Lintao Zhang Conor F. Madigan Matthew H. Moskewicz Sharad Malik ## Abstract One of the most important features of current state-of-the-art SAT solvers is the use of conflict based backtracking and learning techniques. In this paper, we generalize various conflict driven learning strategies in terms of different partitioning schemes of the implication graph. We re-examine the learning techniques used in various SAT solvers and propose an array of new learning schemes. Extensive experiments with real world examples show that the best performing new learning scheme has at least a 2X speedup compared with learning schemes employed in state-of-the-art SAT solvers. ## MD5: e32fe553f8cbfe1728d34e18d4ab9482 ## Links * * * "http://math.ucsd.edu/~sbuss/CourseWeb/Math268_2007WS/zhang01efficient.pdf" # 8: Efficient Implementation of Property Directed Reachability ## Authors Niklas Een, Alan Mishchenko, Robert Brayton ## Abstract Last spring, in March 2010, Aaron Bradley pub- lished the first truly new bit-level symbolic model checking algorithm since Ken McMillan’s interpolation based model checking procedure introduced in 2003. Our experience with the algorithm suggests that it is stronger than interpolation on industrial problems, and that it is an important algorithm to study further. In this paper, we present a simplified and faster implementation of Bradley’s procedure, and discuss our successful and unsuccessful attempts to improve it. ## MD5: c6c96713e51f730400fdcc23b7ae4c80 ## Links * * # 9: The propositional formula chekcker HeerHugo ## Authors J.F. Groote ## Abstract ## MD5: bafea18f9461f7c1a60d05289115ced5 ## Links * * # 10: Kedjebråk och Pells ekvation ## Authors Torbjörn Tambour ## Abstract Kedjebråk är en gammal fin del av aritmetiken som numea är nästan helt bort- glömd, i alla fall har de försvunnit ur kurserna. För vårt vidkommande är de en bra repetition av bl a Euklides algoritm och lösning av diofantiska ekvationer av typen ax + by = 1. De ger också bra övning på att arbeta med kvadratrötter. ## MD5: 2e05048a4727ada8d32de2a261fb017d ## Links * * # 11: The Laplace Expansion Theorem: Computing the Determinants and Inverses of Matrices ## Authors David Eberly ## Abstract A standard method for symbolically computing the determinant of an n × n matrix involves cofactors and expanding by a row or by a column. This document describes the standard formulas for computing the determinants of 2 × 2 and 3 × 3 matrices, mentions the general form of Laplace Expansion Theorem for which the standard determinant formulas are special cases, and shows how to compute the determinant of a 4 × 4 matrix using (1) expansion by a row or column and (2) expansion by 2 × 2 submatrices. Method (2) involves fewer arithmetic operations than does method (1). ## MD5: 5d21efd52d5eb9056cfb022924070617 ## Links * * # 12: NP-complete Problems and Physical Reality ## Authors Scott Aaronson ## Abstract Can NP-complete problems be solved efficiently in the physical universe? I survey proposals including soap bubbles, protein folding, quantum computing, quantum advice, quantum adia- batic algorithms, quantum-mechanical nonlinearities, hidden variables, relativistic time dilation, analog computing, Malament-Hogarth spacetimes, quantum gravity, closed timelike curves, and “anthropic computing.” The section on soap bubbles even includes some “experimental” re- sults. While I do not believe that any of the proposals will let us solve NP-complete problems efficiently, I argue that by studying them, we can learn something not only about computation but also about physics. ## MD5: 104037ffdc06c528803ffe4785bf728d ## Links * * # 13: WHAT IS LIFE? ## Authors ERWIN SCHRODINGER ## Abstract A scientist is supposed to have a complete andthorough I of knowledge, at first hand, of somesubjects and, therefore, is usually expected not towrite on any topic of which he is not a life,master. This is regarded as a matter of noblesseoblige. For the present purpose I beg to renouncethe noblesse, if any, and to be the freed of theensuing obligation. My excuse is as follows: Wehave inherited from our forefathers the keenlonging for unified, all-embracing knowledge.The very name given to the highest institutionsof learning reminds us, that from antiquity to andthroughout many centuries the universal aspecthas been the only one to be given full credit. Butthe spread, both in and width and depth, of themultifarious branches of knowledge by duringthe last hundred odd years has confronted uswith a queer dilemma. We feel clearly that weare only now beginning to acquire reliablematerial for welding together the sum total of allthat is known into a whole; but, on the otherhand, it has become next to impossible for asingle mind fully to command more than a smallspecialized portion of it. I can see no otherescape from this dilemma (lest our true who aimbe lost for ever) than that some of us shouldventure to embark on a synthesis of facts andtheories, albeit with second-hand and incompleteknowledge of some of them -and at the risk ofmaking fools of ourselves. So much for myapology. The difficulties of language are notnegligible. One's native speech is a closely fittinggarment, and one never feels quite at ease whenit is not immediately available and has to bereplaced by another. My thanks are due to DrInkster (Trinity College, Dublin), to Dr PadraigBrowne (St Patrick's College, Maynooth) and,last but not least, to Mr S. C. Roberts. They wereput to great trouble to fit the new garment on meand to even greater trouble by my occasionalreluctance to give up some 'original' fashion ofmy own. Should some of it have survived themitigating tendency of my friends, it is to be putat my door, not at theirs. The head-lines of the ## MD5: 1c7fb6acd474a543be9b6eace278df5e ## Links * # 14: Towards a Complexity-theoretic Understanding of Restarts in SAT solvers ## Author Chunxiao Li1 , Noah Fleming2 , Marc Vinyals3 , Toniann Pitassi2 , and Vijay Ganesh1 ## Abstract Restarts are a widely-used class of techniques integral to the efficiency of Conflict-Driven Clause Learning (CDCL) Boolean SAT solvers. While the utility of such policies has been well-established empirically, a theoretical explanation of whether restarts are indeed crucial to the power of CDCL solvers is lacking. In this paper, we prove a series of theoretical results that characterize the power of restarts for various models of SAT solvers. More precisely, we make the following contributions. First, we prove an exponential separation between a drunk randomized CDCL solver model with restarts and the same model without restarts using a family of satisfiable instances. Second, we show that the configuration of CDCL solver with VSIDS branching and restarts (with activities erased after restarts) is exponentially more powerful than the same configuration without restarts for a family of unsatisfiable instances. To the best of our knowledge, these are the first separation results involving restarts in the context of SAT solvers. Third, we show that restarts do not add any proof complexitytheoretic power vis-a-vis a number of models of CDCL and DPLL solvers with non-deterministic static variable and value selection. ## MD5: 60c0235579dbd7535b8cb8b0a11945c8 ## Links * /home/tony/Documents/papers/local/download.pdf # 15: How To Prove Yourself: Practical Solutions to Identification and Signature Problems ## Author Amos Fiat and Adi Shamir Department of Applied Mathematics The Weizmann Institute of Science Rehovot 76100, Israel ## Abstract In this paper we describe simple identification and signature schemes which enable any user to prove his identity and the authenticity of his messages to any other user without shared or public keys. The schemes are provably secure against any known or chosen message attack if factoring is difficult, and typical implementations require only 1%to 4% of the number of modular multiplications required by the RSA scheme. Due to their simplicity, security and speed, these schemes are ideally suited for microprocessor-based devices such as smart cards, personal computers, and remote control systems. ## MD5: 1ed5c255525327916ef6e93774be5840 ## Links * /home/tony/Documents/papers/local/10.1007%2F3-540-47721-7_12.pdf * https://link.springer.com/content/pdf/10.1007%2F3-540-47721-7_12.pdf # 16: Gateway Forwarding Strategies in Ad hoc Networks ## Author Erik Nordström, Per Gunningberg ## Abstract The story so far. . . Ad hoc ≈ Mobile Multi-hop Wireless Networking IETF started MANET (Mobile Ad hoc NETworks) working group on ad hoc routing in 1995/96. Since then: • Four routing protocols going for RFC status (AODV, OLSR, DSR, TBRPF) • AODV implementations ≈ 10 • Zero deployment One explanation: No Internet integration• Extending the reach of wireless LANs • Disaster area rescue drones with connection to rescue central • Military units communicating with headquarters – Uppsala students are building rescue robots with ad hoc routing for participation in Robocup. ## MD5: 3aab296e21c37df09e9812e05622a5bb ## Links * /home/tony/Documents/papers/local/adhoc04-slides.pdf * http://user.it.uu.se/~erikn/papers/adhoc04-slides.pdf # 17: Minimizing Learned Clauses ## Author Niklas Sörensson1 and Armin Biere2 ## Abstract Minimizing learned clauses is an effective technique to reduce memory usage and also speed up solving time. It has been implemented in M INI S AT since 2005 and is now adopted by most modern SAT solvers in academia, even though it has not been described in the literature properly yet. With this paper we intend to close this gap and also provide a thorough experimental analysis of it’s effectiveness for the first time. ## MD5: c77e4b8aeacd6a68ccc1c75357ab2e3e ## Links * /home/tony/Documents/papers/local/SoerenssonBiere-SAT09.pdf * http://fmv.jku.at/papers/SoerenssonBiere-SAT09.pdf # 18: New Speed Records for Montgomery Modular Multiplication on 8-bit AVR Microcontrollers ## Author Zhe Liu and Johann Großschädl ## Abstract Modular multiplication of large integers is a performancecritical arithmetic operation of many public-key cryptosystems such as RSA, DSA, Diffie-Hellman (DH) and their elliptic curve-based variants ECDSA and ECDH. The computational cost of modular multiplication and related operations (e.g. exponentiation) poses a practical challenge to the widespread deployment of public-key cryptography, especially on embedded devices equipped with 8-bit processors (smart cards, wireless sensor nodes, etc.). In this paper, we describe basic software techniques to improve the performance of Montgomery modular multiplication on 8-bit AVR-based microcontrollers. First, we present a new variant of the widely-used hybrid method for multiple-precision multiplication that is 10.6% faster than the original hybrid technique of Gura et al. Then, we discuss different hybrid Montgomery multiplication algorithms, including Hybrid Finely Integrated Product Scanning (HFIPS), and introduce a novel approach for Montgomery multiplication, which we call Hybrid Separated Product Scanning (HSPS). Finally, we show how to perform the modular subtraction of Montgomery reduction in a regular fashion without execution of conditional statements so as to counteract Simple Power Analysis (SPA) attacks. Our AVR implementation of the HFIPS and HSPS method outperforms the Montgomery multiplication of the MIRACL Crypto SDK by up to 21.58% and 14.24%, respectively, and is twice as fast as the modular multiplication of the TinyECC library. ## MD5: 9030779d0c073eca3cd3e97d0d063464 ## Links * /home/tony/Documents/papers/local/882.pdf * https://eprint.iacr.org/2013/882.pdf # 19: Analyzing and Comparing Montgomery Multiplication Algorithms ## Author Cetin Kaya Koc and Tolga Acar 1 Burton S. Kaliski ## Abstract Abstract This paper discusses several Montgomery multiplication algorithms, two of which have been proposed before. We describe three additional algorithms, and analyze in detail the space and time requirements of all ve methods. These algorithms have been implemented in C and in assembler. The analyses and actual performance results indicate that the Coarsely Integrated Operand Scanning (CIOS) method, detailed in this paper, is the most ecient of all ve algorithms, at least for the general class of processor we considered. The Montgomery multiplication methods constitute the core of the modular exponentiation operation which is the most popular method used in public-key cryptography for encrypting and signing digital ## MD5: 068f77d0a3deb8012c9bf7dff6eab489 ## Links * /home/tony/Documents/papers/local/j37acmon.pdf * https://www.microsoft.com/en-us/research/wp-content/uploads/1996/01/j37acmon.pdf # 20: JID: COMCOM ARTICLE IN PRESS [m5G;November 19, 2015;17:35] ## Keywords Opportunistic networking; Delay-Tolerant networking; DTN routing; Georouting; Privacy ## Author Computer Communications 000 (2015) 118 ## Abstract ## MD5: 5dafc14ca3fd5fe8dfaffecb84a73c57 ## Links * /home/tony/Documents/papers/local/E713.pdf # 21: Two birds, one stone: using mobility behavioral profiles both as destinations and as a routing tool ## Author Adrian Sanchez-Carmonaa, Carlos Borregoa , Sergi Roblesa , Gerard Garcia-Vandellosa ## Abstract We present HabCast, a profile-cast communication paradigm that learns about the mobility habits of the locationaware nodes of the network and uses this information both to route the messages, and to deliver them only to the nodes that match the target behavioral profile. HabCast substitutes destinations identifier by a mobility profile model called habitat, meaning that allows users to send messages to any nodes who usually roams around this area instead of sending messages intended to a node. HabCast is designed to operate without network infrastructure, using Opportunistic Networking strategies and operates in three phases: approximation, floating and delivery phase. HabCast enables new services and applications on Opportunistic Networking by automatically inferring the nodes behavioral profiles and using them to define the messages destinations. The overhead introduced by HabCast is evaluated using a proof-of-concept implementation, and its performance and feasibility is studied, through simulation, under the scope of a real carsharing application. ## MD5: b6d5986299d81f6135c6c506d44d89fe ## Links * /home/tony/Documents/papers/local/joucomnet_a2017m12v99p58.pdf # 22: Checking safety properties using induction and a SAT-solver ## Author Mary Sheeran1;2 , Satnam Singh3 , and Gunnar St almarck1;2 ## Abstract We take a fresh look at the problem of how to check safety properties of nite state machines. We are particularly interested in checking safety properties with the help of a SAT-solver. We describe some novel induction-based methods, and show how they are related to more standard xpoint algorithms for invariance checking. We also present preliminary experimental results in the veri cation of FPGA cores. This demonstrates the practicality of combining a SAT-solver with induction for safety property checking of hardware in a real design ow. ## MD5: 5f7daa21107eb6d8d86f8bc48cb61410 ## Links * /home/tony/Documents/papers/local/Ind.pdf # 23: Time-Optimal Planning for Quadrotor Waypoint Flight ## Author Philipp Foehn, Angel Romero, Davide Scaramuzza ## Abstract Quadrotors are amongst the most agile flying robots. However, planning time- optimal trajectories at the actuation limit through multiple waypoints remains an open problem. This is crucial for applications such as inspection, delivery, search and rescue, and drone racing. Early works used polynomial trajec- tory formulations, which do not exploit the full actuator potential due to their inherent smoothness. Recent works resorted to numerical optimization, but require waypoints to be allocated as costs or constraints at specific discrete times. However, this time-allocation is a priori unknown and renders previ- ous works incapable of producing truly time-optimal trajectories. To generate truly time-optimal trajectories, we propose a solution to the time allocation problem while exploiting the full quadrotor’s actuator potential. We achieve this by introducing a formulation of progress along the trajectory, which en- ables the simultaneous optimization of the time-allocation and the trajectory itself. We compare our method against related approaches and validate it in real-world flights in one of the world’s largest motion-capture systems, where we outperform human expert drone pilots in a drone-racing task. ## MD5: d57f4a3cd34518a38867eac452cc5b71 ## Links * * /home/tony/Documents/papers/local/ScienceRobotics21_Foehn.pdf # 24: WORD EXTRACTION METHOD IN HUMAN SPEECH PROCESSING ## Author Piotr PORWIK, Robert PROKSA ## Abstract A major problem in isolated-word speech recognition systems is detection of the beginning and ending boundaries of the word. It is an essential of speech recognition algorithms, where signal speech segments should be reliably separated. During speech recognition background noise is also recorded, hence the word isolation is difficult. The parametric representation of the speech must provide enough information to characterize the words and to differentiate between acoustically similar words. In this paper the method of words extraction from human speech will be considered. ## MD5: d38e007808a9a07ff603a2ca73b2659f ## Links * /home/tony/Documents/papers/local/Art75R.pdf