test_lbfgsb.hs

import Data.List
import qualified Data.Vector as V
import qualified Data.Vector.Storable as VS
import qualified Data.Vector.Generic as VG
import Numeric.AD
-- from http://hackage.haskell.org/package/l-bfgs-b
import qualified Numeric.LBFGSB as LBFGSB
import qualified Numeric.LBFGSB.Result as R

type Weight = Int
type Lit = Int
type Clause = [Lit]

-- (767.0, ..)
test = (f (R.solution result), result)
  where
    result = LBFGSB.minimize m factr pgtol Nothing (replicate nv (Just 0, Just 1)) (VS.replicate nv 0.5) f g
    m = 5
    factr = 1e7
    pgtol = 1e-5
    f :: (VG.Vector v a, Num a) => v a -> a
    f xs = sum [fromIntegral w * product [evalLit l xs | l <- ls] | (w,ls) <- obj]
    g :: VS.Vector Double -> VS.Vector Double
    g = VG.convert . (grad f :: V.Vector Double -> V.Vector Double) . VG.convert

    (nv, nc, wclauses) = wcnf

    obj :: [(Weight, [Lit])]
    obj = [(w, [-l | l <- ls]) | (w,ls) <- wclauses]

    evalLit :: (VG.Vector v a, Num a) => Lit -> v a -> a
    evalLit l xs = if l > 0 then xs VG.! (v - 1) else 1 - (xs VG.! (v - 1))
      where v = abs l

wcnf :: (Int, Int, [(Weight, Clause)])
wcnf = (nv, nc, wclauses)
  where
    nv = read nv'
    nc = read nc'
    [_p, _wcnf_, nv', nc'] = words (head wcnf_file)
    wclauses = do
     l <- tail wcnf_file
     let (w:ls) = words l
     return (read w, map read (init ls))

-- ram_k3_n10.ra1.wcnf
wcnf_file :: [String]
wcnf_file = 
  [ "p wcnf 45 330"
  , " 890 1 2 10 0"
  , " 238 1 3 11 0"
  , " 352 2 3 18 0"
  , " 853 10 11 18 0"
  , " 319 1 4 12 0"
  , " 129 2 4 19 0"
  , " 656 10 12 19 0"
  , " 870 3 4 25 0"
  , " 88 11 12 25 0"
  , " 705 18 19 25 0"
  , " 415 1 5 13 0"
  , " 955 2 5 20 0"
  , " 56 10 13 20 0"
  , " 178 3 5 26 0"
  , " 610 11 13 26 0"
  , " 81 18 20 26 0"
  , " 239 4 5 31 0"
  , " 830 12 13 31 0"
  , " 393 19 20 31 0"
  , " 433 25 26 31 0"
  , " 124 1 6 14 0"
  , " 385 2 6 21 0"
  , " 605 10 14 21 0"
  , " 525 3 6 27 0"
  , " 793 11 14 27 0"
  , " 657 18 21 27 0"
  , " 177 4 6 32 0"
  , " 423 12 14 32 0"
  , " 509 19 21 32 0"
  , " 616 25 27 32 0"
  , " 40 5 6 36 0"
  , " 183 13 14 36 0"
  , " 356 20 21 36 0"
  , " 996 26 27 36 0"
  , " 163 31 32 36 0"
  , " 658 1 7 15 0"
  , " 582 2 7 22 0"
  , " 566 10 15 22 0"
  , " 357 3 7 28 0"
  , " 764 11 15 28 0"
  , " 267 18 22 28 0"
  , " 187 4 7 33 0"
  , " 454 12 15 33 0"
  , " 359 19 22 33 0"
  , " 923 25 28 33 0"
  , " 784 5 7 37 0"
  , " 497 13 15 37 0"
  , " 846 20 22 37 0"
  , " 680 26 28 37 0"
  , " 363 31 33 37 0"
  , " 563 6 7 40 0"
  , " 623 14 15 40 0"
  , " 653 21 22 40 0"
  , " 183 27 28 40 0"
  , " 847 32 33 40 0"
  , " 519 36 37 40 0"
  , " 140 1 8 16 0"
  , " 221 2 8 23 0"
  , " 618 10 16 23 0"
  , " 317 3 8 29 0"
  , " 260 11 16 29 0"
  , " 56 18 23 29 0"
  , " 698 4 8 34 0"
  , " 522 12 16 34 0"
  , " 661 19 23 34 0"
  , " 283 25 29 34 0"
  , " 62 5 8 38 0"
  , " 464 13 16 38 0"
  , " 928 20 23 38 0"
  , " 597 26 29 38 0"
  , " 200 31 34 38 0"
  , " 888 6 8 41 0"
  , " 304 14 16 41 0"
  , " 664 21 23 41 0"
  , " 860 27 29 41 0"
  , " 139 32 34 41 0"
  , " 365 36 38 41 0"
  , " 908 7 8 43 0"
  , " 807 15 16 43 0"
  , " 80 22 23 43 0"
  , " 256 28 29 43 0"
  , " 336 33 34 43 0"
  , " 200 37 38 43 0"
  , " 855 40 41 43 0"
  , " 131 1 9 17 0"
  , " 523 2 9 24 0"
  , " 239 10 17 24 0"
  , " 634 3 9 30 0"
  , " 407 11 17 30 0"
  , " 895 18 24 30 0"
  , " 694 4 9 35 0"
  , " 456 12 17 35 0"
  , " 466 19 24 35 0"
  , " 417 25 30 35 0"
  , " 931 5 9 39 0"
  , " 300 13 17 39 0"
  , " 429 20 24 39 0"
  , " 826 26 30 39 0"
  , " 85 31 35 39 0"
  , " 508 6 9 42 0"
  , " 619 14 17 42 0"
  , " 526 21 24 42 0"
  , " 984 27 30 42 0"
  , " 682 32 35 42 0"
  , " 354 36 39 42 0"
  , " 271 7 9 44 0"
  , " 450 15 17 44 0"
  , " 187 22 24 44 0"
  , " 675 28 30 44 0"
  , " 762 33 35 44 0"
  , " 623 37 39 44 0"
  , " 378 40 42 44 0"
  , " 652 8 9 45 0"
  , " 288 16 17 45 0"
  , " 900 23 24 45 0"
  , " 675 29 30 45 0"
  , " 883 34 35 45 0"
  , " 524 38 39 45 0"
  , " 147 41 42 45 0"
  , " 622 43 44 45 0"
  , " 809 -1 -2 -3 -10 -11 -18 0"
  , " 624 -1 -2 -4 -10 -12 -19 0"
  , " 784 -1 -3 -4 -11 -12 -25 0"
  , " 43 -2 -3 -4 -18 -19 -25 0"
  , " 485 -10 -11 -12 -18 -19 -25 0"
  , " 722 -1 -2 -5 -10 -13 -20 0"
  , " 382 -1 -3 -5 -11 -13 -26 0"
  , " 424 -2 -3 -5 -18 -20 -26 0"
  , " 406 -10 -11 -13 -18 -20 -26 0"
  , " 979 -1 -4 -5 -12 -13 -31 0"
  , " 394 -2 -4 -5 -19 -20 -31 0"
  , " 648 -10 -12 -13 -19 -20 -31 0"
  , " 44 -3 -4 -5 -25 -26 -31 0"
  , " 286 -11 -12 -13 -25 -26 -31 0"
  , " 637 -18 -19 -20 -25 -26 -31 0"
  , " 209 -1 -2 -6 -10 -14 -21 0"
  , " 694 -1 -3 -6 -11 -14 -27 0"
  , " 766 -2 -3 -6 -18 -21 -27 0"
  , " 167 -10 -11 -14 -18 -21 -27 0"
  , " 20 -1 -4 -6 -12 -14 -32 0"
  , " 272 -2 -4 -6 -19 -21 -32 0"
  , " 181 -10 -12 -14 -19 -21 -32 0"
  , " 153 -3 -4 -6 -25 -27 -32 0"
  , " 960 -11 -12 -14 -25 -27 -32 0"
  , " 678 -18 -19 -21 -25 -27 -32 0"
  , " 384 -1 -5 -6 -13 -14 -36 0"
  , " 388 -2 -5 -6 -20 -21 -36 0"
  , " 257 -10 -13 -14 -20 -21 -36 0"
  , " 358 -3 -5 -6 -26 -27 -36 0"
  , " 930 -11 -13 -14 -26 -27 -36 0"
  , " 59 -18 -20 -21 -26 -27 -36 0"
  , " 859 -4 -5 -6 -31 -32 -36 0"
  , " 688 -12 -13 -14 -31 -32 -36 0"
  , " 981 -19 -20 -21 -31 -32 -36 0"
  , " 393 -25 -26 -27 -31 -32 -36 0"
  , " 907 -1 -2 -7 -10 -15 -22 0"
  , " 796 -1 -3 -7 -11 -15 -28 0"
  , " 622 -2 -3 -7 -18 -22 -28 0"
  , " 824 -10 -11 -15 -18 -22 -28 0"
  , " 425 -1 -4 -7 -12 -15 -33 0"
  , " 464 -2 -4 -7 -19 -22 -33 0"
  , " 717 -10 -12 -15 -19 -22 -33 0"
  , " 274 -3 -4 -7 -25 -28 -33 0"
  , " 370 -11 -12 -15 -25 -28 -33 0"
  , " 714 -18 -19 -22 -25 -28 -33 0"
  , " 430 -1 -5 -7 -13 -15 -37 0"
  , " 211 -2 -5 -7 -20 -22 -37 0"
  , " 157 -10 -13 -15 -20 -22 -37 0"
  , " 728 -3 -5 -7 -26 -28 -37 0"
  , " 533 -11 -13 -15 -26 -28 -37 0"
  , " 77 -18 -20 -22 -26 -28 -37 0"
  , " 780 -4 -5 -7 -31 -33 -37 0"
  , " 700 -12 -13 -15 -31 -33 -37 0"
  , " 629 -19 -20 -22 -31 -33 -37 0"
  , " 729 -25 -26 -28 -31 -33 -37 0"
  , " 671 -1 -6 -7 -14 -15 -40 0"
  , " 267 -2 -6 -7 -21 -22 -40 0"
  , " 416 -10 -14 -15 -21 -22 -40 0"
  , " 512 -3 -6 -7 -27 -28 -40 0"
  , " 398 -11 -14 -15 -27 -28 -40 0"
  , " 133 -18 -21 -22 -27 -28 -40 0"
  , " 109 -4 -6 -7 -32 -33 -40 0"
  , " 589 -12 -14 -15 -32 -33 -40 0"
  , " 347 -19 -21 -22 -32 -33 -40 0"
  , " 509 -25 -27 -28 -32 -33 -40 0"
  , " 161 -5 -6 -7 -36 -37 -40 0"
  , " 152 -13 -14 -15 -36 -37 -40 0"
  , " 503 -20 -21 -22 -36 -37 -40 0"
  , " 8 -26 -27 -28 -36 -37 -40 0"
  , " 390 -31 -32 -33 -36 -37 -40 0"
  , " 150 -1 -2 -8 -10 -16 -23 0"
  , " 463 -1 -3 -8 -11 -16 -29 0"
  , " 600 -2 -3 -8 -18 -23 -29 0"
  , " 645 -10 -11 -16 -18 -23 -29 0"
  , " 136 -1 -4 -8 -12 -16 -34 0"
  , " 786 -2 -4 -8 -19 -23 -34 0"
  , " 268 -10 -12 -16 -19 -23 -34 0"
  , " 141 -3 -4 -8 -25 -29 -34 0"
  , " 882 -11 -12 -16 -25 -29 -34 0"
  , " 839 -18 -19 -23 -25 -29 -34 0"
  , " 984 -1 -5 -8 -13 -16 -38 0"
  , " 582 -2 -5 -8 -20 -23 -38 0"
  , " 373 -10 -13 -16 -20 -23 -38 0"
  , " 232 -3 -5 -8 -26 -29 -38 0"
  , " 628 -11 -13 -16 -26 -29 -38 0"
  , " 192 -18 -20 -23 -26 -29 -38 0"
  , " 811 -4 -5 -8 -31 -34 -38 0"
  , " 980 -12 -13 -16 -31 -34 -38 0"
  , " 480 -19 -20 -23 -31 -34 -38 0"
  , " 796 -25 -26 -29 -31 -34 -38 0"
  , " 247 -1 -6 -8 -14 -16 -41 0"
  , " 521 -2 -6 -8 -21 -23 -41 0"
  , " 906 -10 -14 -16 -21 -23 -41 0"
  , " 53 -3 -6 -8 -27 -29 -41 0"
  , " 476 -11 -14 -16 -27 -29 -41 0"
  , " 710 -18 -21 -23 -27 -29 -41 0"
  , " 863 -4 -6 -8 -32 -34 -41 0"
  , " 987 -12 -14 -16 -32 -34 -41 0"
  , " 815 -19 -21 -23 -32 -34 -41 0"
  , " 910 -25 -27 -29 -32 -34 -41 0"
  , " 851 -5 -6 -8 -36 -38 -41 0"
  , " 926 -13 -14 -16 -36 -38 -41 0"
  , " 383 -20 -21 -23 -36 -38 -41 0"
  , " 317 -26 -27 -29 -36 -38 -41 0"
  , " 936 -31 -32 -34 -36 -38 -41 0"
  , " 989 -1 -7 -8 -15 -16 -43 0"
  , " 517 -2 -7 -8 -22 -23 -43 0"
  , " 629 -10 -15 -16 -22 -23 -43 0"
  , " 468 -3 -7 -8 -28 -29 -43 0"
  , " 224 -11 -15 -16 -28 -29 -43 0"
  , " 952 -18 -22 -23 -28 -29 -43 0"
  , " 196 -4 -7 -8 -33 -34 -43 0"
  , " 115 -12 -15 -16 -33 -34 -43 0"
  , " 545 -19 -22 -23 -33 -34 -43 0"
  , " 373 -25 -28 -29 -33 -34 -43 0"
  , " 769 -5 -7 -8 -37 -38 -43 0"
  , " 850 -13 -15 -16 -37 -38 -43 0"
  , " 583 -20 -22 -23 -37 -38 -43 0"
  , " 981 -26 -28 -29 -37 -38 -43 0"
  , " 982 -31 -33 -34 -37 -38 -43 0"
  , " 502 -6 -7 -8 -40 -41 -43 0"
  , " 567 -14 -15 -16 -40 -41 -43 0"
  , " 690 -21 -22 -23 -40 -41 -43 0"
  , " 675 -27 -28 -29 -40 -41 -43 0"
  , " 504 -32 -33 -34 -40 -41 -43 0"
  , " 382 -36 -37 -38 -40 -41 -43 0"
  , " 586 -1 -2 -9 -10 -17 -24 0"
  , " 200 -1 -3 -9 -11 -17 -30 0"
  , " 466 -2 -3 -9 -18 -24 -30 0"
  , " 903 -10 -11 -17 -18 -24 -30 0"
  , " 262 -1 -4 -9 -12 -17 -35 0"
  , " 832 -2 -4 -9 -19 -24 -35 0"
  , " 181 -10 -12 -17 -19 -24 -35 0"
  , " 755 -3 -4 -9 -25 -30 -35 0"
  , " 666 -11 -12 -17 -25 -30 -35 0"
  , " 397 -18 -19 -24 -25 -30 -35 0"
  , " 720 -1 -5 -9 -13 -17 -39 0"
  , " 602 -2 -5 -9 -20 -24 -39 0"
  , " 78 -10 -13 -17 -20 -24 -39 0"
  , " 261 -3 -5 -9 -26 -30 -39 0"
  , " 201 -11 -13 -17 -26 -30 -39 0"
  , " 109 -18 -20 -24 -26 -30 -39 0"
  , " 849 -4 -5 -9 -31 -35 -39 0"
  , " 789 -12 -13 -17 -31 -35 -39 0"
  , " 899 -19 -20 -24 -31 -35 -39 0"
  , " 682 -25 -26 -30 -31 -35 -39 0"
  , " 519 -1 -6 -9 -14 -17 -42 0"
  , " 408 -2 -6 -9 -21 -24 -42 0"
  , " 284 -10 -14 -17 -21 -24 -42 0"
  , " 137 -3 -6 -9 -27 -30 -42 0"
  , " 946 -11 -14 -17 -27 -30 -42 0"
  , " 397 -18 -21 -24 -27 -30 -42 0"
  , " 641 -4 -6 -9 -32 -35 -42 0"
  , " 392 -12 -14 -17 -32 -35 -42 0"
  , " 65 -19 -21 -24 -32 -35 -42 0"
  , " 531 -25 -27 -30 -32 -35 -42 0"
  , " 877 -5 -6 -9 -36 -39 -42 0"
  , " 337 -13 -14 -17 -36 -39 -42 0"
  , " 907 -20 -21 -24 -36 -39 -42 0"
  , " 693 -26 -27 -30 -36 -39 -42 0"
  , " 158 -31 -32 -35 -36 -39 -42 0"
  , " 982 -1 -7 -9 -15 -17 -44 0"
  , " 499 -2 -7 -9 -22 -24 -44 0"
  , " 597 -10 -15 -17 -22 -24 -44 0"
  , " 981 -3 -7 -9 -28 -30 -44 0"
  , " 25 -11 -15 -17 -28 -30 -44 0"
  , " 272 -18 -22 -24 -28 -30 -44 0"
  , " 734 -4 -7 -9 -33 -35 -44 0"
  , " 323 -12 -15 -17 -33 -35 -44 0"
  , " 962 -19 -22 -24 -33 -35 -44 0"
  , " 605 -25 -28 -30 -33 -35 -44 0"
  , " 667 -5 -7 -9 -37 -39 -44 0"
  , " 482 -13 -15 -17 -37 -39 -44 0"
  , " 852 -20 -22 -24 -37 -39 -44 0"
  , " 123 -26 -28 -30 -37 -39 -44 0"
  , " 807 -31 -33 -35 -37 -39 -44 0"
  , " 241 -6 -7 -9 -40 -42 -44 0"
  , " 876 -14 -15 -17 -40 -42 -44 0"
  , " 378 -21 -22 -24 -40 -42 -44 0"
  , " 789 -27 -28 -30 -40 -42 -44 0"
  , " 976 -32 -33 -35 -40 -42 -44 0"
  , " 817 -36 -37 -39 -40 -42 -44 0"
  , " 540 -1 -8 -9 -16 -17 -45 0"
  , " 570 -2 -8 -9 -23 -24 -45 0"
  , " 332 -10 -16 -17 -23 -24 -45 0"
  , " 562 -3 -8 -9 -29 -30 -45 0"
  , " 721 -11 -16 -17 -29 -30 -45 0"
  , " 388 -18 -23 -24 -29 -30 -45 0"
  , " 99 -4 -8 -9 -34 -35 -45 0"
  , " 788 -12 -16 -17 -34 -35 -45 0"
  , " 553 -19 -23 -24 -34 -35 -45 0"
  , " 690 -25 -29 -30 -34 -35 -45 0"
  , " 906 -5 -8 -9 -38 -39 -45 0"
  , " 919 -13 -16 -17 -38 -39 -45 0"
  , " 654 -20 -23 -24 -38 -39 -45 0"
  , " 160 -26 -29 -30 -38 -39 -45 0"
  , " 356 -31 -34 -35 -38 -39 -45 0"
  , " 512 -6 -8 -9 -41 -42 -45 0"
  , " 594 -14 -16 -17 -41 -42 -45 0"
  , " 985 -21 -23 -24 -41 -42 -45 0"
  , " 242 -27 -29 -30 -41 -42 -45 0"
  , " 171 -32 -34 -35 -41 -42 -45 0"
  , " 9 -36 -38 -39 -41 -42 -45 0"
  , " 456 -7 -8 -9 -43 -44 -45 0"
  , " 446 -15 -16 -17 -43 -44 -45 0"
  , " 133 -22 -23 -24 -43 -44 -45 0"
  , " 451 -28 -29 -30 -43 -44 -45 0"
  , " 64 -33 -34 -35 -43 -44 -45 0"
  , " 168 -37 -38 -39 -43 -44 -45 0"
  , " 637 -40 -41 -42 -43 -44 -45 0"
  ]