6
\$\begingroup\$

Given a matrix M all of whose entries are 0 or 1, we want to known whether there exists a non-zero vector v with each element in {-1, 0, 1}, such that Mv = 0.

An easy way to do this is just to try all possible vectors v. The M is m by n then there are 3n - 1 such vectors. But of course this is PPCG, so we don't want to do anything so simple!

Instead, this task is to convert the problem into an instance of Boolean satisfiability problem.

Input

An m by n matrix M written out with one row per line each space separated. The first list has m and n on it, space separated. For example this 3 by 4 matrix M.

3 4
1 1 0 1
0 1 1 0
0 0 1 1

In this case there does not exist a non-zero vector v, all of whose entries are -1,0 or 1 such that Mv = 0.

Output

An instance of 3-SAT in simplified DIMACS format.

The instance of 3-SAT that you output should be satisfiable if and only if there exists a non-zero vector v, all of whose entries are -1,0 or 1 such that Mv = 0.

The file format will be in a simplified version of the DIMACS format using this specification taken from http://www.satcompetition.org/2009/format-benchmarks2009.html


c
c start with comments
c
c 
p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0

The file can start with comments, that is lines begining with the character c. Right after the comments, there is the line p cnf nbvar nbclauses indicating that the instance is in CNF format; nbvar is the exact number of variables appearing in the file; nbclauses is the exact number of clauses contained in the file. Then the clauses follow. Each clause is a sequence of distinct non-null numbers between -nbvar and nbvar ending with 0 on the same line; it cannot contain the opposite literals i and -i simultaneously. Positive numbers denote the corresponding variables. Negative numbers denote the negations of the corresponding variables.


Score

I will test your code on a 20 by 40 matrix and the score will be the total number of non-comment lines in your 3-SAT instance. Smaller is better.

Running time of your code

Your code should take less than 1 minute to run. I don't want to restrict the languages used but I will attempt to test any code I can run otherwise I will just trust the timing you give. For small instances you could of course just compute the answer but this won't work for matrices of the size I will test.

More examples

Your 3-SAT instances for the following matrices should be unsatisfiable.

1 1 0 1
0 1 1 0
0 0 1 1

1 1 0 1 0
0 1 1 0 1
0 0 1 1 0
0 0 0 1 1

1 0 0 1 0 1 1 0 0
1 1 0 0 1 0 1 1 0
0 1 1 0 0 1 0 1 1
0 0 1 1 0 0 1 0 1
0 0 0 1 1 0 0 1 0
0 0 0 0 1 1 0 0 1

1 1 0 1 0 0 1 1 1 0 0 1
1 1 1 0 1 0 0 1 1 1 0 0
0 1 1 1 0 1 0 0 1 1 1 0
0 0 1 1 1 0 1 0 0 1 1 1
0 0 0 1 1 1 0 1 0 0 1 1
0 0 0 0 1 1 1 0 1 0 0 1
0 0 0 0 0 1 1 1 0 1 0 0

Your 3-SAT instances for the following matrices should be satisfiable.

1 1 0 1 1 1 0 
1 1 1 0 1 1 1 
0 1 1 1 0 1 1 
0 0 1 1 1 0 1 
0 0 0 1 1 1 0


1 0 1 0 0 1 0 0 0
0 1 0 1 0 0 1 0 0
0 0 1 0 1 0 0 1 0
0 0 0 1 0 1 0 0 1
0 0 0 0 1 0 1 0 0
0 0 0 0 0 1 0 1 0

1 0 0 1 1 1 0 1 0 0 1 1
0 1 0 0 1 1 1 0 1 0 0 1
0 0 1 0 0 1 1 1 0 1 0 0
0 0 0 1 0 0 1 1 1 0 1 0
0 0 0 0 1 0 0 1 1 1 0 1
0 0 0 0 0 1 0 0 1 1 1 0
0 0 0 0 0 0 1 0 0 1 1 1

A possible short cut for the busy programmer

One possibly easier route to tacking this problem could be to output Pseudo-Boolean Constraints. See page 6 of http://www.cril.univ-artois.fr/PB12/format.pdf for example. There are then different open source tools and libraries which will convert that to 3-SAT.

\$\endgroup\$
10
  • \$\begingroup\$ I edited your question to say that v's entries can individually be {-1, 0, 1}. I'm not 100% sure you intended this, but it made no sense for all elements to be the same value, if you listed 0 as a possible value while disallowing zero vectors. \$\endgroup\$ – orlp Jul 16 '15 at 5:23
  • \$\begingroup\$ I'm starting to believe this is infeasible, unless I'm missing some smart mathematical shortcut. For example, simply consider the satisfiability of one simple mathematical expression with each variable in {0, 1}: a + b + c + d + e + f + g + h + j + i + k - l - m - n - o - p - q - r - s - t - u - v - w - x - z = 0. That's already a massive explosion in clauses, let alone doing it for every possible expansion of +, - or 0! \$\endgroup\$ – orlp Jul 16 '15 at 5:58
  • \$\begingroup\$ @orlp Thank you for the edit. Could st.ewi.tudelft.nl/jsat/content/volume2/JSAT2_1_Een.pdf help? \$\endgroup\$ – user9206 Jul 16 '15 at 7:13
  • \$\begingroup\$ If anything, that confirms my suspicion. Keep in mind the complexity of evaluating one such inequality as shown in the paper, and then doing that m*(3^n - 1) times, one for each expression. That's 2.199023e13 inequalities for your benchmark. \$\endgroup\$ – orlp Jul 16 '15 at 8:05
  • \$\begingroup\$ @orlp What about making a PBO instance and then calling a tool that converts it to 3-sat? \$\endgroup\$ – user9206 Jul 16 '15 at 8:06
3
\$\begingroup\$

OCaml, ≤ 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 -> []
    | n -> 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 <> Cl1(Const true) then clauses := x :: !clauses ;;
let deref = (!);;
let (!) = function
    | V x -> V (-x) 
    | Const c -> Const (not c)
;;

let mkeq (a:var) (b:var) = match a,b with
    | Const true, b -> b
    | Const false, b -> !b
    | a, Const true -> a
    | a, Const false -> !a
    | a,b -> 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 -> b
    | Const true, _ -> Const true
    | _, Const true -> Const true
    | a, Const false -> a
    | a,b -> 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 -> mkor (mkor a b) (mkorl_ tl)
        | a::[] -> a
        | [] -> Const false
    in mkorl_ (List.filter (function | Const false -> false | _ -> true) l)
;;
let nextsums sums (minus1, zero, plus1) =
    let rec nextsums_ prev sums (minus1, zero, plus1) =
    match sums with 
        | cur::next::tl -> 
            ( mkorl [mkand minus1 next; mkand zero cur; mkand plus1 prev] ) ::
            ( nextsums_ cur (next::tl) (minus1, zero, plus1) )
        | cur::_ -> 
            (mkor (mkand zero cur) (mkand plus1 prev)) ::
            ( nextsums_ cur [] (minus1, zero, plus1) )
        | _ -> [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 -> x) ;;

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

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

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

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

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

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

Printf.printf "p cnf %d %d\n" !numvars (List.length !clauses) ;;
List.iter (fun cl -> print_endline (str_clause cl)) !clauses ;;
\$\endgroup\$
1
  • \$\begingroup\$ This looks very impressive ! Did you get a chance to try it on my test cases? \$\endgroup\$ – user9206 Jul 16 '15 at 18:56
1
\$\begingroup\$

Python, n/a

Not a full answer, but this turns matrices into PBS instances that can be transformed into 3-SAT instances by standard tools:

import fileinput

def pos_vec(i): return "x" + str(1 + 2*i)
def neg_vec(i): return "x" + str(1 + 2*i+1)

def print_pseudo(M):
    print(" ".join("1 x" + str(i) for i in range(1, len(M[0])*2 + 1)) + " > 0;")
    for v in range(len(M[0])):
        print("1 {} 1 {} < 2;".format(pos_vec(v), neg_vec(v)))

    for r in range(len(M)):
        terms = []
        for c in range(len(M[0])):
            if M[r][c]:
                terms.append("1 {}".format(pos_vec(c)))
                terms.append("-1 {}".format(neg_vec(c)))
        print(" ".join(terms) + " = 0;")

M = [[int(b) for b in line.split()] for line in fileinput.input()]
print_pseudo(M)
\$\endgroup\$
1

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy