/*
 * SPDX-FileCopyrightText: 2026 Jacob Bulmash
 * SPDX-License-Identifier: LicenseRef-PolyForm-Strict-1.0.0
 * Copyright 2026 Jacob Bulmash. All rights reserved.
 * Licence: https://polyformproject.org/licenses/strict/1.0.0
 * Required Notice: Copyright 2026 Jacob Bulmash. All rights reserved.
 *
 * Public C11 reference lane for the browser Solver Race.
 * Command: solver INPUT.cnf MAX_FLIPS SEED
 */

#include <stdio.h>
#include <stdint.h>

#define MAX_VARS 2000
#define MAX_CLAUSES 10000
#define MAX_LITERALS 40000
#define MAX_WIDTH 80

static int literals[MAX_LITERALS];
static int offsets[MAX_CLAUSES + 1];
static unsigned char values[MAX_VARS + 1];

static uint32_t next_u32(uint32_t *state) {
    uint32_t x = *state ? *state : 1u;
    x ^= x << 13;
    x ^= x >> 17;
    x ^= x << 5;
    *state = x ? x : 1u;
    return *state;
}

static unsigned long parse_uint(const char *text) {
    unsigned long value = 0;
    if (!text || !*text) return 0;
    while (*text) {
        if (*text < '0' || *text > '9') return 0;
        value = value * 10u + (unsigned long)(*text - '0');
        ++text;
    }
    return value;
}

static int clause_ok(int clause) {
    int i;
    for (i = offsets[clause]; i < offsets[clause + 1]; ++i) {
        int literal = literals[i];
        int variable = literal < 0 ? -literal : literal;
        if (values[variable] == (unsigned char)(literal > 0)) return 1;
    }
    return 0;
}

int main(int argc, char **argv) {
    FILE *input;
    char token[32];
    int variables = 0;
    int clause_count = 0;
    int clause = 0;
    int width = 0;
    int literal_count = 0;
    int literal;
    int index;
    unsigned long max_flips;
    unsigned long flip;
    uint32_t seed;

    if (argc != 4) return 3;
    max_flips = parse_uint(argv[2]);
    seed = (uint32_t)parse_uint(argv[3]);
    if (max_flips < 1 || !seed) return 3;

    input = fopen(argv[1], "r");
    if (!input) return 3;
    while (fscanf(input, "%31s", token) == 1) {
        if (token[0] == 'c') {
            while ((index = fgetc(input)) != '\n' && index != EOF) {}
        } else if (token[0] == 'p') {
            if (fscanf(input, "%31s%d%d", token, &variables, &clause_count) != 3) return 3;
            if (variables < 1 || variables > MAX_VARS || clause_count < 1 || clause_count > MAX_CLAUSES) return 3;
            break;
        }
    }
    while (clause < clause_count && fscanf(input, "%d", &literal) == 1) {
        if (literal == 0) {
            if (width < 1) return 3;
            offsets[++clause] = literal_count;
            width = 0;
        } else {
            int variable = literal < 0 ? -literal : literal;
            if (variable < 1 || variable > variables || width >= MAX_WIDTH || literal_count >= MAX_LITERALS) return 3;
            literals[literal_count++] = literal;
            ++width;
        }
    }
    fclose(input);
    if (clause != clause_count || width != 0) return 3;

    for (index = 1; index <= variables; ++index) {
        values[index] = (unsigned char)(next_u32(&seed) & 1u);
    }
    for (flip = 0; flip <= max_flips; ++flip) {
        int bad = 0;
        int pick = 0;
        int seen = 0;
        for (clause = 0; clause < clause_count; ++clause) {
            if (!clause_ok(clause)) {
                ++bad;
                ++seen;
                if ((next_u32(&seed) % (uint32_t)seen) == 0u) pick = clause;
            }
        }
        if (bad == 0) {
            puts("SATISFIED");
            printf("v");
            for (index = 1; index <= variables; ++index) {
                printf(" %d", values[index] ? index : -index);
            }
            puts(" 0");
            printf("flips %lu\n", flip);
            return 0;
        }
        if (flip == max_flips) break;
        {
            int begin = offsets[pick];
            int width = offsets[pick + 1] - begin;
            int position = begin + (int)(next_u32(&seed) % (uint32_t)width);
            int variable = literals[position];
            if (variable < 0) variable = -variable;
            values[variable] ^= 1u;
        }
    }

    puts("UNKNOWN");
    printf("flips %lu\n", max_flips);
    return 2;
}