write_cnf predictable variable mapping

[weaversa]

It would be nice to have a CNF generation process that used a predictable mapping. Does write_cnf have a predictable mapping of CNF variables to predicate inputs? For example:

sawscript> write_cnf "test" {{ \(x:[3]) y -> x < y }}
sawscript> :q
$ more test
c Result of efficient AIG-to-CNF conversion using package CNF
p cnf 11 17
1 -4 -2 0
1 -4 7 0
1 7 -2 0
-1 -7 2 0
-1 4 2 0
-1 4 -7 0
2 8 3 0
2 -5 8 0
2 -5 3 0
-2 5 -8 0
-2 -8 -3 0
-2 5 -3 0
3 6 -9 0
-3 -6 0
-3 9 0
10 0
-1 0

It looks like the cnf file is being generated via abc's &write_cnf command. This command states:

CNF variable mapping rules:

	           Assume CNF has N variables, with variable IDs running from 0 to N-1.
	           Variable number 0 is not used in the CNF.
	           Variables 1, 2, 3,... <nPOs> represent POs in their natural order.
	           Variables N-<nPIs>, N-<nPIs>+1, N-<nPIs>+2, ... N-1, represent PIs in their natural order.

From this I deduce that x == [5, 6, 7] and y == [8, 9, 10]. Is that right?

I'm not sure this is correct -- I have generated some larger CNF that claim in the header to have, for example 8000 variables, yet the larger variable number showing in the CNF is around 6000.

[weaversa]

From the following experiments I've gained confidence that SAW's write_cnf uses abc's write_cnf command rather than &write_cnf. Also, I don't know the mapping rules for write_cnf. Does anyone know what they are? Or, consider swapping to &write_cnf where the rules are documented in abc?

sawscript> write_cnf "test" {{ \x -> x == 0b0001 }}
sawscript>
$ more test
c Result of efficient AIG-to-CNF conversion using package CNF
p cnf 7 7
1 2 3 4 -5 0
-1 5 0
-1 -4 0
-1 -2 0
-1 -3 0
6 0
1 0

sawscript> write_aig "test.aig" {{ \x -> x == 0b0001 }}
sawscript>
$ abc
UC Berkeley, ABC 1.01 (compiled Dec 20 2020 08:49:16)
abc 01> read test.aig
abc 02> write_cnf test.cnf
CNF stats: Vars =      7. Clauses =       7. Literals =       15.   Time =     0.01 sec
abc 02> ^D***EOF***
[fett@Slave2 test-cryptol-specs]$ more test.cnf
c Result of efficient AIG-to-CNF conversion using package CNF
p cnf 7 7
2 3 4 5 -6 0
-2 6 0
-2 -5 0
-2 -3 0
-2 -4 0
-7 0
2 0

sawscript> write_aig "test" {{ \x -> x == 0b0001 }}
sawscript> :q
$ abc
UC Berkeley, ABC 1.01 (compiled Dec 20 2020 08:49:16)
abc 01> &r test
abc 01> &write_cnf "test.cnf"
CNF stats: Vars =      8. Clauses =       9. Literals =       19. Time =     0.00 sec
abc 01> ^D***EOF***
$ more test.cnf
c Result of efficient AIG-to-CNF conversion using package CNF
p cnf 8 9
2 0
2 -3 0
-2 3 0
3 5 6 7 -8 0
-3 8 0
-3 -7 0
-3 -6 0
-3 -5 0
-4 0

I'm unable to try write_aig_external etc. because I'm using Docker and abc seems to be installed incorrectly? Maybe?

$ docker pull galoisinc/saw:nightly
nightly: Pulling from galoisinc/saw
Digest: sha256:38c6ca19ccd5710166e1ca773372e79a63d4d0d774a09ed8b3b0a72143447610
Status: Image is up to date for galoisinc/saw:nightly
$ docker run --rm -it --mount type=bind,src=/Users,dst=/Users --workdir=$(pwd) --user=$(id -u):$(id -g) --env CRYPTOLPATH=$(pwd) galoisinc/saw:nightly $*

docker.io/galoisinc/saw:nightly
 ┏━━━┓━━━┓━┓━┓━┓
 ┃ ━━┓ ╻ ┃ ┃ ┃ ┃
 ┣━━ ┃ ╻ ┃┓ ╻ ┏┛
 ┗━━━┛━┛━┛┗━┛━┛ version 0.7.0.99 (<non-dev-build>)



sawscript> write_cnf_external "test.cnf" {{ \x -> x == 0b0001 }}

Stack trace:
"write_cnf_external" (<stdin>:1:1-1:19):
abc returned non-zero exit code: ExitFailure 127
Standard output:

Standard error:
abc: error while loading shared libraries: libreadline.so.7: cannot open shared object file: No such file or directory


sawscript> exec "which" ["abc"] ""
[18:13:37.295] "/usr/local/bin/abc\n"

[atomb]

The write_cnf command in SAW calls directly into the C code of ABC at a level in the function call hierarchy that's a little below the top-level command processing, but I think you may be right that it corresponds to the write_cnf command in ABC. The write_cnf_external function uses ABC's &write_cnf, however (and it sounds like that's the better one to choose in this case). Given that we're going to remove the linked-in ABC soon, maybe it makes sense to focus on making sure that write_cnf_external works well? The recent PR #1214 should address that.

[atomb]

And now PR #1320 incorporates a Haskell implementation of AIG and CNF creation, for which we can control variable ordering.

[sauclovian-g]

It sounds like the code that inspired the original report has been removed; is there anything left to do here?

[RyanGlScott]

Indeed, I think we've done all we can do here with the information shown above. If there are further issues with SAW's write_cnf command, let's open separate issues for them.