Sat Python Packages

satcfdi

The best open-source python library to generate and process SAT's CFDI

pindakaas

A Rust library to transform integer and pseudo Boolean constraints into conjunctive normal form

ttable

a Pythonic toolkit for working with Boolean expressions

mqt-qusat

MQT QuSAT - Using Satisfiability Testing (SAT) Techniques for Encoding Quantum Computing

dratify

Check DRAT/DRUP proofs of unsatisfiability inside your Python process. Zero dependencies, optional Rust accelerator.

mcp-cfdi-mx

Model Context Protocol (MCP) server for Mexican Electronic Invoicing (CFDI 4.0, Complemento de Pagos 2.0). Provide tools to validate, generate, and explore API specifications for SAT/PAC interoperability. Vendor-neutral: seals the CFDI locally with your own CSD; any PAC receives an already-sealed document.

cdclkit

A readable, self-checking CDCL SAT solver, preprocessor and encoding library. Every answer comes with a certificate.

eqbool

Testing boolean expressions for equivalence

bauhaus

Build logical theories for SAT solvers on the fly

autoguess

An easy-to-use, general and open-source tool to solve the guess-and-determine problem

dfa-identify

Python library for identifying/learning DFAs from labeled examples by reduction to SAT.

origoid

Official OrigoID Python SDK — identity verification API for Mexico: CURP (RENAPO), INE voter list, RFC/CSF/CFDI (SAT), NSS (IMSS), OFAC/PEPs/SAT 69-B screening, face match. Zero data retention.

nonebot-plugin-cqsat

业余无线电助手，基于Nonebot2

mcp-mexico

MCP server that gives AI agents official Mexican public data: Banxico exchange and interest rates, INEGI inflation, UMA and ISR tables.

limboole

Fork of the Limboole SAT solver frontend from http://fmv.jku.at/limboole/ modified to be executable using WebAssembly on the web.

normal-form

A Python package for working with Conjunctive Normal Form (CNFs) and Boolean Satisfiability (SAT)

definition

A quick command line tool to find word meanings from 4-5 online dictionaries

sats-receiver

Satellites data receiver based on GNU Radio

npycomp

A Python library for NP-complete reductions.

satex

SAT Heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers

modenexus

Compile system models to d-DNNF circuits, then diagnose, track, and learn on one artifact: exact posteriors, ranked diagnoses, mode tracking, EM — with a PyTorch backend for GPU inference.

cfdibills

Utility to parse, validate and verify CFDI (Mexican invoice)

oraculai

An implementation of the O_SAT and O_UNSAT oracles. These oracles cannot exist. They do now.

pycscl

A lightweight CNF SAT constraint encoder library