A toy implementation of a simple SAT solver in the C#.

• Supports DPLL algorithm.
• Supports DIMACS format
• Simple Sudoku solver

Solving problem described in the DIMACS file.

 var sat = await Sat.FromFile(dimacsFilePath).ConfigureAwait(false);

var isSatisfiable = sat.Solve();
Console.WriteLine(sat.FoundModel);
Assert.IsTrue(isSatisfiable);

Hard sudoku, try it.

Encoding Sudoku rules.

    public static void RunNotFunSudoku()
    {
      var board = new SudokuBoard
      {
        [0, 1] = new CellValue(2),

        [1, 3] = new CellValue(6),
        [1, 8] = new CellValue(3),

        [2, 1] = new CellValue(7),
        [2, 2] = new CellValue(4),
        [2, 4] = new CellValue(8),

        [3, 5] = new CellValue(3),
        [3, 8] = new CellValue(2),

        [4, 1] = new CellValue(8),
        [4, 4] = new CellValue(4),
        [4, 7] = new CellValue(1),

        [5, 0] = new CellValue(6),
        [5, 3] = new CellValue(5),

        [6, 4] = new CellValue(1),
        [6, 6] = new CellValue(7),
        [6, 7] = new CellValue(8),

        [7, 0] = new CellValue(5),
        [7, 5] = new CellValue(9),

        [8, 7] = new CellValue(4),

      };

      Run(board);
   }

Solved sudoku.