Conversion to Boolean satisfiability
OCaml, &leq; 475318

After defining the basic logic gates (I ended up using only AND and OR), I compose them to make a variable for each of the possible partial sums of a row of M and v. A total of O(mn2) variables/clauses are used. This is an initial effort that doesn't make any attempt to simplify the formula. In the worst case (a matrix with no zeroes), it generates 475,318 clauses for a 20x40 matrix.



let rec genlist f n = 
    match n with
    | 0 -&gt; []
    | n -&gt; let e = f() in e :: genlist f (n-1)
;;

let numvars = ref 0 ;;
type var = V of int | Const of bool;;
let mkv () = incr numvars; V !numvars;;
type clause = Cl1 of var | Cl2 of var*var | Cl3 of var*var*var ;;
let clauses = ref [] ;;
let req (x:clause) = if x &lt;&gt; Cl1(Const true) then clauses := x :: !clauses ;;
let deref = (!);;
let (!) = function
    | V x -&gt; V (-x) 
    | Const c -&gt; Const (not c)
;;

let mkeq (a:var) (b:var) = match a,b with
    | Const true, b -&gt; b
    | Const false, b -&gt; !b
    | a, Const true -&gt; a
    | a, Const false -&gt; !a
    | a,b -&gt; let v = mkv() in
    req@@Cl3 ( !v, a, !b ) ;
    req@@Cl3 ( !v, !b, a ) ;
    req@@Cl3 ( v, a, b ) ;
    req@@Cl3 ( v, !a, !b );
    v 
;;

let mkxor a b = ! (mkeq a b) ;;

let mkor (a:var) (b:var) = match a,b with
    | Const false, b -&gt; b
    | Const true, _ -&gt; Const true
    | _, Const true -&gt; Const true
    | a, Const false -&gt; a
    | a,b -&gt; let v = mkv() in
    req@@Cl2 ( v, !a ) ;
    req@@Cl2 ( v, !b ) ;
    req@@Cl3 ( !v, a, b ) ;
    v 
;;

let mkand a b = ! (mkor !a !b) ;;


let mkorl l = 
    let rec mkorl_ = function
        | a::b::tl -&gt; mkor (mkor a b) (mkorl_ tl)
        | a::[] -&gt; a
        | [] -&gt; Const false
    in mkorl_ (List.filter (function | Const false -&gt; false | _ -&gt; true) l)
;;
let nextsums sums (minus1, zero, plus1) =
    let rec nextsums_ prev sums (minus1, zero, plus1) =
    match sums with 
        | cur::next::tl -&gt; 
            ( mkorl [mkand minus1 next; mkand zero cur; mkand plus1 prev] ) ::
            ( nextsums_ cur (next::tl) (minus1, zero, plus1) )
        | cur::_ -&gt; 
            (mkor (mkand zero cur) (mkand plus1 prev)) ::
            ( nextsums_ cur [] (minus1, zero, plus1) )
        | _ -&gt; [mkand plus1 prev]
    in 
    (mkand minus1 (List.hd sums)) ::
    nextsums_ (Const false) sums (minus1, zero, plus1)
;;

let rec entry_zero row v sums maxsum =
    if row=[] then List.nth sums maxsum else
    if List.hd row = 0 then entry_zero (List.tl row) (List.tl v) sums maxsum else
    let (a,b,c) = List.hd v in
    let elemv = if List.hd row = -1 then (c,b,a) else (a,b,c) in
    entry_zero (List.tl row) (List.tl v) (nextsums sums elemv) (maxsum+1)
;;


let req1of3 (a,b,c) = 
    req@@Cl2(!a, !b);
    req@@Cl2(!a, !c);
    req@@Cl2(!b, !c);
    req@@Cl3(a, b, c);;

let rdint () = Scanf.bscanf Scanf.Scanning.stdin " %d" (fun x -&gt; x) ;;

let m = rdint();;
let n = rdint();;

let vec = genlist (fun () -&gt; (mkv(), mkv(), mkv()) ) n;;
List.iter req1of3 vec;;

let mat = genlist (fun () -&gt; genlist rdint n) m;;

List.iter (fun row -&gt; req@@Cl1 (entry_zero row vec [Const true] 0) ) mat;;

let nonzeros = List.map (function _,z,_ -&gt; !z) vec ;; 
req@@Cl1 (mkorl nonzeros) ;;

exception Bug of string;;
let str_clause (cl:clause) = match cl with
    | Cl1(V a) -&gt; Printf.sprintf "%d 0" a
    | Cl2(V a,V b) -&gt; Printf.sprintf "%d %d 0" a b
    | Cl3(V a,V b,V c) -&gt; Printf.sprintf "%d %d %d 0" a b c
    | _ -&gt; raise @@ Bug "there seems to be";;
let (!) = deref;;

Printf.printf "p cnf %d %d\n" !numvars (List.length !clauses) ;;
List.iter (fun cl -&gt; print_endline (str_clause cl)) !clauses ;;