tiny.smt.dimacs

1//! Reads and writes Boolean formulas in conjunctive normal form as plain text. The format is DIMACS2//! CNF: a `p cnf V C` header gives the variable and clause counts, `c` lines are comments, and each3//! clause lists its literals as signed variable numbers, 1-based, ending with 0.4//!5//! Other SAT tools and benchmark collections exchange formulas as text, so a caller needs to load6//! such a file into a solver and to print a solver's clauses for another tool. A text written7//! elsewhere may be malformed, or may disagree with its own header about how many clauses it holds.8//!9//! Variable 1 of the text is the solver's variable 0, and a negative number is the negated literal.10//! The reader treats the header's clause count as a check and its variable count as a floor: a11//! clause may name a variable past the count, and the solver grows to hold it. The writer prints12//! every clause the solver holds, learned clauses the solver kept included, so a text written after13//! a solve can hold more clauses than were added.14const std = @import("std");15const sat = @import("sat/root.zig");1617/// The errors `parse` returns for a malformed text, besides the allocator's and the solver's, so18/// code that reports why a DIMACS text was refused can switch on them. A header count that fails to19/// parse as a number returns the error of `std.fmt.parseInt`, which this set leaves out. `parse`20/// returns an inferred error set.21pub const ParseError = error{22    /// A `p` line whose kind differs from `cnf` or that lacks a count.23    InvalidHeader,24    /// A clause token other than a 32-bit signed integer, or a last clause missing a closing 0.25    InvalidLiteral,26    /// The number of clauses differs from the header's count.27    ClauseCountMismatch,28};2930/// Returns a new solver that allocates with `allocator` and holds the variables and clauses of the31/// DIMACS text `source`, so code can load a formula written by another tool, then solve the32/// returned solver. The caller owns the solver and frees it with `deinit`. Lines are trimmed of33/// spaces, tabs and carriage returns, and blank lines and lines starting with `c` are skipped. A34/// `p cnf V C` line adds V variables and sets C as the expected clause count. The parser accepts a35/// text without a header, and a second header adds its variables and replaces the expected count. A36/// clause may span lines, and one line may hold more than one clause: each 0 ends one. A lone 0 is37/// the empty clause. The call returns `InvalidHeader`, `InvalidLiteral` and `ClauseCountMismatch`38/// as their tags describe, and the errors of `std.fmt.parseInt` for a header count that fails to39/// parse as a number. The literal -2147483648 makes the call panic.40pub fn parse(allocator: std.mem.Allocator, source: []const u8) !sat.Solver {41    var solver = sat.Solver.init(allocator);42    errdefer solver.deinit();43    var expected_clauses: ?usize = null;44    var clauses_seen: usize = 0;45    var clause: std.ArrayList(sat.Literal) = .empty;46    defer clause.deinit(allocator);47    var lines = std.mem.splitScalar(u8, source, '\n');48    while (lines.next()) |raw_line| {49        const line = std.mem.trim(u8, raw_line, " \t\r");50        if (line.len == 0 or line[0] == 'c') continue;51        var tokens = std.mem.tokenizeAny(u8, line, " \t\r");52        const first = tokens.next() orelse continue;53        if (std.mem.eql(u8, first, "p")) {54            const kind = tokens.next() orelse return ParseError.InvalidHeader;55            if (!std.mem.eql(u8, kind, "cnf")) return ParseError.InvalidHeader;56            const variable_count = try std.fmt.parseInt(usize, tokens.next() orelse return ParseError.InvalidHeader, 10);57            expected_clauses = try std.fmt.parseInt(usize, tokens.next() orelse return ParseError.InvalidHeader, 10);58            var index: usize = 0;59            while (index < variable_count) : (index += 1) _ = try solver.addVariable();60            continue;61        }62        var current: ?[]const u8 = first;63        while (current) |token| {64            const value = std.fmt.parseInt(i32, token, 10) catch return ParseError.InvalidLiteral;65            if (value == 0) {66                try solver.addClause(clause.items);67                clause.clearRetainingCapacity();68                clauses_seen += 1;69            } else {70                try clause.append(allocator, try sat.Literal.fromDimacs(value));71            }72            current = tokens.next();73        }74    }75    if (clause.items.len > 0) return ParseError.InvalidLiteral;76    if (expected_clauses) |expected| {77        if (expected != clauses_seen) return ParseError.ClauseCountMismatch;78    }79    return solver;80}8182/// Writes `solver` as DIMACS CNF: a `p cnf V C` header, then one line per clause of its literals83/// and a closing 0, so code can hand a solver's formula to another tool. An empty clause added to84/// the solver appears once, as a line holding only 0, and the header counts it. The function writes85/// every clause the solver holds, learned clauses the solver kept included. The call returns only86/// the writer's errors.87pub fn write(writer: *std.Io.Writer, solver: *const sat.Solver) std.Io.Writer.Error!void {88    const empty_clauses: usize = @intFromBool(solver.has_empty_clause);89    try writer.print("p cnf {d} {d}\n", .{90        solver.variableCount(),91        solver.clauseCount() + empty_clauses,92    });93    if (solver.has_empty_clause) {94        try writer.writeAll("0\n");95    }96    for (solver.clauses.items) |clause| {97        for (clause.literals) |literal| {98            try writer.print("{d} ", .{literal.toDimacs()});99        }100        try writer.writeAll("0\n");101    }102}103104test "DIMACS writer preserves the empty clause" {105    var solver = sat.Solver.init(std.testing.allocator);106    defer solver.deinit();107    _ = try solver.addVariable();108    try solver.addClause(&.{sat.Literal.positive(0)});109    try solver.addClause(&.{});110    var buffer: [64]u8 = undefined;111    var stream = std.Io.Writer.fixed(&buffer);112    try write(&stream, &solver);113    const text = stream.buffered();114    try std.testing.expect(std.mem.indexOf(u8, text, "p cnf 1 2\n") != null);115    try std.testing.expect(std.mem.indexOf(u8, text, "\n0\n") != null);116117    var parsed = try parse(std.testing.allocator, text);118    defer parsed.deinit();119    try std.testing.expectEqual(sat.Status.unsat, try parsed.solve());120}121122test "DIMACS parser builds satisfiable formula" {123    var solver = try parse(std.testing.allocator,124        \\c example125        \\p cnf 2 2126        \\1 2 0127        \\-1 0128        \\129    );130    defer solver.deinit();131    try std.testing.expectEqual(sat.Status.sat, try solver.solve());132}133134test "DIMACS writer roundtrips clauses" {135    var solver = sat.Solver.init(std.testing.allocator);136    defer solver.deinit();137    const a = try solver.addVariable();138    const b = try solver.addVariable();139    try solver.addClause(&.{ sat.Literal.positive(a), sat.Literal.negative(b) });140    var buffer: [256]u8 = undefined;141    var stream = std.Io.Writer.fixed(&buffer);142    try write(&stream, &solver);143    const text = stream.buffered();144    try std.testing.expect(std.mem.indexOf(u8, text, "p cnf 2 1\n") != null);145    try std.testing.expect(std.mem.indexOf(u8, text, "1 -2 0\n") != null);146}

1pub const dimacs = @import("dimacs.zig");