pybipe 1.0.0

Python bindings for the bipe SAT preprocessor

pybipe

Python bindings for bipe, a state-of-the-art C++20 SAT preprocessing library. pybipe supports bipartitioning (input/output variable identification via Padoa definability), bounded variable elimination (BVE), backbone derivation, equivalence substitution, and DAC extraction, with full option configuration and DIMACS parsing. Built with nanobind and scikit-build-core.

---

🚀 Users Guide

1. Installation

Install from PyPI:

pip install pybipe

Or install from the GitLab Package Registry:

pip install pybipe --extra-index-url https://gitlab.univ-artois.fr/api/v4/projects/24773/packages/pypi/simple

---

2. Usage Examples

2.1 Basic SAT Preprocessing

You can run preprocessing on raw Python clause structures (list of lists of DIMACS 1-based literals):

from pybipe import PreprocManager, OptionPreproc, PreprocMethod, run_preproc

# Define input CNF formula
nb_vars = 3
clauses = [
    [1, 2],
    [-2, 3],
    [-1, -3]
]
projected = [1, 2, 3]  # Candidate variables for bipartitioning

# Configure options
opts = OptionPreproc()
opts.autoConfig = True  # Enable automatic density-based tuning

# Run preprocessing
mgr = PreprocManager()
out_vars, out_clauses, out_projected = mgr.run(
    nbVar=nb_vars,
    clauses=clauses,
    projected=projected,
    options=opts
)

print(f"Preprocessed: nbVar={out_vars}, {len(out_clauses)} clauses remaining.")

Or using the simplified single-function interface:

out_vars, out_clauses, out_projected = run_preproc(
    nbVar=3,
    clauses=[[1, 2], [-2, 3]],
    projected=[1, 2, 3],
    options=opts
)

---

2.2 Parsing DIMACS Files

You can parse DIMACS CNF files directly into a Python ParsedProblem object:

from pybipe import ParserDimacs

parser = ParserDimacs()
problem = parser.parse_dimacs("path/to/formula.cnf")

print(f"Variables: {problem.nbVar}, Clauses: {len(problem.clauses)}")
print("Projected variables:", problem.projected)

# Re-print as DIMACS string
print(problem.display())

---

2.3 Solver Options & Custom Configurations

pybipe exposes native C++ optree configuration groups (OptionPreproc, OptionEliminator, OptionBipartition, OptionBackbone, OptionDac, OptionReducer) with property accessors and docstrings:

from pybipe import OptionPreproc, PreprocMethod, load_options_from_dict, dump_options_to_dict

opt = OptionPreproc()

# 1. Modify top-level preprocessor options
opt.timeout = 600
opt.autoConfig = False
opt.optionPreprocMethod = PreprocMethod.SHARP_EQUIV

# 2. Modify nested eliminator options
opt.optionEliminator.growthBudget = 1.5
opt.optionEliminator.oracleVivif = True
opt.optionEliminator.bva = True

# 3. Serialize options to/from Python Dictionaries
config_dict = dump_options_to_dict(opt)
opt_restored = load_options_from_dict(config_dict)

---

🛠️ Developers Guide

1. Requirements

Before building locally, ensure the following dependencies are installed:

• C++20 compatible compiler (GCC >= 10, Clang >= 10)
• CMake (>= 3.15)
• Zlib development headers (zlib1g-dev / zlib-devel)
• Python >= 3.8

---

2. Local Build Pipeline

To compile the C++ extension module and deploy it into your Python environment:

# Clone pybipe
git clone https://gitlab.univ-artois.fr/logical/pybipe.git
cd pybipe

# Build and run tests
./build.sh --test

Alternatively, install in editable mode:

pip install -e .

---

3. Automatic Code Generation

If bipe option headers or data structures change, re-run the code generation scripts:

python3 scripts/generate_binding_hpp.py /path/to/bipe
python3 scripts/generate_bindings.py /path/to/bipe
python3 scripts/generate_runner_bindings.py /path/to/bipe

---

4. Running the Test Suite

LD_PRELOAD=$(gcc -print-file-name=libstdc++.so.6) PYTHONPATH=. python3 tests/test_options.py
LD_PRELOAD=$(gcc -print-file-name=libstdc++.so.6) PYTHONPATH=. python3 tests/test_preproc.py
LD_PRELOAD=$(gcc -print-file-name=libstdc++.so.6) PYTHONPATH=. python3 tests/test_parser.py

---

5. GitLab CI/CD Pipeline

The repository includes a multi-stage .gitlab-ci.yml pipeline:

• Build Stage: Runs cibuildwheel to build standalone Linux and Windows wheels for Python 3.8-3.13, plus an sdist package.
• Deploy Stage: Triggered on pushing Git tags, publishing wheel packages to the GitLab PyPI Package Registry or PyPI using twine.