MaxSAT-Based Compression for Tsetlin Machines

We consider the computational problem of compacting Tsetlin Machine (TM) 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 for larger TMs. The main challenge is to extract them. Heuristic pruning does not work for TMs because clauses interact through Boolean logic. A clause is unimportant in isolation, but it becomes critical when others are removed. We formalize compression as the Minimum Discriminating Clause Set (MDCS) problem: find the smallest subset of clauses that preserves the trained model's separation of training samples. We prove that MDCS is NP-hard. We solve MDCS via weighted partial Maximum Satisfiability (MaxSAT). A partition-and-merge strategy allows us to scale to 100K samples. MaxSAT compression significantly outperforms direct training on all but one of 13 datasets at matched capacity, with improvements up to 26 percentage points and a median of 6 percentage points.