API Reference fixpoint_sat v#0.1.9

Copy Markdown

Modules

Fixpoint.SatSolver

This module solves SAT problems represented in CNF form. It's a list of lists of integers, where a positive integer i represents a boolean variable mapped to i, and a negative integer j represents negation of a boolean variable mapped to j. Examples of CNF representation

Fixpoint.SatSolver.VariableSelector.DLIS

Dynamic Largest Individual Sum.