SAT Solving Using XOR-OR-AND Normal Forms (XNFs)

This repository contains source code for XNF-based SAT solvers as described in the PhD thesis:

J.Danner, SAT Solving Using XOR-OR-AND Normal Forms and Cryptographic Fault Attacks, Universität Passau, 2025.

Tools / Solvers

• (Q)ANFto2XNF (Algorithms 3.2 and 3.3):
  A conversion algorithm from ANF to 2-XNF, implemented in anf_to_2xnf by B. Andraschko.

• CDXCL-lite (Algorithm 4.6):
  A conflict-driven XNF SAT solver, implemented in the submodule Xorricane by J. Danner.

• Graph2XNFSAT (Algorithm 5.5):
  A graph-based DPLL-style 2-XNF SAT solver, implemented in the submodule 2-Xornado by J. Danner.

Benchmark Suites

All random and cryptogrpahic benchmark suites of Chapter 6 are available under the Releases section.

---

Setup

Run git submodule update --init --recursive to clone all submodules. Instructions to run and build the tools and solvers can be found in their respective submodules.