From cca8377dfba9005834f240a1e8498e9ea89b681b Mon Sep 17 00:00:00 2001 From: DualFroz Date: Fri, 28 Aug 2026 15:50:00 +0200 Subject: [PATCH] test: add cdcl, encoder, and difference logic tests --- test/Main.hs | 268 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 268 insertions(+) diff --git a/test/Main.hs b/test/Main.hs index 02e4ebc..d9940c2 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -89,6 +89,79 @@ tests = , check "formula parser evaluates a & (b | ~c) correctly" parserEvaluates , check "formula parser respects precedence (~ then & then ->)" parserPrecedence + + , check "Luby sequence prefix matches reference" lubyPrefixOk + , check "Luby is always a power of two" (all isPowerOfTwo (lubySequence 200)) + + , check ("CDCL agrees with brute force on " ++ show (length randomCnfs) ++ " random CNFs") + (all cdclCorrect randomCnfs) + , check ("CDCL agrees with DPLL on " ++ show (length randomCnfs) ++ " random CNFs") + (all cdclMatchesDpll randomCnfs) + , check ("CDCL finds a verified model for " ++ show (length satisfiableCnfs) + ++ " constructed-satisfiable CNFs") + (all cdclModelVerifies satisfiableCnfs) + , check "CDCL: empty clause is UNSAT" (solveCdcl (CNF [[]]) == CdclUnsat) + , check "CDCL: empty CNF is SAT" (isCdclSat (solveCdcl (CNF []))) + , check "CDCL: (a v b) ^ (~a) forces a=False, b=True" cdclForcedSmall + , check ("CDCL solves Tseitin CNFs equisat to brute force on " + ++ show (length randomFormulas) ++ " formulas") + (all cdclTseitinEquisat randomFormulas) + + , check "CDCL: PHP(3,2) is UNSAT" (solveCdcl (pigeonhole 3 2) == CdclUnsat) + , check "CDCL: PHP(4,3) is UNSAT" (solveCdcl (pigeonhole 4 3) == CdclUnsat) + , check "CDCL: PHP(5,4) is UNSAT" (solveCdcl (pigeonhole 5 4) == CdclUnsat) + , check "CDCL: PHP(6,5) is UNSAT" (solveCdcl (pigeonhole 6 5) == CdclUnsat) + , check "CDCL: PHP(7,6) is UNSAT" (solveCdcl (pigeonhole 7 6) == CdclUnsat) + , check "CDCL: PHP(5,5) is SAT with a verified model" (cdclModelVerifies (pigeonhole 5 5)) + + , check "at-most-one encodes cardinality <= 1 exactly" (all atMostOneCorrect [1 .. 5]) + , check "exactly-one encodes cardinality == 1 exactly" (all exactlyOneCorrect [1 .. 5]) + , check "at-least-one is a single clause of all literals" atLeastOneShape + + , check "queens N=1 is SAT" (isCdclSat (solveCdcl (queens 1))) + , check "queens N=2 is UNSAT" (solveCdcl (queens 2) == CdclUnsat) + , check "queens N=3 is UNSAT" (solveCdcl (queens 3) == CdclUnsat) + , check "queens N=4..10 are SAT with valid placements" + (all queensSatValid [4 .. 10]) + + , check "coloring: K4 needs 4 colors (3 is UNSAT)" + (solveCdcl (coloring 3 completeK4) == CdclUnsat) + , check "coloring: K4 is 4-colorable with a valid coloring" + (coloringSatValid 4 completeK4) + , check "coloring: odd cycle C5 is not 2-colorable" + (solveCdcl (coloring 2 cycleC5) == CdclUnsat) + , check "coloring: odd cycle C5 is 3-colorable with a valid coloring" + (coloringSatValid 3 cycleC5) + , check "coloring: even cycle C6 is 2-colorable with a valid coloring" + (coloringSatValid 2 cycleC6) + , check "coloring: bipartite graph is 2-colorable with a valid coloring" + (coloringSatValid 2 bipartite) + + , check "sudoku: a real puzzle is solved with a valid grid" + (sudokuSolvesValid sudokuPuzzle) + , check "sudoku: two identical givens in a row make it UNSAT" + (solveCdcl (sudoku 3 [(1, 1, 5), (1, 2, 5)]) == CdclUnsat) + + , check "preprocess: subsumption preserves the model set on random CNFs" + (all (\c -> modelSetEq c (subsume c)) randomCnfs) + , check "preprocess: self-subsuming resolution preserves the model set" + (all (\c -> modelSetEq c (selfSubsume c)) randomCnfs) + , check "preprocess: unit propagation is equisatisfiable and sound" + (all unitPropSound randomCnfs) + , check "preprocess: pure literal elimination is equisatisfiable" + (all pureElimEquisat randomCnfs) + , check ("preprocess: full pipeline is correct on " ++ show (length randomCnfs) + ++ " random CNFs") + (all preprocessCorrect randomCnfs) + + , check "difference logic: a negative cycle is UNSAT" (solveDl dlNegCycle == DlUnsat) + , check "difference logic: a feasible system is SAT with a verified model" + (dlSatVerified dlFeasible) + , check "difference logic: disjunctive constraint picks a feasible branch" + (dlSatVerified dlDisjunctive) + , check ("difference logic agrees with bounded brute force on " + ++ show (length randomDlProblems) ++ " random problems") + (all dlAgrees randomDlProblems) ] check :: String -> Bool -> IO Bool @@ -302,3 +375,198 @@ randLeaf s0 = let (k, s1) = randInt 0 (length atomPool - 1) s0 randomFormulas :: [Formula] randomFormulas = fst (genN 200 (randFormula 3) 4242) + +isCdclSat :: CdclResult -> Bool +isCdclSat (CdclSat _) = True +isCdclSat CdclUnsat = False + +lubyPrefixOk :: Bool +lubyPrefixOk = + lubySequence 15 == [1, 1, 2, 1, 1, 2, 4, 1, 1, 2, 1, 1, 2, 4, 8] + +isPowerOfTwo :: Int -> Bool +isPowerOfTwo n = n > 0 && (n .&. (n - 1)) == 0 + +cdclCorrect :: CNF -> Bool +cdclCorrect cnf = case solveCdcl cnf of + CdclSat model -> satisfies model cnf && bruteForceSat cnf + CdclUnsat -> not (bruteForceSat cnf) + +cdclMatchesDpll :: CNF -> Bool +cdclMatchesDpll cnf = isCdclSat (solveCdcl cnf) == isSat (solve cnf) + +cdclModelVerifies :: CNF -> Bool +cdclModelVerifies cnf = case solveCdcl cnf of + CdclSat model -> satisfies model cnf + CdclUnsat -> False + +cdclForcedSmall :: Bool +cdclForcedSmall = case solveCdcl cnfSatSmall of + CdclSat model -> Map.lookup (Var 1) model == Just False + && Map.lookup (Var 2) model == Just True + CdclUnsat -> False + +cdclTseitinEquisat :: Formula -> Bool +cdclTseitinEquisat f = isCdclSat (solveCdcl (tsCnf (tseitin f))) == formulaSat f + +countTrue :: Int -> Assignment -> Int +countTrue n asn = length [ () | i <- [1 .. n], Map.findWithDefault False (Var i) asn ] + +atMostOneCorrect :: Int -> Bool +atMostOneCorrect n = + all (\asn -> satisfies asn cnf == (countTrue n asn <= 1)) (allAssignments vs) + where + lits = [ posLit (Var i) | i <- [1 .. n] ] + cnf = CNF (atMostOne lits) + vs = [ Var i | i <- [1 .. n] ] + +exactlyOneCorrect :: Int -> Bool +exactlyOneCorrect n = + all (\asn -> satisfies asn cnf == (countTrue n asn == 1)) (allAssignments vs) + where + lits = [ posLit (Var i) | i <- [1 .. n] ] + cnf = CNF (exactlyOne lits) + vs = [ Var i | i <- [1 .. n] ] + +atLeastOneShape :: Bool +atLeastOneShape = atLeastOne lits == [lits] + where lits = [ posLit (Var 1), posLit (Var 2), posLit (Var 3) ] + +queensSatValid :: Int -> Bool +queensSatValid n = case solveCdcl (queens n) of + CdclSat model -> validQueens n model + CdclUnsat -> False + +coloringSatValid :: Int -> Graph -> Bool +coloringSatValid k g = case solveCdcl (coloring k g) of + CdclSat model -> validColoring k g model + CdclUnsat -> False + +completeK4 :: Graph +completeK4 = Graph 4 [(1, 2), (1, 3), (1, 4), (2, 3), (2, 4), (3, 4)] + +cycleC5 :: Graph +cycleC5 = Graph 5 [(1, 2), (2, 3), (3, 4), (4, 5), (5, 1)] + +cycleC6 :: Graph +cycleC6 = Graph 6 [(1, 2), (2, 3), (3, 4), (4, 5), (5, 6), (6, 1)] + +bipartite :: Graph +bipartite = Graph 6 [(1, 4), (1, 5), (2, 5), (2, 6), (3, 4), (3, 6)] + +sudokuSolvesValid :: [(Int, Int, Int)] -> Bool +sudokuSolvesValid givens = case solveCdcl (sudoku 3 givens) of + CdclSat model -> validSudoku 3 givens model + CdclUnsat -> False + +sudokuPuzzle :: [(Int, Int, Int)] +sudokuPuzzle = parseGrid 3 (unlines + [ "530070000" + , "600195000" + , "098000060" + , "800060003" + , "400803001" + , "700020006" + , "060000280" + , "000419005" + , "000080079" ]) + +modelSetEq :: CNF -> CNF -> Bool +modelSetEq a b = + all (\asn -> satisfies asn a == satisfies asn b) (allAssignments vs) + where vs = nub (allVars a ++ allVars b) + +unitPropSound :: CNF -> Bool +unitPropSound cnf = case unitPropagate cnf of + Nothing -> not (bruteForceSat cnf) + Just (units, residual) -> + bruteForceSat cnf == bruteForceSat residual + && case solveCdcl residual of + CdclSat m -> satisfies (completeModel cnf (reconstruct units m)) cnf + CdclUnsat -> True + +pureElimEquisat :: CNF -> Bool +pureElimEquisat cnf = + bruteForceSat cnf == bruteForceSat residual + && case solveCdcl residual of + CdclSat m -> satisfies (completeModel cnf (reconstruct pures m)) cnf + CdclUnsat -> True + where (pures, residual) = pureLiteralElim cnf + +preprocessCorrect :: CNF -> Bool +preprocessCorrect cnf = case preprocess cnf of + Unsatisfiable -> not (bruteForceSat cnf) + Simplified fixed residual -> + bruteForceSat cnf == bruteForceSat residual + && case solveCdcl residual of + CdclSat m -> satisfies (completeModel cnf (reconstruct fixed m)) cnf + CdclUnsat -> True + +dlNegCycle :: DlProblem +dlNegCycle = DlProblem + [DiffAtom 1 2 0, DiffAtom 2 3 0, DiffAtom 3 1 (-1)] + (CNF [[posLit (Var 1)], [posLit (Var 2)], [posLit (Var 3)]]) + +dlFeasible :: DlProblem +dlFeasible = DlProblem + [DiffAtom 1 2 2, DiffAtom 2 3 3] + (CNF [[posLit (Var 1)], [posLit (Var 2)]]) + +dlDisjunctive :: DlProblem +dlDisjunctive = DlProblem + [DiffAtom 1 2 (-1), DiffAtom 2 1 (-1)] + (CNF [[posLit (Var 1), posLit (Var 2)]]) + +dlSatVerified :: DlProblem -> Bool +dlSatVerified prob = case solveDl prob of + DlSat model -> dlModelSatisfies prob model + DlUnsat -> False + +dlAgrees :: DlProblem -> Bool +dlAgrees prob = + let brute = dlBruteSat prob + in case solveDl prob of + DlSat model -> brute && dlModelSatisfies prob model + DlUnsat -> not brute + +dlBruteSat :: DlProblem -> Bool +dlBruteSat prob = + any (\assignment -> dlModelSatisfies prob (Map.fromList assignment)) (intAssignments vars) + where vars = nub (concatMap (\a -> [dlLhs a, dlRhs a]) (dlAtoms prob)) + +intAssignments :: [Int] -> [[(Int, Int)]] +intAssignments = go + where + domain = [-6 .. 6] + go [] = [[]] + go (v : vs) = [ (v, d) : rest | d <- domain, rest <- go vs ] + +randDlAtom :: Int -> Seed -> (DiffAtom, Seed) +randDlAtom numDlVars s0 = + let (a, s1) = randInt 1 numDlVars s0 + (b, s2) = randInt 1 numDlVars s1 + (w, s3) = randInt (-2) 2 s2 + in (DiffAtom a b w, s3) + +randDlLit :: Int -> Seed -> (Lit, Seed) +randDlLit numAtoms s0 = + let (v, s1) = randInt 1 numAtoms s0 + (b, s2) = randBool s1 + in (Lit (Var v) b, s2) + +randDlClause :: Int -> Seed -> (Clause, Seed) +randDlClause numAtoms s0 = + let (len, s1) = randInt 1 2 s0 + in genN len (randDlLit numAtoms) s1 + +randDlProblem :: Seed -> (DlProblem, Seed) +randDlProblem s0 = + let numAtoms = 4 + numDlVars = 3 + (as, s1) = genN numAtoms (randDlAtom numDlVars) s0 + (nc, s2) = randInt 1 5 s1 + (cls, s3) = genN nc (randDlClause numAtoms) s2 + in (DlProblem as (CNF cls), s3) + +randomDlProblems :: [DlProblem] +randomDlProblems = fst (genN 60 randDlProblem 20240828)