A proposed polynomial-time SAT solver concept

I've been working on a polynomial-time SAT solver concept for over a year. This approach doesn't use the resolution rule and directly addresses DPLL's core limitation, where backtracking occurs without retaining state memory.

(archived concept)

DPLL with Conflict Tree

This algorithm is based on decision-only DPLL, with the use of a conflict tree to prevent re-exploring conflicting branches.

1. Building the Conflict Tree: When encountering a conflict, create a leaf in the conflict tree storing every condition that caused the conflict.

function solveSAT {
    conflict = checkConflict(formula, assignment);

    if (conflict && !conflict.skip) {
        return conflict;
    } else {
        conflictTreeLeft = {left: solveSAT(x_i = 0).conditions}
        freePaths = updateConflictTree(conflictTreeLeft, x_i = 1);
        conflictTree = {left: conflictTreeLeft.left, right: solveSAT(x_i = 1, freePaths).conditions}

        return conflictTree;
    }
}

2. Updating the Conflict Tree: When changing a variable after encountering a conflict, check which conflicts in the tree have become solved, and create a free path from the leaves to the root.

function updateConflictTree(conflictTree, variable) {
    for (let i = 0; i < conflictTree.length; i++) {
        let conflict = conflictTree[i];
        let conflictSolved = 1;

        for (let j = 0; j < conflict.length; j++) {
            let condition = conflict[j];

            if (!checkSatisfied(condition, variable)) {
                conflictSolved = 0;
            }
        }

        if (conflictSolved) {
            createFreePath(conflict, conflictTree);
        }
    }
}

3. Using the Conflict Tree: Copy free paths from the left branch of the conflict tree to the right branch, and skip decisions that are outside the free path at the current decision level.

function checkConflict(formula, assignment) {
    let conditions = [];
    let skip = 0;

    for (let i = 0; i < formula.length; i++) {
        let condition = formula[i];

        if (!checkSatisfied(condition, assignment)) {
            conditions.push(condition);
        }
    }

    let currentDecisionFreePathLevel = freePaths[assignment][currentDecision].level;
    let alternativeDecisionFreePathLevel = freePaths[assignment][alternativeDecision].level;

    if (!currentDecisionFreePathLevel) {
        currentDecisionFreePathLevel = 0;
    }

    if (!alternativeDecisionFreePathLevel) {
        alternativeDecisionFreePathLevel = 0;
    }

    if (currentDecisionFreePathLevel < alternativeDecisionFreePathLevel) {
        skip = 1;
    }

    return {
        conditions,
        skip
    };
}

function copyFreePaths(decisionBranch, freePaths) {
    let currentDecisionFreePathLevel = decisionBranch[currentDecision].level;
    let alternativeDecisionFreePathLevel = decisionBranch[alternativeDecision].level;

    if (!currentDecisionFreePathLevel) {
        currentDecisionFreePathLevel = 0;
    }

    if (!alternativeDecisionFreePathLevel) {
        alternativeDecisionFreePathLevel = 0;
    }

    if (currentDecisionFreePathLevel == alternativeDecisionFreePathLevel) {
        for (let i = 0; i < freePaths.length; i++) {
            freePaths[i].level = alternativeDecisionFreePathLevel + 1;
        }

        freePaths[decisionBranch][alternativeDecision] = freePaths;
    }
}

(These snippets are informal pseudocode)

Example: (x8 || x9) && (x8 || -x9) && (-x8 || x9) && (-x8 || -x9)

• x1..x7 = 0
• x8 = 0
• x9 = 0
• Conflict: (x8 || x9)
• Update conflict tree (x9 = 1)
• Free path: x9 = 1
• x9 = 1
• Conflict: (x8 || -x9)
• Backtrack out of the current branch
• Update conflict tree (x8 = 1)
• Free paths: x9 = 0, x9 = 1
• x8 = 1
• x9 = 0
• Conflict: (-x8 || x9)
• Update conflict tree (x9 = 1)
• Free path: x9 = 1
• x9 = 1
• Conflict: (-x8 || -x9)
• Backtrack out of the current branch
• Update conflict tree (x7..1 = 1)
• No free paths
• Formula is unsatisfiable