Books
Michael Soltys.
An introduction to the analysis of algorithms
Published by World Scientific
3rd edition
328 pages, 2018
Michael Soltys.
An introduction to computational complexity
Published by the Jagiellonian University Press.
143 pages, 2009
[PDF]
Journal papers
Hung Dang, Ginger Reyes, Katharine Soltys, and Michael Soltys
Enrollment predictions with machine learning.
Abstract: A Machine Learning framework for predicting enrollment is proposed. The framework consists of Amazon Web Services SageMaker together with standard Python tools for Data Analytics, including Pandas, NumPy, MatPlotLib and Scikit-Learn. The tools are deployed with Jupyter
Notebooks running on AWS SageMaker. Based on three years of enrollment
history, a model is built to compute – individually or in batch mode – probabilities of enrollments for given applicants. These probabilities can then be used during the admission period to target undecided students. The audience for this paper is both SEM practitioners and technical practitioners in the area of data analytics. Through reading this paper, enrollment management professionals will be able to understand what goes into the preparation of Machine Learning model to help with predicting admission rates. Technical experts, on the other hand, will gain a blue-print for what is required from them.
Strategic Enrollment Management Quarterly, volume 9, issue 2, July 2021
[link]Konrad Kułakowski, Jiří Mazurek, Jaroslav Ramík and Michael Soltys
When is the condition of order preservation met?
Abstract: This article explores a relationship between inconsistency in the pairwise comparisons method and conditions of order preservation. A pairwise comparisons matrix with elements from an alo-group is investigated. This approach allows for a generalization of previous results. Sufficient conditions for order preservation based on the properties of elements of pairwise comparisons matrix are derived. A numerical example is presented.
European Journal of Operational Research, 277(1):248-254, August 2019
[doi]- Eric Gentry, Frank Lyu, Ryan McIntyre and Michael Soltys
SEAKER: A tool for fast digital forensic triage
Abstract: Faced with a preponderance of high capacity digital media devices, forensic investigators must be able to review them quickly, and establish which devices merit further attention. This early stage of an investigation is called triage and it is a chief part of evidence assessment. In this paper we present a digital forensic device, which we named SEAKER (Storage Evaluator and Knowledge Extraction Reader), which enables forensic investigators to perform triage on many digital devices very quickly. Instead of imaging the drives, which takes hours, SEAKER does a search for files with names that conform to pre-established patterns. The search is done by mounting the devices in read-only mode (to preserve evidence) and listing the contents of the device. Unlike imaging, this approach takes minutes rather than hours. Also, SEAKER’s hardware consists principally of a Raspberry Pi (RP) and so it is very inexpensive —this is crucial in this era of budgetary constraints. Once SEAKER has identified media devices of interest, those can be confiscated for further investigation in a lab. But devices that do not have hits can be left at the scene. This has two principal benefits: forensic examiners can concentrate on those devices that are promising in terms of evidence for the given investigation, and devices without hits are not confiscated from legitimate users.
Advances in Information and Communication, Springer 2019
[doi] - Ryan McIntyre and Michael Soltys
An improved upper bound and algorithm for clique covers
Abstract: Indeterminate strings have received considerable attention in the recent past; see for example [Christodoulakis et al., Indeterminate strings, prefix arrays and undirected graphs, TCS 600 4 (2015)] and [Helling et al., Constructing an Indeterminate String from its Associated Graph, TCS 710 (2018)]. This attention is due to their applicability in bioinformatics, and to the natural correspondence with undirected graphs. One aspect of this correspondence is the fact that the minimal alphabet size of indeterminates representing any given undirected graph corresponds to the size of the minimal clique cover of this graph. This paper first considers a related problem proposed in the Helling 2018 paper mentioned above: characterize $latex \Theta_n(m)$, which is the size of the largest possible minimal clique cover (i.e., an exact upper bound), and hence alphabet size of the corresponding indeterminate, of any graph on $latex n$ vertices and $latex m$ edges. We provide improvements to the known upper bound for $latex \Theta_n(m)$ in section 3.3. Helling et al. 2018 also presents an algorithm which finds clique covers in polynomial time. We build on this result with an original heuristic for vertex sorting which significantly improves their algorithm’s results, particularly in dense graphs.
Journal of Discrete Algorithms, 48:42-56, 2018.
[doi][pdf][blog] - Joel Helling, P.J. Ryan, W.F. Smyth, Michael Soltys
Constructing an Indeterminate String from its Associated Graph
Abstract: As discussed at length in [Christodoulakis et al., Indeterminate strings, prefix arrays and undirected graphs, Theoret. Comput. Sci. 600 4 (2015)], there is a natural one-many correspondence between simple undirected graphs G with vertex set $latex V=\{1,2,\ldots,n\}$ and indeterminate strings $latex x=x[1..n]$ – that is, sequences of subsets of some alphabet Sigma. In this paper, given G, we consider the “reverse engineering” problem of computing a corresponding x on an alphabet Sigma_min of minimum cardinality. This turns out to be equivalent to the NP-hard problem of computing the intersection number of G, thus in turn equivalent to the clique cover problem. We describe a heuristic algorithm that computes an approximation to $latex \Sigma_\text{min}$ and a corresponding $latex x$. We give various properties of our algorithm, including some experimental evidence that on average it requires $latex O(n^2\log n)$ time. We compare it with other heuristics, and state some conjectures and open problems.
Journal of Theoretical Computer Science, 710: 88-96, 2018.
Also presented at LSD&LAW 2017.
[doi][github][blog] - Michael Soltys and Neerja Mhaskar
A formal framework for stringology
Abstract: A new formal framework for Stringology is proposed, which consists of a three-sorted logical theory $latex \mathscr{S}$ designed to capture the combinatorial reasoning about finite strings. We propose a language $latex \mathcal{L}_\mathscr{S}$ for expressing assertions about strings, and study in detail two sets of formulas $latex \Sigma_0^B$, a set of formulas
decidable in polytime, and $latex \Sigma_1^B$, a set of formulas with the property that those provable in $latex \mathscr{S}$ yield polytime algorithms.
Journal of Discrete Applied Mathematics, Volume 274, 15 March 2020, Pages 141-151
[doi][pdf] - Ariel Fernández, Ryszard Janicki, Michael Soltys
Computing covers from matchings with permutations
Abstract: We present a matrix permutation algorithm for computing a minimal vertex cover from a maximal matching in a bipartite graph. Our algorithm is linear time and linear space, and provides an interesting perspective on a well known problem. Unlike most algorithms, it does not use the concept of alternating paths, and it is formulated entirely in terms of combinatorial operations on a binary matrix. The algorithm relies on permutations of rows and columns of a 0-1 matrix which encodes a bipartite graph together with its maximal matching. This problem has many important applications such as network switches which essentially compute maximal matchings between their incoming and outgoing ports.
The International Journal of Computer Applications, 24(2): 72-80, June 2017
[pdf][blog][searchdl][volume] - Waldemar W. Koczkodaj, Dominik Strzalka, Jean-Pierr Magnot, Jiri Mazurek, James Peters, Michael Soltys, Jacek Szybowski, Arturo Tozzi, Hojjat Rakhshani
On normalization of inconsistency indicators in pairwise comparisons
Abstract: In this study, we provide mathematical and practice-driven justification for using [0, 1] normalization of inconsistency indicators in pairwise comparisons. The need for normalization, as well as problems with the lack of normalization, are presented. A new type of paradox of infinity is described.
International Journal of Approximate Reasoning, 86:73-79, July 2017.
[doi][blog][arXiv] - Waldemar W. Koczkodaj, Ludmil Mikhailov, Grzegorz Redlarski, Jacek Szybowski, Gaik Tamazian, Michael Soltys, Elisa Wajch and Kevin Kam Fung Yuen
Important Facts and Observations about Pairwise Comparisons
Abstract: This study has been inspired by numerous requests from researchers who often confuse Saaty’s AHP with the Pairwise Comparisons (PC) method, taking AHP as the only representation of PC. Most formal results of this survey article are based on a recently published work by Koczkodaj and Szwarc. This article should be regarded as an interpretation and clarification of future theoretical investigations of PC. In addition, this article is a reflection on general PC research at a higher level of abstraction: the philosophy of science. It delves into the foundations and implications of pairwise comparisons. Finally, open problems have also been reported for future research.
Special Issue on Pairwise Comparisons in Fundamenta Informaticae, 144(3-4): 291-307, 2016
[doi] - Barbara Sandrasagra and Michael Soltys
Complex Ranking Procedures
Abstract: We propose a research program for developing a formal framework for ranking procedures based on the Pairwise Comparisons method. We are interested in the case where relatively few items are to be ranked with a complex procedure and according to a large number of criteria. A typical example of this scenario is a competition where several companies bid for a contract, and where the selection of the winner is done with multiple criteria according to an intricate selection procedure. Several other applications are suggested.
Special Issue on Pairwise Comparisons in Fundamenta Informaticae, 144(3-4): 223-240, 2016
[doi][blog] - Michael Soltys
A Formal Approach to Ranking Procedures
Abstract: A formal framework for ranking procedures is proposed. The case of interest is where relatively few items are to be ranked with a complex procedure and according to a large number of criteria. A typical example of this scenario is a competition where several companies bid for a contract, and where the selection of the winner is done with multiple criteria according to an intricate selection procedure. A case study of a bidding procedure is presented, and a logical theory for matrix algebra is proposed as the formal framework for working with Pairwise Comparisons.
International Journal of Knowledge-based and Intelligent Engineering Systems, 19(4): 225-234, 2015
[doi] - Neerja Mhaskar and Michael Soltys
String Shuffle: Circuits and Graphs
Abstract: We show that shuffle, the problem of determining whether a string w can be composed from an order preserving shuffle of strings x and y, is not in AC^0, but it is in AC^1. The fact that shuffle is not in AC0 is shown by a reduction of parity to shuffle and invoking the seminal result of Furst et al., while the fact that it is in AC1 is implicit in the results of Mansfield. Together, the two results provide a lower and upper bound on the complexity of this combinatorial problem. We also explore an interesting relationship between graphs and the shuffle problem, namely what types of graphs can be represented with strings exhibiting the anti-Monge condition.
Journal of Discrete Algorithms, 31:120-128, March 2015.
[doi][github][blog] - Sam Buss and Michael Soltys
Unshuffling a Square is NP-Hard
Abstract: A shuffle of two strings is formed by interleaving the characters into a new string, keeping the characters of each string in order. A string is a square if it is a shuffle of two identical strings. There is a known polynomial time dynamic programming algorithm to determine if a given string z is the shuffle of two given strings x,y; however, it has been an open question whether there is a polynomial time algorithm to determine if a given string z is a square. We resolve this by proving that this problem is NP-complete via a many-one reduction from 3-Partition.
Journal of Computer and System Sciences, 80(4):766-776, 2013.
[doi][arXiv][slides][github 1][github 2] - Michael Soltys
Proving properties of matrices over Z2
Abstract: We prove assorted properties of matrices over Z_2, and outline the complexity of the concepts required to prove these properties. The goal of this line of research is to establish the proof complexity of matrix algebra. It also presents a different approach to linear algebra: one that is formal, consisting in algebraic manipulations according to the axioms of a ring, rather than the traditional semantic approach via linear transformations. Archive for Mathematical Logic, 51(5):535-551, 2012.
[doi] - Grzegorz Herman and Michael Soltys
Unambiguous functions in logarithmic space
Abstract: We investigate different variants of unambiguity in the context of computing multi-valued functions. We propose a modification to the standard computation models of Turing machines and configuration graphs, which allows for unambiguity-preserving composition. We define a notion of reductions (based on function composition), which allows nondeterminism but controls its level of ambiguity. In light of this framework we establish reductions between different variants of path counting problems. We obtain improvements of results related to inductive counting. Fundamenta Informaticae, 114(2):129-147, 2012.
[doi] - Michael Soltys
Feasible proofs of Szpilrajn’s theorem: A proof-complexity framework for concurrent automata
Abstract: The aim of this paper is to propose a proof-complexity framework for concurrent automata. Since the behavior of concurrent processes can be described with partial orders, we start by formalizing proofs of Szpilrajn’s theorem. This theorem says that any partial order may be extended to a total order. We give two feasible proofs of the finite case of Szpilrajn’s theorem. The first proof is formalized in the logical theory LA extended to ordered rings; this yields a TC^0 Frege derivation. The second proof is formalized in the logical theory ∃LA and yields a P/poly Frege derivation. Although TC^0 is a much smaller complexity class than P/poly, the trade-off is that the P/poly proof is algebraically simpler—it requires the algebraic theory LA over the simplest of rings: Z_2.
Journal of Automata, Languages and Combinatorics, 16(1):27-38, 2011. - Michael Soltys and Craig Wilson
On the complexity of computing winning strategies for finite poset games
Abstract: This paper is concerned with the complexity of computing winning strategies for poset games. While it is reasonably clear that such strategies can be computed in PSPACE, we give a simple proof of this fact by a reduction to the game of geography. We also show how to formalize the reasoning about poset games in Skelley’s theory WW_1^1 for PSPACE reasoning. We conclude that W_1^1 can use the “strategy stealing argument” to prove that in poset games with a supremum the first player always has a winning strategy.
Theory of Computing Systems, 48(3):680-692, 2011.
[doi] - Grzegorz Herman and Michael Soltys
On the Ehrenfeucht-Mycielski sequence
Abstract: We introduce the inverted prefix tries (a variation of suffix tries) as a convenient formalism for stating and proving properties of the Ehrenfeucht- Mycielski sequence. We also prove an upper bound on the position in the sequence by which all strings of a given length will have appeared; our bound is given by the Ackermann function, which, in light of experi- mental data, may be a gross over-estimate. Still, it is the best explicitly known upper bound at the moment. Finally, we show how to compute the next bit in the sequence in a constant number of operations.
Journal of Discrete Algorithms, 7(4):500-508, 2009.
[doi][github]
(In 2008, we used generate.c available on GitHub, in order to obtain the first 30 million bits of the EM sequence in just under two minutes with 2Gb of RAM). - Grzegorz Herman, Tim Paterson and Michael Soltys
A propositional proof system with quantification over permutations of variables,
Abstract: We introduce a new propositional proof system, which we call H, that allows quantifi- cation over permutations. In H we may write (∃ab)α and (∀ab)α, which is semantically equivalent to α(a, b) ∨ α(b, a) and α(a, b) ∧ α(b, a), respectively. We show that H with cuts restricted to Σ_1 formulas (we denote this system H_1) simulates efficiently the Hajós calculus (HC) for constructing graphs which are non-3-colorable. This shows that short proofs over formulas that assert the exis- tence of permutations can capture polynomial time reasoning (as by [9], HC is equivalent in strength to EF, which in turn captures polytime reasoning). We also show that EF simulates efficiently H^*_1, which is H_1 with proofs restricted to being tree-like. In short, we show that H^∗1_1 ≤p EF ≤p H_1.
Fundamenta Informaticae, 79(1-2):71-83, 2007. - Michael Soltys
The proof theoretic strength of the Steinitz Exchange Theorem
Abstract: We show that the logical theory QLA proves the Cayley-Hamilton theorem from the Steinitz Exchange theorem together with a strength- ening of the linear independence principle. Since QLA is a fairly weak theory (in the sense that its quantifier-free fragment, LA, translates into tautologies with TC^0-Frege proofs—when restricted to the field Q of the rationals), it follows that the proof complexity of matrix algebra can be distilled to the Steinitz Exchange theorem.
Discrete Applied Mathematics, 155(1):53-60, 2007.
[doi] - Michael Soltys
LA, Permutations, and the Hajos Calculus
Abstract: LA is a simple and natural logical system for reasoning about matrices. We show that LA, over finite fields, proves a host of matrix identities (so called “hard matrix identities”) from the matrix form of the pigeon- hole principle. LAP is LA with matrix powering; we show that LAP extended with quantification over permutations is strong enough to prove fundamental theorems of linear algebra (such as the Cayley-Hamilton The- orem). Furthermore, we show that LA with quantification over permuta- tions expresses NP graph-theoretic properties, and proves the soundness of the Hajós Calculus. Several open problems are stated.
Theoretical Computer Science, 348(2-3):321-333, December 2005.
[doi] - Neil Thapen and Michael Soltys
Weak Theories of Linear Algebra
Abstract: We investigate the theories LA,LAP,∀LAP of linear algebra, which were originally defined to study the question of whether com- mutativity of matrix inverses has polysize Frege proofs. We give sen- tences separating quantified versions of these theories, and define a fragment ∃LA of ∀LAP in which we can interpret a weak theory V_1 of bounded arithmetic and carry out polynomial time reasoning about matrices – for example, we can formalize the Gaussian elimination algorithm. We show that, even if we restrict our language, ∃LA proves the commutativity of inverses.
Archive for Mathematical Logic, 44(2):195-208, 2005.
[doi] - Michael Soltys and Stephen Cook
The Proof Complexity of Linear Algebra
Abstract: We introduce three formal theories of increasing strength for lin- ear algebra in order to study the complexity of the concepts needed to prove the basic theorems of the subject. We give what is apparently the first feasible proofs of the Cayley-Hamilton theorem and other properties of the determinant, and study the propositional proof complexity of matrix identities such as AB = I → BA = I.
Annals of Pure and Applied Logic, 130(1-3):207-275, December 2004.
[doi] - Michael Soltys and Alasdair Urquhart
Matrix Identities and the Pigeonhole Principle
Abstract: We show that short bounded-depth Frege proofs of matrix identities, such as P Q = I ⊃ QP = I (over the field of two elements), imply short bounded-depth Frege proofs of the pigeonhole principle. Since the latter principle is known to require exponential-size bounded-depth Frege proofs, it follows that the propositional version of the matrix principle also requires bounded-depth Frege proofs of exponential size.
Archive for Mathematical Logic, 43(3):351-358, April 2004.
[doi] - Michael Soltys
Extended Frege and Gaussian Elimination
Abstract: We show that the Gaussian Elimination algorithm can be proven cor- rect with uniform Extended Frege proofs of polynomial size, and hence feasibly. More precisely, we give short uniform Extended Frege proofs of the tautologies that express the following: given a matrix A, the Gaussian Elimination algorithm reduces A to row-echelon form. We also show that the consequence of this is that a large class of matrix identities can be proven with short uniform Extended Frege proofs, and hence feasibly.
Bulletin of the Section of Logic, 31(4):1-17, 2002. - Michael Soltys
Berkowitz’s Algorithm and Clow Sequences,
Abstract: A combinatorial interpretation of Berkowitz’s algorithm is presented. Berkowitz’s algorithm is the fastest known parallel algorithm for computing the characteristic polynomial of a matrix. The combinatorial interpretation is based on “loop covers” introduced by Valiant, and “clow sequences”, defined by Mahajan and Vinay. Clow sequences turn out to capture very succinctly the computations performed by Berkowitz’s algorithm, which otherwise are quite difficult to analyze. The main contribution of this paper is a proof of correctness of Berkowitz’s algorithm in terms of clow sequences.
Electronic Journal of Linear Algebra, 9:42-54, 2002.
[ELA repository] - Stephen Cook and Michael Soltys
Boolean Programs and Quantified Propositional Proof Systems
Abstract: We introduce the notion of Boolean programs, which provide more concise descriptions of Boolean functions than Boolean circuits. We characterize nonuniform PSPACE in terms of polynomial size families of Boolean programs. We then show how to use Boolean programs to witness quantifiers in the subsystems G1 and G∗1 of the proof system G for the quantified propositional calculus.
Bulletin of the Section of Logic, 28(3):119-129, 1999.
Proceedings
- Michael Soltys
Cloudifying the Curriculum with AWS
Abstract: This is an Innovate Practice Full Paper. The Cloud has become a principal paradigm of computing in the last ten years, and Computer Science curricula must be updated to reflect that reality. This paper examines simple ways to accomplish curriculum cloudification using Amazon Web Services (AWS), for Computer Science and other disciplines such as Business, Communication and Mathematics.
Frontiers in Engineering (FiE) 2021, October 2021
[doi][post] - Samuel Decanio, Michael Soltys, Kimo Hildreth
Voyager: Tracking with a click
Abstract: Attribution, the ability to match events on the Internet to actors who caused them, is a difficult problem in Cybersecurity and Digital Forensics. The Internet was not designed to track behavior of users; instead, it is a common open platform that is propitious to anonymity. Different actors take advantage of this anonymity, and if they break the law, it is up to law enforcement to track them, i.e., to attribute actions to actors in way that would stand up in court. In this paper we present a tool, called Voyager, based on the idea of a tracking pixel, which can help investigators with attribution.
Accepted for KES2020 publication, September 2020
[doi][presentation][post] - Zane Gittins and Michael Soltys
Malware Persistence Mechanisms
Abstract: In the public imagination Cybersecurity is very much about malware, even though malware constitutes only part of all the threats faced by Cybersecurity experts. However, malware is still one of the best methods to gain persistent access and control of a target system. Malware is often combined with a well socially-engineered phishing attack that deceives a user to gain a foothold on a system. Once the attacker gains a beachhead in the victim’s network, it may be used to download additional payloads and exploit vulnerabilities, to gain more control and access within a network. Using malware as their foothold, attackers are able to to conduct reconnaissance, gather intelligence (e.g., exfiltration of intellectual property) or simply inflict damage or extortion (e.g., ransomware). All of this has to be done in a way that allows an attacker to retain access for as long as possible; the ability to do so is called persistence, and this paper examines the different techniques used by malware to accomplish persistence in an ever evolving landscape.
Accepted for KES2020 publication, September 2020
[doi][presentation][post] - Eric Gentry and Michael Soltys
SEAKER: A mobile digital forensics triage device
Abstract: As our world of digital devices continues to expand, the amount of digital evidence encountered by law enforcement during case investigation is ever increasing. Faced with a preponderance of high capacity digital media devices, forensic investigators must be able to review them quickly, and establish which devices merit further attention. Utilizing a small single-board computer called Raspberry Pi, this mobile digital forensics triage device provides fast, targeted feedback for immediate evidence assessment.
In this paper we present a digital forensic device, named SEAKER (Storage Evaluator and Knowledge Extraction Reader), which enables forensic investigators to perform triage on many digital devices very quickly. Developed for on-scene, time-sensitive investigations, its utility extends to preventing over-collection and large backlogs at digital forensics labs worldwide.
Procedia Computer Science, Knowledge-Based and Intelligent Information & Engineering Systems: Proceedings of the 23rd International Conference KES2019, Volume 159, 2019, Pages 1652-1661.
Presented Invited Session IS13: Cybercrime Investigation and Digital Forensics, Budapest, Hungary, September 2019.
[doi] - Christopher Kuske, Konrad Kułakowski and Michael Soltys
Approximating consistency in pairwise comparisons
Abstract: We propose parametrized families of algorithms for approximating inconsistent matrices with consistent ones. We present experimental results, and optimize distance versus performance.
Procedia Computer Science, Knowledge-Based and Intelligent Information & Engineering Systems: Proceedings of the 23rd International Conference KES2019, Volume 159, 2019, Pages 814-823.
Presented at Invited Session IS18: Decision modeling with and without pairwise comparisons, Budapest, Hungary, September 2019.
[doi] - Noelle Abe and Michael Soltys
Deploying Health Campaign Strategies to Defend Against Social Engineering Threats
Abstract: The threat of social engineering is one that affects not only the financial and reputational wellbeing of corporate entities but also the basic rights of individuals to privacy. Methods common to health campaigns used to disseminate information warning against social engineering have the potential for success. By providing potential scenarios and exact descriptions of threats, the recipients of the messages might become more aware of the dangers posed through the Internet. Case studies of effective health campaigns will be examined, as well as specific threats that could be avoided by more awareness on the part of the individual. Psychological effects of different techniques and the way that general knowledge can help to prevent social engineering attacks will also be examined.
Procedia Computer Science, Knowledge-Based and Intelligent Information & Engineering Systems: Proceedings of the 23rd International Conference KES2019, Volume 159, 2019, Pages 824-831.
Presented at Invited Sessions IS24: Knowledge-based Learning and Education Support System: Design and Function, Budapest, Hungary, September 2019.
[doi] - Ariel Fernández, Ryszard Janicki and Michael Soltys
A permutation-based algorithm for computing covers from matchings
Abstract: We present a matrix permutation algorithm for computing a minimal vertex cover from a maximal matching in a bipartite graph. Our algorithm is linear time and linear space, and provides an interesting perspective on a well known problem. Unlike most algorithms, it does not use the concept of alternating paths, and it is formulated entirely in terms of combinatorial operations on a binary matrix.
To appear at the 32nd International Conference on Computers and Their Applications (CATA2017), March 2017. - Waldemar Koczkodaj and Michael Soltys
Consistency-driven Pairwise Comparisons Approach to Abandoned Mines Hazard Rating
Abstract: The pairwise comparisons method, together with inconsistency analysis, are used to assess the hazard level for abandoned mines. Weights, reflecting the relative importance of the objectives concerned are one of the most commonly used solutions for this type of data. Subjective assessments involve inaccuracy (which is difficult to manage) and inconsistency in assessments (which can be measured and may influence the accuracy). The pairwise comparisons method allows us to define a consistency measure and use it as a validation technique. A consistency-driven knowledge acquisition, supported by a properly designed software, contributes to the improvement of quality of knowledge-based systems.
The 7th International Conference on Computational Methods (ICCM2016), August 2016. - Neerja Mhaskar and Michael Soltys
Forced repetitions over alphabet lists
Abstract. Thue [Thu06] showed that there exist arbitrarily long square-free strings over an alphabet of three symbols (not true for two symbols). An open problem was posed in [GKM10], which is a generalization of Thue’s original result: given an alphabet list L = L1, . . . , Ln, where |Li| = 3, is it always possible to find a square-free string, w = w1w2 . . . wn, where wi ∈ Li? In this paper we show that repetitions can be forced on square-free strings over alphabet lists iff a suffix of the square-free string conforms to a pattern which we term as an offending suffix. We also prove properties of offending suffixes. However, the problem remains tantalizingly open.
To appear in 21st Prague Stringology Conference (PSC), August 2016.
[slides] - Neerja Mhaskar and Michael Soltys
A formal framework for Stringology
Abstract: A new formal framework for Stringology is proposed, which consists of a three-sorted logical theory S designed to capture the combinatorial reasoning about finite words. A witnessing theorem is proven which demonstrates how to extract algo- rithms for constructing strings from their proofs of existence. Various other applications of the theory are shown. The long term goal of this line of research is to introduce the tools of Proof Complexity to the analysis of strings.
20th Prague Stringology Conference (PSC), to appear in Lecture Notes in Computer Science, 2015.
[slides] - Neerja Mhaskar and Michael Soltys
Non-repetitive strings over alphabet lists
Abstract: A word is non-repetitive if it does not contain a subword of the form vv. Given a list of alphabets L=L_1,L_2,…,L_n, we investigate the question of generating non-repetitive words w=w_1w_2 … w_n, such that the symbol w_i is a letter in the alphabet L_i. This problem has been studied by several authors (e.g., Grytczuk, Shallit, and it is a natural extension of the original problem posed and solved by A. Thue. While we do not solve the problem in its full generality, we show that such strings exist over many classes of lists. We also suggest techniques for tackling the problem, ranging from online algorithms, to combinatorics over 0-1 matrices, and to proof complexity. Finally, we show some properties of the extension of the problem to abelian squares.
WALCOM: Algorithms and Computation, volume 8973 of Lecture Notes in Computer Science, pages 270-281, February 2015.
[doi][github-1][github-2][blog] - Michael Soltys
Fair ranking in competitive bidding procurement: A case analysis
Best Paper Award.
Abstract: Fair and transparent procurement procedures are a cornerstone of a well functioning free-market economy. In particular, bidding is a mechanism whereby companies compete for contracts; when functioning well, the process rewards both the quality of the proposal, and the “reasonableness” of the quote. This way, both the company and the public win. The bidding process requires a fair and transparent ranking procedure. Once the parameters of the competition are established, the company issuing the bid is required by law to abide by those parameters. Not surprisingly, opposing interests may try to “game the system.” The more complex the service, the harder it is to rank competing bids. Complex services require complex ranking, which in turn makes undue influence more difficult to uncover. In this paper we analyze the case of two companies, Reilly Security and Contemporary Security, bidding for the contract of providing security during the Pan American games in Toronto 2015: The Pan Am Games are the world’s third largest international multi-sport Games; they are only surpassed in size and scope by the Olympic Summer Games and the Asian Games. We argue that the ranking procedures did not reflect the quality of the bids, resulting in one of the companies submitting a substantially more expensive bid, and still winning the competition. The reader may gain information on this contentious matter by reading a number of newspaper articles. The author consulted for Executek International on this matter.
18th International Conference in Knowledge Based and Intelligent Information and Engineering Systems (KES), volume 35, Procedia Computer Science, pages 1138-1144, Pomorski Park Naukowo-Techniczny (PPNT), Gdynia, September 2014.
[doi][slides][blog] - Ariel Fernández and Michael Soltys
Feasible combinatorial matrix theory
Abstract: We give the first, as far as we know, feasible proof of König’s Min-Max Theorem (KMM), a fundamental result in combinatorial matrix theory, and we show the equivalence of KMM to various Min-Max principles, with proofs of low complexity.
38th International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 8087 of Lecture Notes in Computer Science, pages 777-788, IST, Klosterneuburg, Austria, August 2013.
Click here for an expanded proof of Claim 8 in the paper.
[doi][slides] - Michael Soltys
Circuit complexity of shuffle
Abstract: We show that sh(x,y,w), the problem of determining whether a string w can be composed from an order preserving shuffle of strings x and y, is not in AC^0, but it is in AC^1. The fact that shuffle is not in AC^0 is shown by a reduction of parity to shuffle and invoking the seminal result from 1984 regrind parity not in AC^0, while the fact that it is in AC^1 is implicit in the 1982 results of Mansfield. Together, the two results provide a strong complexity bound for this combinatorial problem.
International Workshop on Combinatorial Algorithms (IWOCA), volume 8288 of the Lecture Notes in Computer Science, pages 402-411, Rouen, France, July 2013.
[doi][slides] - Katharine Blanchard and Michael Soltys
Perceptions of foundational knowledge by computer science students
Abstract: In this paper we are concerned with computer science students’
perceptions of foundational knowledge, understood as the mathematical
underpinnings of the field. We review recent literature on the
subject, propose an approach for teaching foundational knowledge, and
finally present a case study where we analyze the merits of our
approach. We make our observations based on experience and on a
student survey.
17th Western Canadian Conference on Computing Education (WCCCE), University of British Columbia, Vancouver, May 2012.
[doi][slides] - Michael Soltys
The proof theoretic strength of the Steinitz exchange theorem
Abstract: We show that the proof complexity of matrix algebra can be distilled to the Steinitz Exchange Theorem (SET): given a total set of vectors T, and a linearly independent set E, we can compute a set F such that |E|=|F| and (T-F) ∩ E is also total. We observe that the set F can be computed with NC^2 algorithms (polynomial size, depth O(log^2n) circuits), and outline a proof of the Cayley-Hamilton Theorem (a central result of matrix algebra) from SET within the logical theory QLA.
10th Meeting on Computer Algebra and Applications (EACA), pages 174-177, Seville, September 2006.
[slides] - David L. Parnas and Michael Soltys
Basic Science for Software Developers
14th International Symposium on Formal Methods, pages 15-20, Canada, August 2006. - Michael Soltys
Feasible Proofs of Matrix Properties with Csanky’s Algorithm
Abstract: We show that Csanky’s fast parallel algorithm for computing the characteristic polynomial of a matrix can be formalized in the logical theory LAP, and can be proved correct in LAP from the principle of linear independence. LAP is a natural theory for reasoning about linear algebra introduced in Soltys & Cook. Further, we show that several principles of matrix algebra, such as linear independence or the Cayley-Hamilton Theorem, can be shown equivalent in the logical theory QLA. Applying the separation between complexity classes AC\subsetneq DET, we show that these principles are in fact not provable in QLA. In a nutshell, we show that linear independence is “all there is” to elementary linear algebra (from a proof complexity point of view), and furthermore, linear independence cannot be proved trivially (again, from a proof complexity point of view).
19th International Workshop Computer Science Logic (CSL), volume 3634 of Lecture Notes in Computer Science, pages 493-508, Oxford, August 2005.
[doi][slides][arXiv] - Michael Soltys
LA, Permutations, and the Hajos Calculus
Abstract: LA is a simple and natural field independent system for reasoning about matrices. We show that LA extended to contain a matrix form of the pigeonhole principle is strong enough to prove a host of matrix identities (so called “hard matrix identities” which are candidates for separating Frege and extended Frege). LAP is LA with matrix powering; we show that LAP extended with quantification over permutations is strong enough to prove theorems such as the Cayley-Hamilton Theorem. Furthermore, we show that LA extended with quantification over permutations expresses NP graph-theoretic properties, and proves the soundness of the Hajós calculus. A corollary is that a fragment of Quantified Permutation Frege (a novel propositional proof system that we introduce in this paper) is p-equivalent of extended Frege. Several open problems are stated.
31st International Colloquium on Automata, Languages and Programming (ICALP), volume 3142 of Lecture Notes in Computer Science, pages 1176-1187, Turku, July 2004.
[doi][slides] - Michael Soltys
Matrix algebra with quantification over permutations
Abstract: We introduce a logical system (called ∃PLAP) for reasoning about matrix algebra. ∃PLAP formalizes existential quantification over permutations, and it is strong enough to derive important results of matrix algebra such as the Cayley Hamilton Theorem. On the other hand, ∃PLAP is feasible, in the sense that it falls within polynomial time reasoning. This result elucidates further the proof complexity of linear algebra based on Berkowitz’s fast parallel algorithm for computing the characteristic polynomial.
9th Meeting on Computer Algebra and Applications (EACA), pages 301-305, Santander, July 2004. - Michael Soltys
Finite Fields and Propositional Proof Systems
Abstract: Propositional proof complexity is a well established area of theoretical computer science; it is an area of research intimately connected with complexity theory and automated reasoning. In this paper we introduce a proof system, which we call A (a fragment of the theory LA), for formalizing algebraic proofs over arbitrary fields, and we show how to translate formulas and proofs over A into propositional proofs, and conclude that we can formalize properties of finite fields (where the depth is small) with short Frege proofs.
The 7th World Multiconference on Systemics, Cybernetics and Informatics, pages 141-146, Orlando, Florida, July 2003. - Michael Soltys and Stephen Cook
The Proof Complexity of Linear Algebra,
Abstract: We introduce three formal theories of increasing strength for linear algebra in order to study the complexity of the concepts needed to prove the basic theorems of the subject. We give what is apparently the first feasible proofs of the Cayley Hamilton theorem and other properties of the determinant, and study the propositional proof complexity of matrix identities.
17th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 335-344, Copenhagen, July 2002.
[slides]
Presentations
- Eric Gentry, Frank Lyu, Ryan McIntyre and Michael Soltys
SEAKER: A tool for fast digital forensic triage
Abstract: Faced with a preponderance of high capacity digital media devices, forensic investigators must be able to review them quickly, and establish which devices merit further attention. This early stage of an investigation is called triage and it is a chief part of evidence assessment. In this paper we present a digital forensic device, which we named SEAKER (Storage Evaluator and Knowledge Extraction Reader), which enables forensic investigators to perform triage on many digital devices very quickly. Instead of imaging the drives, which takes hours, SEAKER does a search for files with names that conform to pre-established patterns. The search is done by mounting the devices in read-only mode (to preserve evidence) and listing the contents of the device. Unlike imaging, this approach takes minutes rather than hours. Also, SEAKER’s hardware consists principally of a Raspberry Pi (RP) and so it is very inexpensive — this is crucial in this era of budgetary constraints. Once SEAKER has identified media devices of interest, those can be confiscated for further investigation in a lab. But devices that do not have hits can be left at the scene. This has two principal benefits: forensic examiners can concentrate on those devices that are promising in terms of evidence for the given investigation, and devices without hits are not confiscated from legitimate users.
Future of Information and Communications Conference (FICC), 2019, San Francisco
[pdf][post] - Carlos Adrián Gomez, Michael Soltys and Adam Sędziwy
iSprinkle: when education, innovation and application meet
Abstract: This paper presents a senior undergraduate project which consists in the implementation of a Raspberry Pi based sprinkler system. The outcome is ingenious and innovative for several reasons: it is a low cost product, but of high quality and versatility (arguably better and cheaper than most household products on the market); it is well suited for usage in draught stricken regions (such as Southern California); it interfaces automatically with weather stations on the Internet, and adapts its sprinkling according to forecasts. For the student this was an opportunity to apply a wide range of technologies, APIs, and to work with watering regulations. The project was both pedagogically rich and intellectually challenging.
5th International Conference on Educational Innovation in Technical Careers, INDOTEC 2017, Granada, Spain
[pdf][poster] - Ariel Fernández and Michael Soltys
Feasible combinatorial matrix theory: polytime proofs for König’s Min-Max and related theorems
Abstract: We show that the well-known König’s Min-Max Theorem (KMM), a fundamental result in combinatorial matrix theory, can be proven in the first order theory LA with induction restricted to ∑_1^B formulas. This is an improvement over the standard textbook proof of KMM which requires ∏_2^B induction, and hence does not yield feasible proofs – while our new approach does. LA is a weak theory that essentially captures the ring properties of matrices; however, equipped with ∑_1^B$ induction LA is capable of proving KMM, and a host of other combinatorial properties such as Menger’s, Hall’s and Dilworth’s Theorems. Therefore, our result formalizes Min-Max type of reasoning within a feasible frame work.
Short presentation at LICS 2013, Tulane University, New Orleans.
[slides][full version] - Michael Soltys and Greg Herman
Unambiguous functions in logarithmic space
Abstract: We investigate different variants of unambiguity in the context of computing multi-valued functions. We propose a modification to the standard computation models of Turing Machines and configuration graphs, which allows for unambiguity-preserving composition. We define a notion of reductions (based on function composition), which allows nondeterminism but controls its level of ambiguity. In light of this framework we establish reductions between different variants of path counting problems. We obtain improvements of results related to inductive counting.
5th Conference on Computability in Europe (CiE), pages 162-175, Heidelberg, August 2009.
[slides] - Michael Soltys and Craig Wilson
On the complexity of computing winning strategies for finite poset games
Abstract: This paper is concerned with the complexity of computing winning strategies for poset games. While it is reasonably clear that such strategies can be computed in PSPACE, we give a simple proof of this fact by a reduction to the game of geography. We also show how to formalize the reasoning about poset games in Skelley’s theory W_1^1 for PSPACE reasoning. We conclude that W_1^1 can use the “strategy stealing argument” to prove that in poset games with a supremum the first player always has a winning strategy.
4th Conference on Computability in Europe (CiE), pages 415-424, Athens, June 2008.
[slides] - Michael Soltys
Feasible proofs of matrix identities with Csanky’s algorithm
Abstract: We show that Csanky’s fast parallel algorithm for computing the characteristic polynomial of a matrix can be formalized in the logical theory LAP, and can be proved correct in LAP from the principle of linear independence. LAP is a natural theory for reasoning about linear algebra introduced in Soltys & Cook. Further, we show that several principles of matrix algebra, such as linear independence or the Cayley-Hamilton Theorem, can be shown equivalent in the logical theory QLA. Applying the separation between complexity classes AC\subsetneq DET, we show that these principles are in fact not provable in QLA. In a nutshell, we show that linear independence is “all there is” to elementary linear algebra (from a proof complexity point of view), and furthermore, linear independence cannot be proved trivially (again, from a proof complexity point of view).
The 7th International Workshop on Logic and Computational Complexity, LCC, affiliated with the 20th Annual IEEE Symposium on Logic in Computer Science (LICS), Chicago, June 2005.
[slides]
Technical reports
- YuLin Bingle, Vance Brahosky, Amanda Carpenter, Mariana Holliday, Alan Jaeger, Michael Soltys
Workforce Development in IT
Abstract: This paper examines the landscape of workforce development in the IT industry, from the perspective of academia, government, cloud companies and small-medium size businesses.
September 2023
http://hdl.handle.net/20.500.12680/ff365c670 - Tyler King and Michael Soltys
Minimum Path Star Topology Algorithms for Weighted Regions and Obstacles
Abstract: Shortest path algorithms have played a key role in the past century, paving the way for modern day GPS systems to find optimal routes along static systems in fractions of a second. One application of these algorithms includes optimizing the total distance of power lines (specifically in star topological configurations). Due to the relevancy of discovering well-connected electrical systems in certain areas, finding a minimum path that is able to account for geological features would have far-reaching consequences in lowering the cost of electric power transmission. We initialize our research by proving the convex hull as an effective bounding mechanism for star topological minimum path algorithms. Building off this bounding, we propose novel algorithms to manage certain cases that lack existing methods (weighted regions and obstacles) by discretizing Euclidean space into squares and combining pre-existing algorithms that calculate local minimums that we believe have a possibility of being the absolute minimum. We further designate ways to evaluate iterations necessary to reach some level of accuracy. Both of these novel algorithms fulfill certain niches that past literature does not cover.
https://arxiv.org/abs/2109.06944 - Socrates Frangis, Jorge Lacoste, and Michael Soltys
Cybersecurity: a Navy and CSUCI collaboration.
Abstract: This whitepaper is a result of active collaboration between the Naval Surface Warfare Center, Port Hueneme Division and Dr. Michael Soltys from the California State University Channel Islands. This paper was developed in part during the Office of Naval Research, Summer Faculty Research Program while Professor Soltys was engaged with Cyber Security Leadership at the Command. This paper summarizes the need for cyber security professionals in the Navy workforce and provides potential methods in which the California State University Channel Islands and the Naval Surface Warfare Center Port Hueneme Division can leverage the existing Education Partnership Agreement as well as potential other contract mechanisms to further the mutual goals of the organizations. Additionally recomendations are provided to create opportunities of scholarship and employment for graduating students.
Navy technical report [https://apps.dtic.mil/sti/pdfs/AD1124375.pdf], January 2021. - Michael Soltys
Proving correctness of Machine Learning procedures.
Abstract: This paper explores approaches to proving the correctness of Machine Learning procedures, starting from a background of algorithm and
circuit correctness.
Navy technical report, December 2020. - Michael Soltys
WordPress on AWS: a Communication Framework
Abstract: This paper re-examines the content of a standard advanced course in Cybersecurity from the perspective of Cloud Computing. More precisely, we review the core concepts of Cybersecurity, as presented in a senior undergraduate or graduate class, in light of the Amazon Web Services (AWS) cloud.
https://arxiv.org/abs/2007.01823 - Michael Soltys
Cybersecurity in the AWS Cloud
Abstract: This paper re-examines the content of a standard advanced course in Cybersecurity from the perspective of Cloud Computing. More precisely, we review the core concepts of Cybersecurity, as presented in a senior undergraduate or graduate class, in light of the Amazon Web Services (AWS) cloud.
https://arxiv.org/abs/2003.12905 - Michael Soltys
Cloudifying the curriculum with AWS
Abstract: The Cloud has become a principal paradigm of computing in the last ten years, and Computer Science curricula must be updated to reflect that reality. This paper examines simple ways to accomplish curriculum cloudification using Amazon Web Services (AWS), for Computer Science and other disciplines such as Business, Communication and Mathematics.
https://arxiv.org/abs/2002.04020 - Michael Soltys
Gaussian lattice reduction algorithm terminates in polynomial time
Abstract: In this short note we show that the classical Gaussian reduction algorithm for finding the shortest vector in an R^2 lattice works in polynomial time. In other words, we show that the SVP (shortest vector problem) has a polytime solution in the case of two dimensions. This has always been known, but the author could not find an explicit proof.
McMaster Computing and Software Technical Report (CAS-11-10-MS), 2011. - Michael Soltys
A note on finding a rational symmetric matrix for a given separable polynomial
Abstract: Given a separable polynomial p(x)∈Q[x], which splits in R[x], is it possible to find a symmetric matrix over Q whose eigenvalues are precisely the roots of p(x)? This note investigates this questions, and provides a condition on p(x) under which it is always possible to find such a matrix—the question whether such a matrix can be found unconditionally is left open. The condition we give is that the Vandermonde matrix of the roots of p(x) be (quasi) orthogonal.
McMaster Computing and Software Technical Report (CAS-08-12-MS), 2008. - Greg Herman and Michael Soltys
A polytime proof of correctness of the Rabin-Miller algorithm from Fermat’s little theorem
Abstract: Although a deterministic polytime algorithm for primality testing isnow known, the Rabin-Miller randomized test of primality continues being the most efficient and widely used algorithm. We prove the correctness of the Rabin-Miller algorithm in the theory V^1 for polynomial time reasoning, from Fermat’s little theorem. This is interesting because the Rabin-Miller algorithm is a polytime randomized algorithm, which runs in the class RP (i.e., the class of polytime Monte Carlo algorithms), with a sampling space exponential in the length of the binary encoding of the input number. (The class RP contains polytime P.) However, we show how to express the correctness in the language of $\V$, and we also show that we can prove the formula expressing correctness with polytime reasoning from Fermat’s Little theorem, which is generally expected to be independent of V^1. Our proof is also conceptually very basic in the sense that we use the extended Euclid’s algorithm, for computing greatest common divisors, as the main workhorse of the proof. For example, we make do without proving the Chinese Reminder theorem, which is used in the standard proofs.
arXiv:0811.3959, 2008.
[arXiv] - David L. Parnas and Michael Soltys
Basic Science for Software Developers
McMaster SQRL Technical Report (7), 2002. - Michael Soltys
A Model-Theoretic Proof of the Completeness of LK Proofs,
McMaster Computing and Software Technical Report (CAS-06-05-MS), 1999.
(Originally posted on elogic, March 30, 1999.)
Other
- Joshua C. Nwokeji, Myra Roldan, Michael Soltys and Terry Holmes
A Hands-on Approach to Cloudifying Curriculum in Computing and Engineering Education
Panel, Frontiers in Engineering (FiE) 2021, Lincoln Nebraska, October 13, 2021.
[post] - David Bremner, Antoine Deza and Michael Soltys
Foreword: selected papers from the Franco-Canadian workshop on combinatorial algorithms
Journal of Combinatorial Optimization, 16(4):323, 2008.
[doi] - Más que difícil, complejo
Interviewed by Bruno Massare for Information Technology (Argentina), May 2008. - Michael Soltys
The complexity of derivations of matrix identities.
PhD thesis, University of Toronto, 2001.