a Pythonic toolkit for working with Boolean expressions

[SIGKDD 2023] HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline

The first efficient procedure to test whether a sampler is uniform

Framework for studying cryptographic hash functions using SAT.

High-level interfaces over @msoos's CryptoMiniSat.

SATX es un lenguaje formal y motor de decisión para el modelado, análisis y resolución de sistemas complejos bajo restricciones, especialmente aquellos caracterizados por conflictos estructurales entre objetivos, normas y actores, conocidos como Wicked Systems.

Solving the two-dimensional strip packing problem, using several combinatorial decision making and optimization approaches: Constraint Programming, Boolean SATisfiability, Satisfiability Modulo Theory; Integer Linear Programming.

Generate and solve random instances of MAX-SAT and instances of MAX-SAT that are deterministically and pseudo-randomly generated from the solutions of previous MAX-SAT instances. This is a prototype of how a proof of work algorithm can be derived from a relevant problem.

A lightweight CNF SAT constraint encoder library

Optimization & Solving common API (SAT, MILP, etc.)

A suite for minimizing constraint systems (CNF/DNF/MILP inequalities)

A naive implementation of Algorithmic Lovász local lemma.

Artificial Intelligence Lab

Using a SAT solver to prove correctness of schedules given a list of constraints.

An implementation of the DPLL algorithm for solving SAT problems

This algorithms computes the clauses needed, to solve Minesweeper and check for satisfiability

Pygplib: Python First-Order Graph Property Library

A personal implementation of a basic SAT solver.

Automated theorem proving, Logic Programming, Optimization examples.

A simple implementation of the 3SAT problem