Sudoku Analysis¶

Shiny, A. K., & Pujari, A. K. (1999). An Efficient Algorithm to Generate Prime Implicants. Journal of Automated Reasoning, 22(2), 149–170. https://doi.org/10.1023/A:1005940031099.

In this paper, an efficient recursive algorithm is presented to compute the set of prime implicants of a propositional formula in conjunctive normal form (CNF). The propositional formula is represented as a (0,1)-matrix, and a set of 1’s across its columns are termed as paths. The algorithm finds the prime implicants as the prime paths in the matrix using the divide-and-conquer technique. The algorithm is based on the principle that the prime implicant of a formula is the concatenation of the prime implicants of two of its subformulae. The set of prime paths containing a specific literal and devoid of a literal are characterized. Based on this characterization, the formula is recursively divided into subformulae to employ the divide-and-conquer paradigm. The prime paths of the subformulae are then concatenated to obtain the prime paths of the formula. In this process, the number of subsumption operations is reduced. It is also shown that the earlier algorithm based on prime paths has some avoidable computations that the proposed algorithm avoids. Besides being more efficient, the proposed algorithm has the additional advantage of being suitable for the incremental method, without recomputing prime paths for the updated formula. The subsumption operation is one of the crucial operations for any such algorithms, and it is shown that the number of subsumption operation is reduced in the proposed algorithm. Experimental results are presented to substantiate that the proposed algorithm is more efficient than the existing algorithms.

Cheng, CK. (2011). Lecture 15: Karnaugh Maps II. In CSE20, Discrete Mathematics. University of California, San Diego. https://cseweb.ucsd.edu/classes/sp11/cse20-a/notes/lec15.ppt.

Objective of this course is to introduce discrete mathematics for computer system designs.

Kleer, J. de. (1999). An Improved Incremental Algorithm for Generating Prime Implicates. In H. J. Levesque & F. Pirri (Eds.), Logical Foundations for Cognitive Agents: Contributions in Honor of Ray Reiter (pp. 103–112). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-60211-5_9.

In 1987 Ray Reiter and I wrote a paper entitled “Foundations of assumption-based truth maintenance systems: Preliminary report” which showed how the behavior of the Assumption-Based Truth Maintenance System can be defined using the notions of prime implicate and prime implicant. This definition of the ATMS immediately suggests generalizing the ATMS to operate on arbitrary clauses. This generalization raises two immediate computational challenges (to me, not Ray who seems immune to such challenges). First, computing prime implicates/implicants is very expensive. Second, since ATMS’s are used incrementally we need to exploit previous computation. This paper describes an improved and incremental algorithm to compute prime implicates/implicants. This algorithm allows us to experiment with the ideas Ray and I laid out in our paper. Unfortunately, the task is inherently NP-complete and all this paper can accomplish is present a more clever incremental algorithm.

del Val, A. (1994). Tractable Databases: How to Make Propositional Unit Resolution Complete through Compilation. In J. Doyle, E. Sandewall, & P. Torasso (Eds.), Principles of Knowledge Representation and Reasoning (pp. 551–561). Morgan Kaufmann. https://doi.org/10.1016/B978-1-4832-1452-8.50146-9.

We present procedures to compile any propositional clausal database σ into a logically equivalent “compiled” database σ* such that. for any clause C, σ |= C if and only if there is a unit refutation of σ* U C. It follows that once the compilation process is complete any query about the logical consequences of σ can be correctly answered in time linear in the sum of the sizes of σ* and the query. The compiled database σ* is for all but one of the procedures a subset of the set PI(σ) of prime implicates of σ, but σ* can be exponentially smaller than PI(σ). Of independent interest, we prove the equivalence of unit-refutability with two restrictions of resolution, and provide a new sufficient condition for unit refutation completeness, thus identifying a new class of tractable theories, one which is of interest to abduction problems as well. Finally, we apply the results to the design of a complete LTMS.

Echenim, M., Peltier, N., & Tourret, S. (2017). Prime Implicate Generation in Equational Logic. J. Artif. Intell. Res., 60, 827–880. https://api.semanticscholar.org/CorpusID:8314981.

We present an algorithm for the generation of prime implicates in equational logic, that is, of the most general consequences of formulæ containing equations and disequations between first-order terms. This algorithm is defined by a calculus that is proved to be correct and complete. We then focus on the case where the considered clause set is ground, i.e., contains no variables, and devise a specialized tree data structure that is designed to efficiently detect and delete redundant implicates. The corresponding algorithms are presented along with their termination and correctness proofs. Finally, an experimental evaluation of this prime implicate generation method is conducted in the ground case, including a comparison with state-of-the-art propositional and first-order prime implicate generation tools.

Kean, A., & Tsiknis, G. (1990). An incremental method for generating prime implicants/implicates. Journal of Symbolic Computation, 9(2), 185–206. https://doi.org/https://doi.org/10.1016/S0747-7171(08)80029-6.

Given the recent investigation of Clause Management Systems (CMSs) for ArtificialIntelligence applications, there is an urgent need for an efficient incremental method for generating prime implicants. Given a set of clauses F, a set of prime implicants II of F and a clause C1 the problem can be formulated as finding the set of prime implicants for II U C. Intuitively, the property of implicants, being prime implies that any effort to generate prime implicants from a set of prime implicants will not yield any new prime implicants but themselves. In this paper, we exploit the properties of prime implicants and propose an incremental method for generating prime implicants from a set of existing prime implicants plus a new clause. The correctness proof and complexity analysis of the incremental method are presented, and the intricacy of subsumptions in the incremental method is also examined. Additionally, the role of prime implicants in the CMS is also mentioned.

Mossé, M., Sha, H., & Tan, L.-Y. (2022). A Generalization of the Satisfiability Coding Lemma and Its Applications. In K. S. Meel & O. Strichman (Eds.), 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022) (Vol. 236, pp. 9:1–9:18). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.SAT.2022.9.

The seminal Satisfiability Coding Lemma of Paturi, Pudlák, and Zane is a coding scheme for satisfying assignments of k-CNF formulas. We generalize it to give a coding scheme for implicants and use this generalized scheme to establish new structural and algorithmic properties of prime implicants of k-CNF formulas. Our first application is a near-optimal bound of \(n \cdot 3^{n(1-Ω(1/k))}\) on the number of prime implicants of any n-variable k-CNF formula. This resolves an open problem from the Ph.D. thesis of Talebanfard, who proved such a bound for the special case of constant-read k-CNF formulas. Our proof is algorithmic in nature, yielding an algorithm for computing the set of all prime implicants - the Blake Canonical Form BCF - of a given k-CNF formula. The problem of computing the Blake Canonical Form BCF of a given function is a classic one, dating back to Quine, and our work gives the first non-trivial algorithm for k-CNF formulas.

Scherer, W. (2013). Partial Distributive Expansion of CNF Problems. https://sw-amt.ws/satoku/doc/doc-partial-distributive-expansion/README.html.

Partial distributive expansion of CNF formulas by expanding disjunctive CNF clauses fo full DNF clauses for propagation of required conjunctive refinements.