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
Journal papers

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 alogroup 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:248254, 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 preestablished patterns. The search is done by mounting the devices in readonly 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 , 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 vertices and edges. We provide improvements to the known upper bound for 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:4256, 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 onemany correspondence between simple undirected graphs G with vertex set and indeterminate strings – 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 NPhard 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 and a corresponding . We give various properties of our algorithm, including some experimental evidence that on average it requires time. We compare it with other heuristics, and state some conjectures and open problems.
Journal of Theoretical Computer Science, 710: 8896, 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 threesorted logical theory designed to capture the combinatorial reasoning about finite strings. We propose a language for expressing assertions about strings, and study in detail two sets of formulas , a set of formulas
decidable in polytime, and , a set of formulas with the property that those provable in yield polytime algorithms.
Journal of Discrete Applied Mathematics, 2018
[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 01 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): 7280, June 2017
[pdf][blog][searchdl][volume]
 Waldemar W. Koczkodaj, Dominik Strzalka, JeanPierr 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 practicedriven 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:7379, 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(34): 291307, 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(34): 223240, 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 Knowledgebased and Intelligent Engineering Systems, 19(4): 225234, 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 antiMonge condition.
Journal of Discrete Algorithms, 31:120128, March 2015.
[doi][github][blog]
 Sam Buss and Michael Soltys
Unshuffling a Square is NPHard
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 NPcomplete via a manyone reduction from 3Partition.
Journal of Computer and System Sciences, 80(4):766776, 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):535551, 2012.
[doi]
 Grzegorz Herman and Michael Soltys
Unambiguous functions in logarithmic space
Abstract: We investigate different variants of unambiguity in the context of computing multivalued functions. We propose a modification to the standard computation models of Turing machines and configuration graphs, which allows for unambiguitypreserving 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):129147, 2012.
[doi]
 Michael Soltys
Feasible proofs of Szpilrajn’s theorem: A proofcomplexity framework for concurrent automata
Abstract: The aim of this paper is to propose a proofcomplexity 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 tradeoff 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):2738, 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):680692, 2011.
[doi]
 Grzegorz Herman and Michael Soltys
On the EhrenfeuchtMycielski 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 overestimate. 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):500508, 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 non3colorable. 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 treelike. In short, we show that H^∗1_1 ≤p EF ≤p H_1.
Fundamenta Informaticae, 79(12):7183, 2007.
 Michael Soltys
The proof theoretic strength of the Steinitz Exchange Theorem
Abstract: We show that the logical theory QLA proves the CayleyHamilton 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 quantifierfree fragment, LA, translates into tautologies with TC^0Frege 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):5360, 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 CayleyHamilton The orem). Furthermore, we show that LA with quantification over permuta tions expresses NP graphtheoretic properties, and proves the soundness of the Hajós Calculus. Several open problems are stated.
Theoretical Computer Science, 348(23):321333, 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):195208, 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 CayleyHamilton 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(13):207275, December 2004.
[doi]
 Michael Soltys and Alasdair Urquhart
Matrix Identities and the Pigeonhole Principle
Abstract: We show that short boundeddepth Frege proofs of matrix identities, such as P Q = I ⊃ QP = I (over the field of two elements), imply short boundeddepth Frege proofs of the pigeonhole principle. Since the latter principle is known to require exponentialsize boundeddepth Frege proofs, it follows that the propositional version of the matrix principle also requires boundeddepth Frege proofs of exponential size.
Archive for Mathematical Logic, 43(3):351358, 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 rowechelon 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):117, 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:4254, 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):119129, 1999.
Proceedings
 Ariel Fernández, Ryszard Janicki and Michael Soltys
A permutationbased 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
Consistencydriven 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 consistencydriven knowledge acquisition, supported by a properly designed software, contributes to the improvement of quality of knowledgebased 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 squarefree 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 squarefree string, w = w1w2 . . . wn, where wi ∈ Li? In this paper we show that repetitions can be forced on squarefree strings over alphabet lists iff a suffix of the squarefree 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 threesorted 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
Nonrepetitive strings over alphabet lists
Abstract: A word is nonrepetitive 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 nonrepetitive 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 01 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 270281, February 2015.
[doi][github1][github2][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 freemarket 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 multisport 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 11381144, Pomorski Park NaukowoTechniczny (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 MinMax Theorem (KMM), a fundamental result in combinatorial matrix theory, and we show the equivalence of KMM to various MinMax 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 777788, 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 402411, 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 (TF) ∩ 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 CayleyHamilton Theorem (a central result of matrix algebra) from SET within the logical theory QLA.
10th Meeting on Computer Algebra and Applications (EACA), pages 174177, Seville, September 2006.
[slides]
 David L. Parnas and Michael Soltys
Basic Science for Software Developers
14th International Symposium on Formal Methods, pages 1520, 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 CayleyHamilton 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 493508, 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 CayleyHamilton Theorem. Furthermore, we show that LA extended with quantification over permutations expresses NP graphtheoretic 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 pequivalent 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 11761187, 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 301305, 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 141146, 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 335344, 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 preestablished patterns. The search is done by mounting the devices in readonly 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 MinMax and related theorems
Abstract: We show that the wellknown König’s MinMax 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 MinMax 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 multivalued functions. We propose a modification to the standard computation models of Turing Machines and configuration graphs, which allows for unambiguitypreserving 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 162175, 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 415424, 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 CayleyHamilton 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
 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 (CAS1110MS), 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 (CAS0812MS), 2008.
 Greg Herman and Michael Soltys
A polytime proof of correctness of the RabinMiller algorithm from Fermat’s little theorem
Abstract: Although a deterministic polytime algorithm for primality testing isnow known, the RabinMiller randomized test of primality continues being the most efficient and widely used algorithm. We prove the correctness of the RabinMiller algorithm in the theory V^1 for polynomial time reasoning, from Fermat’s little theorem. This is interesting because the RabinMiller 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 ModelTheoretic Proof of the Completeness of LK Proofs,
McMaster Computing and Software Technical Report (CAS0605MS), 1999.
(Originally posted on elogic, March 30, 1999.)
Other
 David Bremner, Antoine Deza and Michael Soltys
Foreword: selected papers from the FrancoCanadian 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.