MaxSAT-Based Compression for Tsetlin Machines

We consider the computational problem of compacting Tsetlin Machine classifiers by reducing the number of propositional clauses while preserving predictive accuracy. TMs trained with limited clause capacity often perform poorly because stochastic optimization cannot reliably find the few precise clauses needed in a vast configuration space. High-quality compact subsets also exist in the case of larger Tsetlin Machines. The difficulty here lies in extracting them. Local pruning heuristics can fail badly on TMs because clauses interact through Boolean logic: a clause may appear unimportant in isolation yet becomes critical when others are removed. We formalize compression as the Minimum Discriminating Clause Set (MDCS) problem, which asks to find a smallest subset of clauses that preserves the trained model's discrimination of training samples. We show that MDCS is NP-hard. We solve MDCS using weighted partial Maximum Satisfiability (MaxSAT). A partition-and-merge strategy allows us to scale to 100,000 samples. Across 13 datasets, the compressed model preserves the 200-clause teacher's accuracy within a few percentage points while using a median of only 16 clauses, and outperforms a matched-capacity TM trained from scratch on every dataset where direct training has room to improve, by up to 45 percentage points.