meelgroup / bosphorus Goto Github PK

View Code? Open in Web Editor NEW

64.0 7.0 18.0 580 KB

Bosphorus, ANF simplifier and solver, and ANF-to-CNF converter

License: Other

CMake 17.36% C 0.94% C++ 71.56% Python 9.07% Shell 1.07%

anf cryptoanalysis sat cnf dimacs anf-simplifications

bosphorus's People

Contributors

Stargazers

Watchers

Forkers

shrawant vzhn cassiersg avinashvarna siweisun csy1234 leonmelis 061012 ozppupbg erwinhaasnoot aljungberg mherasg tinylabs liuguozhen0 kknckk minionsjay flash-lhr russell-project-org

bosphorus's Issues

Multi-thread trigger assertion

The operation succeeds when using the default number of threads, but the assertion fails after setting the number of threads.
OS： 5.17.0-kali3-amd64
CPU：Intel(R) Core(TM) i5-8300H CPU @ 2.30GHz

r05.cnf.txt

Unexpected behavior on a factored system

I tried to solve the following system which is not in ANF (ternary factorized system):

(x1*x4 + x0*x5)*x8 + (x3*x4 + x0*x7)*x9 + (x3*x6 + x2*x7)*x10 + (x2*x5 + x1*x6)*x11
(x2*x4 + x0*x6)*x8 + (x3*x5 + x1*x7)*x9 + (x2*x4 + x0*x6)*x10 + (x3*x5 + x1*x7)*x11
(x2*x5 + x1*x6)*x8 + (x1*x4 + x0*x5)*x9 + (x3*x4 + x0*x7)*x10 + (x3*x6 + x2*x7)*x11
(x3*x4 + x0*x7)*x8 + (x3*x6 + x2*x7)*x9 + (x2*x5 + x1*x6)*x10 + (x1*x4 + x0*x5)*x11
(x3*x5 + x1*x7)*x8 + (x2*x4 + x0*x6)*x9 + (x3*x5 + x1*x7)*x10 + (x2*x4 + x0*x6)*x11
(x3*x6 + x2*x7)*x8 + (x2*x5 + x1*x6)*x9 + (x1*x4 + x0*x5)*x10 + (x3*x4 + x0*x7)*x11 + 1

However, a bosphorus call on this system still produce a solution (which is not a solution
of the problem however). After inspecting the output with option --anfwrite, it seems that
some parsing is still going on and that a system is somehow produced, which is pretty odd.

Is it a feature, or should the parser raise an error because the system is not in ANF ?

Thoughts on Bosphorus

Hi Mate,

Some of the promised thoughts on Bosphorus. Along the way I even implemented a PoC for the parser. Hopefully some of it will find its way back into bosphorus proper. My C++ skills are unfortunately lacking, I wish I could help you more there.

Bosphorus is really great as an API/preprocessor step into CMS and we cannot thank you enough for all the resources you and the meelgroup have made available. For us, as software engineers, SAT is quite a daunting subject and the papers on it are quite difficult to comprehend. But these tools, in addition to major increases in computational power, means I think it is becoming easier to grasp the subject, and to build practical applications around SAT.

Monomials considered harmful?

As mentioned, our use-cases often result in very large polynomials, and we've ran into a few bottlenecks, one of which is the algorithm used in subsitute.

I think more generally these performance bottlenecks are due to BRiAl. BRiAl really is a lib intended for mathematicians, but unfortunately the most natural way to think about polynomials (as an array of monomials, which itself is an array of variables/terms), is also likely to lead to highly inefficient code. Using Zero-suppressed Decision Diagrams (ZDDs) for these polynomials, as done by Brickenstein/Dreyer in PolyBoRi was really a stroke of genius, but this puts a lot of cognitive strain on the use of the lib if one really needs things to be performant.

A lot of the intuition I have for ZDD's & BoolPoly's has come from our frustration with the Python front-end for BRiAl, both in its need of the full Sage suite as a dependency, as well as its general slow-ness (crossing the python/c boundary too often is a huge performance killer). A further big dose of Not-Invented-Here, as well as a general interest in understanding what ZDDs are, led me to create my own pure-python lib for handling bool polynomials in ZDDs.

For me, it was really important to realize that with BRiAl one should think of a polynomial not being stored as an ANF: x(1)*x(2)*(x3) + x(1)*(x3) + x(2)*x(3), but in a recursive tree-like form where nodes look like so value * hi-branch + lo-branch). Fully extended, the BoolPoly actually looks more like this: x(1) * (x(2) * (x(3) * (1 + 0)) + (x(3) * (1 + 0) + 0)) + (x(2) * (x(3) * (1 + 0) + 0) + 0) (one should remember that terms are always deduplicated).

This branching structure, in combination with node deduplication, makes storage of boolpolys very efficient. It also makes monomial iteration very tricky, and algorithms that use monomial iteration nearly all terribly inefficient. I would maybe even wager that in code written for performance, no instances of BooleMonomials should be used. A quick leads to many uses of BooleMonomials, I've looked at the first 4/5 most salient ones:

BLib::do_sample_and_clone

for (const BooleMonomial& mono : poly)
    if (unique.find(mono.hash()) == unique.end())
        ++out;

This code seems to try and count the amount of monomials in poly that are also in the set unique. Basically, counting the size of the monomial-wise intersect of the two polys. Actually, this is might be an interesting problem and I will put this on my list to try and solve.

for (const BooleMonomial& mono : equations.back())
            unique.insert(mono.hash());

unique seems to need to be a set, because we do not want the XOR extinguishing behaviour that regular polynomials have. This seems to make necessary a monomial-wise union on the two polys. Added to list of functions my ZDD lib needs to support :)

BLib::subsitute

for (const BooleMonomial& mono : poly) {
    if (!mono.reducibleBy(from_var)) {
        quotient += mono;
    }
}

This one we've already looked at and fixed :)
One issue remains, I think the swap function is a potential memory leak. We noticed that Bosphorus memory use inexplicably seems to rise, even as the total size of the polys seem to decrease. I think that is because the quotientsare not properly garbage-collected anymore after having been swapped

cnf.cpp

There is a lot of use of BooleMonomials (even poly iteration) in this file. Honestly, I don't really understand what goes on here, but I would be willing to listen to explanations and see if we can come up with algorithms that are more suitable to BRiAl in the CNF conversions.

In fact.. has any work been done on building SAT solvers that work directly on BoolPoly's in ZDD form?

Parser

Another bottleneck is the Parser. Actually, I don't think it is the parser so much, as it is the ANF format that is used for representing polys. It would be interesting to use a format that allows polys to be expressed in tree form, and that support references of one node to another. Basically, a textual format close to how BRiAl stores polys in ZDD's. Is there any standard on any format like that?

Further, it is possible to pre-process a poly from an ANF file a bit, so that building the ZDD from the ANF becomes way more efficient. Stringified forms of polys that BRiAl outputs are generally keeping to variable ordering. This is essentially due to the "stringify"'s natural starting point is the head node of the tree and then recursively descending to the terminal nodes. Unfortunately, rebuilding a poly from the ANF form means that a lot of work is constantly being done descending down the tree as well.

x1 * x2, means that there is a singleton x1 that is updated to now have a reference to x2 on its hi-branch. Multiplying by x3, will mean going down through x1 to x2, and updating the hi-branch of x2 to a reference to x3. For 1000s of variables, this means going down the same tree 1000s of times. One that grows with every variable being added.

Handling these monomials in reverse order, that is, we first take x2 and then multiply by x1, means we only update the singleton x to refernce the x2 node. Similarly, multiplying by x0 means that we update the singleton x0 to reference the x1 node.

The same goes for XOR, but over the lo-branch. Experimentally, I can verify that the same holds true even for more complex ANDs and XORs. You can look at the following gist for a short benchmark script that makes use of sage's BRiAl to generate the polys.

https://gist.github.com/ErwinHaasnoot/1d6a5aa1296174e31d08585a6d0a6f81

Check the difference between a reverse-order parser, and a regular-order parser. There might be some quirks there related to how python works, but I think it would be fairly easy to try and implement the reverse-order parsing in Bosphorus and still, probably, get a significant speed-up.

With the given parameters in the gist, the results are as follows:

Original parser: 11.58
New parser: 0.53
Speed-up: 21.86

I think this speed-up gets larger as the polynomial gets more complex. Hopefully this will be interesting enough for you to look into!

Ok, I think this is enough for now :) I'm sure there is enough here to digest. Also, some interesting work for me left to do as well irt the monomial set functions.

Docker build fails due to deprecation of Ubuntu 19.04

Hi!

I've been dabbling in SAT solving recently and came across this great tool. Unfortunately, my first attempt at building the docker image failed.

Sending build context to Docker daemon  994.8kB
Step 1/36 : FROM ubuntu:19.04 as builder
 ---> c88ac1f841b7
Step 2/36 : LABEL maintainer="Mate Soos"
 ---> Using cache
 ---> afd290d3adb6
Step 3/36 : LABEL version="1.0"
 ---> Using cache
 ---> f596b3719289
Step 4/36 : LABEL Description="Bosphorus"
 ---> Using cache
 ---> 71175ca36d25
Step 5/36 : ENV DEBIAN_FRONTEND=noninteractive
 ---> Running in 2d3195720178
Removing intermediate container 2d3195720178
 ---> b1f3cc1f335b
Step 6/36 : RUN apt-get update
 ---> Running in 3ab93a802801
Ign:1 http://archive.ubuntu.com/ubuntu disco InRelease
Ign:2 http://archive.ubuntu.com/ubuntu disco-updates InRelease
Ign:3 http://archive.ubuntu.com/ubuntu disco-backports InRelease
Err:4 http://archive.ubuntu.com/ubuntu disco Release
  404  Not Found [IP: 91.189.88.152 80]
Err:5 http://archive.ubuntu.com/ubuntu disco-updates Release
  404  Not Found [IP: 91.189.88.152 80]
Err:6 http://archive.ubuntu.com/ubuntu disco-backports Release
  404  Not Found [IP: 91.189.88.152 80]
Ign:7 http://security.ubuntu.com/ubuntu disco-security InRelease
Err:8 http://security.ubuntu.com/ubuntu disco-security Release
  404  Not Found [IP: 91.189.91.39 80]
Reading package lists...
E: The repository 'http://archive.ubuntu.com/ubuntu disco Release' does not have a Release file.
E: The repository 'http://archive.ubuntu.com/ubuntu disco-updates Release' does not have a Release file.
E: The repository 'http://archive.ubuntu.com/ubuntu disco-backports Release' does not have a Release file.
E: The repository 'http://security.ubuntu.com/ubuntu disco-security Release' does not have a Release file.
The command '/bin/sh -c apt-get update' returned a non-zero code: 100

This is due to ubuntu 19.04 no longer being supported by Canonical.

https://ubuntu.com/about/release-cycle

Fortunately, the build seems to work fine on Ubuntu 19.10. Ideally however the image would be upgraded to an LTS version of ubuntu (20.04), as 19.10 is slated for deprecation in 6 months with the release of Ubuntu 20.10.

Moving the image to Ubuntu 20.04 is proving difficult. First off, it fails early in the build process due to tzdata now requiring a dialog. This is remedied by adding the following line near the top of the Dockerfile

ENV DEBIAN_FRONTEND=noninteractive

However, Cryptominisat is failing to build after that:

/usr/bin/ld: /usr/lib/gcc/x86_64-linux-gnu/9/libstdc++.a(eh_globals.o): undefined reference to symbol '__tls_get_addr@@GLIBC_2.3'
/usr/bin/ld: /lib/x86_64-linux-gnu/ld-linux-x86-64.so.2: error adding symbols: DSO missing from command line
collect2: error: ld returned 1 exit status
make[2]: *** [cmsat5-src/CMakeFiles/cryptominisat5.dir/build.make:118: cryptominisat5] Error 1
make[1]: *** [CMakeFiles/Makefile2:155: cmsat5-src/CMakeFiles/cryptominisat5.dir/all] Error 2
make: *** [Makefile:130: all] Error 2

I tried upgrading cryptominisat to 5.6.8

# build CMS
WORKDIR /
RUN wget https://github.com/msoos/cryptominisat/archive/5.6.8.tar.gz \
    && tar -xvf 5.6.8.tar.gz
WORKDIR /cryptominisat-5.6.8
RUN mkdir build
WORKDIR /cryptominisat-5.6.8/build
RUN cmake -DSTATICCOMPILE=ON .. \
    && make -j2 \
    && make install \
    && rm -rf *

but this brings up a slightly different error.

/usr/bin/ld: attempted static link of dynamic object `/usr/lib/x86_64-linux-gnu/libboost_program_options.so.1.71.0'
collect2: error: ld returned 1 exit status
make[2]: *** [cmsat5-src/CMakeFiles/cryptominisat5-bin.dir/build.make:118: cryptominisat5] Error 1
make[1]: *** [CMakeFiles/Makefile2:155: cmsat5-src/CMakeFiles/cryptominisat5-bin.dir/all] Error 2
make: *** [Makefile:130: all] Error 2

I would love to help out here, but I am not very familiar with this type of buildchain and it seems like an easily correctable issue by someone who is more knowledgeable about the project.

If I can be of any more assistance here please let me know!

All the best

terminate called after throwing an instance of 'polybori::PBoRiError'

Error running: Segmentation fault (core dumped)

Dear Mr Soos，
I need your help. I have installed "bosphorus" on my computer before and it can be used normally, but when I install "bosphorus" on a server platform, I use a "test.anf" file that has been verified on my computer When the server platform was running, a "Segmentation fault (core dumped)" error occurred.

ANF to CNF conversion

Dear developer team,

Is it possible to add an option to the tool, so that one can convert an ANF to it's CNF equivalent without creating the new variables? In the current version, when the ANF representation is converted to it's CNF equivalent, a lot of new variables are created, but in many cases we need to convert an ANF representation to the minimized (or approximately minimized) CNF representation without generating new variables. Thank you for creating such a useful tool.

Kind regards,
Hosein

Bosphorus reports unsat but CryptoMiniSat can solve this SHA-256 CNF

CryptoMiniSat easily solves this attached CNF:

cryptominisat5 d17-55.cnf
c BreakID not compiled in, disabling
c CryptoMiniSat version 5.8.0
c CMS Copyright Mate Soos ([email protected])
c CMS SHA revision 6477e8bc43b0fda7038965bb148b64b8637c804b
...
c Reading file 'd17-55.cnf'
c -- header says num vars:          93423
c -- header says num clauses:      232905
c -- clauses added: 233216
c -- xor clauses added: 0
c -- vars added 93423
c Parsing time: 0.06 s
c clause size stats. size3: 46187 size4: 0 size5: 0 larger: 0
...
c Mem used                 : 37.34       MB
c Total time (this thread) : 3.62
s SATISFIABLE
v 1 2 -3 4 -5 6 -7 -8 -9 10 11 12 -13 -14 -15 16 -17 -18 19 20 21 22 -23 24 -25
...

But Bosphorus fails on the same:

docker run --rm -v `pwd`/:/dat/ msoos/bosphorus --cnfread /dat/d17-55.cnf --solve
c Bosphorus SHA revision 35022458344323665b24257732093a3444b4c69c
c Executed with command line: /usr/local/bin/bosphorus --cnfread /dat/d17-55.cnf --solve
c Compilation env CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS =  -Wall -Wextra -Wunused -pedantic -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -mtune=native -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -ggdb3 | COMPILE_DEFINES =  | STATICCOMPILE = ON | ONLY_SIMPLE =  | Boost_FOUND = TRUE | STATS =  | SQLITE3_FOUND =  | ZLIB_FOUND = TRUE | VALGRIND_FOUND =  | ENABLE_TESTING =  | M4RI_FOUND = TRUE | SLOW_DEBUG =  | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE =  | PYTHON_LIBRARY =  | PYTHON_INCLUDE_DIRS =  | MY_TARGETS =  | LARGEMEM =  | LIMITMEM =  | compilation date time = Apr 29 2021 22:02:25
c --- Configuration --
c maxTime = 1.00e+20
c XL simp (deg = 1; s = 30.00+4.00): 1
c EL simp (s = 30.00): 1
c SAT simp (10000:100000): 1
 using 1 threads
c Cut num: 5
c Brickenstein cutoff: 10
c --------------------
c [cnf-to-anf] Chopping up CNF with 93423 variables.
c [anf-to-cnf] Constructing ANF from CNF. New vars: 0 Extra cls needed : 0 Chunked cls: 233216 Vars: 93423
c [CNF Input] read in T: 0.65
c ---- ANF stats -----
c Num total vars: 93423
c Num free vars: 93423
c Num equations: 233216
c Num monoms in eqs: 513454
c Max deg in eqs: 3
c Simple XORs: 311
c Num vars set: 0
c Num vars replaced: 0
c --------------------
c [ANF hash] Calculating ANF hash...
c [ANF hash] Done. T: 0.03
c Simplifying....
c [boshp] Running iterative simplification...
c [ANF prop] Running ANF propagation...
c [ANF prop] Left eqs: 210811 T: 0.23
c [iter-simp] ------ Iteration 0
c [XL] Running XL... ring size: 93423
c [XL] Done. Learnt: 2586 T: 10.06
c [XL] learnt 2586 new facts in 10.06 seconds.
c [ANF prop] Running ANF propagation...
c [ANF prop] Left eqs: 205636 T: 0.14
c [iter-simp] ------ Iteration 0
c [ElimLin] Running ElimLin... ring size: 93423
c [GJ] UnSAT
c [ElimLin] learnt 0 new facts in 19.15 seconds.
c [ after 0.2 iteration(s) in 29.58 seconds.]
c Simplifying finished.
c ---- ANF stats -----
c Num total vars: 93423
c Num free vars: 82319
c Num equations: 205636
c Num monoms in eqs: 456224
c Max deg in eqs: 3
c Simple XORs: 0
c Num vars set: 8518
c Num vars replaced: 2586
c --------------------
c [CNF-out] added UNSAT to CNF
c [CNF-gen] Number of value assignments = 8518
c Number of equiv assigments = 2586
c [CNF conversion] in 0.56 seconds.
c ---- CNF stats -----
c Map sizes            : 93423/93423
c Clause Sets          : 216741
c Added as CNF         : 205636
c Added as simple ANF  : 11104
c Added as complex  ANF: 0
c --------------------
s ANF-UNSATISFIABLE
c Learnt 13349 fact(s) in 31.01 seconds using 582.37MB.

d17-55.cnf.gz

The CNF file represents a 17 round SHA-256 with a determined output hash and a partially determined input (9 unknown bits). I don't know for certain that my CNF is sound, but I feel like CryptoMiniSat would have complained if it weren't. Instead, CryptoMiniSat readily solves the problem and finds the solution I expect.

Both programs seem to agree on the number of variables and clauses, which suggests it's not some blatant syntax error. While posting this issue I realised the CNF file has an incorrect clause count in its header (232905 vs the real count of 233217). Even after fixing this the result is the same though. CryptoMiniSat solves the problem and Bosphorus says it's unsatisfiable.

To rule out that I made a mistake while compiling Bosphorus I used the latest Docker image (9dc02c0e39e1) for this test.

cnf simplification problem with double equations

It can't convert ANF to CNF.

Hello, I use bosphorus to convert ANF to CNF.
The command is "./bosphorus --anfread fail_create_cnf.eqs --cnfwrite fail_create_cnf.cnf "
But it kept stopping at the first Iteration 0, I don't know what's wrong.
The attach is my fail ANF file "fail_create_cnf.zip".
Thank you!

fail_create_cnf.zip

what(): Variable index out of bounds. - with 510 variables and clauses

Hi!

Thanks again for making this tool avaiable. I've been having a lot of fun playing around with it. It works great normally, but I've hit a (hopefully interesting) snag.

You mention in the README.md that:

Known issues

    PolyBoRi cannot handle ring of sizes over approx 1 million (1048574). Do not run bosphorus on instances with over a million variables.

I seem to have found an instance where I get a PBoriError at 510 variables, with as many clauses. I have been able to successfully run bosphorus on ANF's with many more variables, so this seems like an issue worth reporting. The full output I'm getting is as follows:

c Bosphorus SHA revision dbf61ae96a7a18bdf7547835ddf955d34ec8f211
c Executed with command line: /usr/local/bin/bosphorus --anfread /dat/polybori_error.txt
c Compilation env CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS =  -Wall -Wextra -Wunused -pedantic -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -mtune=native -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -ggdb3 | COMPILE_DEFINES =  | STATICCOMPILE = ON | ONLY_SIMPLE =  | Boost_FOUND = 1 | STATS =  | SQLITE3_FOUND =  | ZLIB_FOUND = TRUE | VALGRIND_FOUND =  | ENABLE_TESTING =  | M4RI_FOUND = TRUE | SLOW_DEBUG =  | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE =  | PYTHON_LIBRARY =  | PYTHON_INCLUDE_DIRS =  | MY_TARGETS =  | LARGEMEM =  | LIMITMEM =  | compilation date time = Apr 25 2020 12:34:11
c --- Configuration --
c maxTime = 1.00e+20
c XL simp (deg = 1; s = 30.00+4.00): 1
c EL simp (s = 30.00): 1
c SAT simp (10000:100000): 1
 using 1 threads
c Cut num: 5
c Brickenstein cutoff: 10
c --------------------
terminate called after throwing an instance of 'polybori::PBoRiError'
  what():  Variable index out of bounds.

Please find the .anf in the attachment (renamed to .txt, because github does not allow uploads otherwise)
polybori_error.txt

For context, this is an ANF of the first 32-bit Mersenne Twister state transform on the seed bits (x(0)..x(31), with a myriad of help-variables sprinkled in. I'm not 100% sure yet whether it is an actual representation of the mersenne twister, but in any case it should be a valid ANF

I hope you will be able to look at this! If you need any further information, please do let me know.

Best,

Erwin

Bug in `subsitute` function?

Dear Mate,

I think I have uncovered a bug in a critical function that is called during the ElimLin simplification process. The specific line is this:

bosphorus/src/anfutils.cpp

Line 120 in eaed7ea

poly = quotient * to_poly;

If we consider the very simple case where:

from_var = x(1)
poly = x(2)
to_poly = <don't care>

The polynomial quotient will be 0 (and the remainder x(2) )

The line in question will cause the function to return the value of the quotient * to_poly, which will also always be 0. We would instead expect the output to be unchanged (considering x(1) is not present in the poly).

In the case where from_var == poly, the quotient will be 1 and thus should be covered by the next branch in the if-else statement.

In practice, I don't know how often a simplification where the poly is a singleton happens, but I thought it would be good for you to have another look at it, so that consistency of the simplification process can be guaranteed.

Btw: in large polynomials, this function is a significant bottleneck with exponential time-complexity. I am working on a pull request with an algorithm that is more suited to the CUDD back-end that BRiAl uses. I hope you will consider it by the time the request is made!

Best,

Erwin

README -s mistake?

The README lists the following example command:

$ ./bosphorus --anfread test.anf --anfwrite out.anf --cnfwrite out.cnf -s --solvewrite solution

However running this with Bosphorus 3.0 produces:

Some option you gave was wrong. Please give '--help' to get help
Unkown option: unrecognised option '-s'

Running without -s produces no solution file. I think the intended option here is --solve.

cnf to anf conversion makes it unsat

Hi Mate!

I have a cnf file, maybe a little bit big: p cnf 40397 108920
sat.cnf.gz

My problem is that while it is easily solved by cryptominisat, after I convert it into anf, it will be unsatisfiable.

I do the conversion using the docker image:

docker run --rm -v `pwd`/:/dat/ msoos/bosphorus --cnfread /dat/sat.cnf --anfwrite /dat/sat.anf

It's unsat with --xl 0, but sat with --el 0, so I guess the ElimLin causes it somehow. I tried to make the cnf smaller, but then the issue was not reproducible.
Do you have any idea? Am I doing something wrong?

Thanks!

Regards,
Gábor

How to count the number of solutions to an ANF input?

Basically, you can translate your ANF to CNF, and that CNF will have a "c ind X Y Z 0" line. You can now read this CNF with CryptoMiniSat and get all the solutions:

soos@tiresias:build$ cat a.anf
x1 + x2 + x3 + x0
x1 + x2 + 1
soos@tiresias:build$ ./bosphorus --anfread a.anf --cnfwrite a.cnf
c Bosphorus SHA revision 47edb6b2cd98c6fbc3bffcc35dbf2569bc29f58e
c Executed with command line: ./bosphorus --anfread a.anf --cnfwrite a.cnf
[...]
soos@tiresias:build$ cat a.cnf
p cnf 4 4
2 3 0
-2 -3 0
1 4 0
-1 -4 0
c ind 1 2 3 4 0
soos@tiresias:build$ ./cryptominisat5 --maxsol 1000 a.cnf
[...]
c Number of solutions found until now:      4
s UNSATISFIABLE

So this means, the original ANF had 4 solutions. If the original ANF has many solutions, you can use ApproxMC to count the number of solutions:

soos@tiresias:build$ ./approxmc a.cnf
[...]
c [appmc] Number of solutions is: 4*2**0
s mc 4

Note that ApproxMC is much more suitable if you have many more solutions.

first experience

Hi Mate,
here is my first experience with bosphorus.
I use the Debian distribution (testing/unstable but actually mainly unstable which has. e.g. gcc 8.2).
First, I compiled BRiAl by myself. That needed also the package libboost-test-dev.
But finally, I used the Debian package libbrial-dev.
Since I do experiments with several versions of CryptoMiniSat, I don't do the make install step there but run cryptominisat5 from the build directory. Therefore, I added the line

include_directories( ${cryptominisat5_DIR}/cmsat5-src )

to the file CMakeLists.txt right behind the block

find_package(cryptominisat5 REQUIRED)
if (cryptominisat4_FOUND)
    message(STATUS "OK, CryptoMiniSat5 found")
endif()

to make cmake find the CMS header files and called cmake with something like this

cmake -Dcryptominisat5_DIR=/home/opt/cryptominisat.git-ff39e02a ..

The build succeded. Your test example also works. I just added the switch -e <path-to-cryptominisat5-version>.
I also tried a small example of mine and learned that bosphorus just accepts variables with x and a number.

I will do further tests for sure. At the moment I'm trying to make the newer SageMath working with CMS since I use it for the generation of some ANF (or I have to recompile version 7.6).

Regards,
Jörg.

Missing end-to-end tests

There are no end-to-end tests for ANF parsing, CNF writing, etc. So there may be some bugs in some of these parsers and CNF/ANF writers, and we may introduce new ones, but we will not be alerted to them.

multiple SATs

Hi Developers.
I'm writing in the hope you may add to bosphorus some option to save all computed SATs in ANF form.
It would be useful if the SATs are written in the output file as they are computed and with total computing time till such SAT is appeared. Note that cryptominisat5 provides multiple SATs with option --maxsol.
Many thanks in advance,
Bob

Counting the number of solutions after ANF->CNF conversion

Hi,

I'd like to use the Bosphorus as a CNF to ANF converter in my new tool. However, I want to become sure whether the CNF reader works correctly. The following example taken from the previous closed issues represents that the CNF reader doesn't work properly. It should be noted that I reproduced the following results via the new version and noticed that there is still the same issue in the new version.

The attached file, contains the CNF of Skinny-128 Sbox in 'dimacs' format. The number of solutions for the given CNF must be 256, since it actually describe an 8-bit Sbox, and it is known that the number of possible (input, output) pairs, for a given 8-bit bijective Sbox must be 256. The CNF file has been attached, however you can reproduce it via the following command in SageMath:

from sage.crypto.sbox import SBox
s = SBox([0x65 , 0x4c , 0x6a , 0x42 , 0x4b , 0x63 , 0x43 , 0x6b , 0x55 , 0x75 , 0x5a , 0x7a , 0x53 , 0x73 , 0x5b , 0x7b ,0x35 , 0x8c , 0x3a , 0x81 , 0x89 , 0x33 , 0x80 , 0x3b , 0x95 , 0x25 , 0x98 , 0x2a , 0x90 , 0x23 , 0x99 , 0x2b ,0xe5 , 0xcc , 0xe8 , 0xc1 , 0xc9 , 0xe0 , 0xc0 , 0xe9 , 0xd5 , 0xf5 , 0xd8 , 0xf8 , 0xd0 , 0xf0 , 0xd9 , 0xf9 ,0xa5 , 0x1c , 0xa8 , 0x12 , 0x1b , 0xa0 , 0x13 , 0xa9 , 0x05 , 0xb5 , 0x0a , 0xb8 , 0x03 , 0xb0 , 0x0b , 0xb9 ,0x32 , 0x88 , 0x3c , 0x85 , 0x8d , 0x34 , 0x84 , 0x3d , 0x91 , 0x22 , 0x9c , 0x2c , 0x94 , 0x24 , 0x9d , 0x2d ,0x62 , 0x4a , 0x6c , 0x45 , 0x4d , 0x64 , 0x44 , 0x6d , 0x52 , 0x72 , 0x5c , 0x7c , 0x54 , 0x74 , 0x5d , 0x7d ,0xa1 , 0x1a , 0xac , 0x15 , 0x1d , 0xa4 , 0x14 , 0xad , 0x02 , 0xb1 , 0x0c , 0xbc , 0x04 , 0xb4 , 0x0d , 0xbd ,0xe1 , 0xc8 , 0xec , 0xc5 , 0xcd , 0xe4 , 0xc4 , 0xed , 0xd1 , 0xf1 , 0xdc , 0xfc , 0xd4 , 0xf4 , 0xdd , 0xfd ,0x36 , 0x8e , 0x38 , 0x82 , 0x8b , 0x30 , 0x83 , 0x39 , 0x96 , 0x26 , 0x9a , 0x28 , 0x93 , 0x20 , 0x9b , 0x29 ,0x66 , 0x4e , 0x68 , 0x41 , 0x49 , 0x60 , 0x40 , 0x69 , 0x56 , 0x76 , 0x58 , 0x78 , 0x50 , 0x70 , 0x59 , 0x79 ,0xa6 , 0x1e , 0xaa , 0x11 , 0x19 , 0xa3 , 0x10 , 0xab , 0x06 , 0xb6 , 0x08 , 0xba , 0x00 , 0xb3 , 0x09 , 0xbb ,0xe6 , 0xce , 0xea , 0xc2 , 0xcb , 0xe3 , 0xc3 , 0xeb , 0xd6 , 0xf6 , 0xda , 0xfa , 0xd3 , 0xf3 , 0xdb , 0xfb ,0x31 , 0x8a , 0x3e , 0x86 , 0x8f , 0x37 , 0x87 , 0x3f , 0x92 , 0x21 , 0x9e , 0x2e , 0x97 , 0x27 , 0x9f , 0x2f ,0x61 , 0x48 , 0x6e , 0x46 , 0x4f , 0x67 , 0x47 , 0x6f , 0x51 , 0x71 , 0x5e , 0x7e , 0x57 , 0x77 , 0x5f , 0x7f ,0xa2 , 0x18 , 0xae , 0x16 , 0x1f , 0xa7 , 0x17 , 0xaf , 0x01 , 0xb2 , 0x0e , 0xbe , 0x07 , 0xb7 , 0x0f , 0xbf ,0xe2 , 0xca , 0xee , 0xc6 , 0xcf , 0xe7 , 0xc7 , 0xef , 0xd2 , 0xf2 , 0xde , 0xfe , 0xd7 , 0xf7 , 0xdf , 0xff])
print(s.cnf(format = 'dimacs'))

CNF file: skinny64_sbox.zip
I solved the above SAT problem via your nice tool, called CryptoMiniSat5 with the following command:

cryptominisat5 --verb 0 --maxsol 500 skinny64_sbox.cnf > solutions.txt

As you can see in solutions.zip, there are only 256 different solutions for this SAT problem. Let's simplify this CNF with the Bosphorus, to see whether it keeps the number of solutions unchanged or not.
I simplified it via the following command:

./bosphorus --cnfread skinny64_sbox.cnf --cnfwrite simplified.cnf

The simplified version of the above SAT problem, has been included in the simplified.zip. When I solved the simplified.cnf with the CryptoMiniSat5, I observed that it has more than 256 solutions. I solved it via the following command:

cryptominisat5 --verb 0 --maxsol 500 simplified.cnf > solutions1.txt

As you can see in solutions1.txt file, there are more than 256 different solutions for the simplified CNF! So, I think the Bosphorus doesn't prereserve the equality. Let me know if I am wrong please.

Kind regards,
Hosein

Originally posted by @hadipourh in #11 (comment)

Tests gone missing

There might be something not immediately apparent but I couldn't find any lit tests in the repository.

Trying to run the test suite as per the README,

$ pip install lit OutputCheck
$ lit bosphorus/tests
lit: /home/alexander/venv/bosphorus/lib/python3.9/site-packages/lit/discovery.py:133: warning: unable to find test suite for 'bosphorus/tests'
lit: /home/alexander/venv/bosphorus/lib/python3.9/site-packages/lit/discovery.py:267: warning: input 'bosphorus/tests' contained no tests
error: did not discover any tests for provided path(s)

What am I overlooking?

If the Bosporus has executable file in Windows system?

Dear msoos
The Bosporus helped me a lot.(I only use it to convert ANF to CNF, and solve the CNF is faster than ANF2CNF)
But I mainly use Windows system, this main:

get ANF in Windows system;
send ANF to Linux system and convert to CNF;
send CNF to Windows or Linux systems.
It's a bit of a hassle.
So I wang to know if the Bosporus has executable file in Windows system?
Such as bosporus.exe...
Or it only can run in the Linux system?

Looking forward to your reply!
Thank you.

The executable file about the newest bosphorus

Dear author.
I don't know if it's my problem.
I noticed that: the same ANF file use different version bosphorus,
will get the different CNF file(including file size and SAT solving speed).
For example the executable file: https://github.com/meelgroup/bosphorus/releases/download/bosphorus-3.0/bosphorus-linux64.gz
and some version I compiled myself earlier(about 2022.9) get different CNF file.
But unfortunately, I lost the history compiled bosphorus file, and now I can't compile successfully.
So could you please give me a copy of the newest executable file(like bosphorus-linux64 can run directly, no other dependencies).
Because I noticed that my compiled result still need shared libraries: libbosphorus.so.3.0.

Looking forward to your reply!
Best wishes to you!
--zfx

CNF reading does not care about independent set and will lose/create solutions.

Likely this will never be fixed, but I am putting this here anyway.

ANF independent set is not translated to CNF indep set

As title says. The CNF indep set does not reflect the ANF indep set.

CNF with XOR extension

Some ANF systems with long XOR equations really blow up when converted to CNF and use massive amounts of RAM plus introduce additional temporary variables and clauses which slow down the SAT solver.

Since Bosphorus uses Crytpominisat for the SAT stage, shouldn't it use XOR clauses, at least internally?

I don't know exactly what CMS does with the XOR clauses. Maybe it cuts them internally to fit into its CNF based solving strategies. But even if it does cut internally, at least it doesn't need to spend time in the XOR recovery stage mentioned in the blog post.

Paper link and bib link broken

I did manage to find the paper here:

https://past.date-conference.com/proceedings-archive/2019/pdf/0149.pdf

And here is the bibtex:

@INPROCEEDINGS{8715061,
  author={Choo, Davin and Soos, Mate and Chai, Kian Ming A. and Meel, Kuldeep S.},
  booktitle={2019 Design, Automation & Test in Europe Conference & Exhibition (DATE)}, 
  title={Bosphorus: Bridging ANF and CNF Solvers}, 
  year={2019},
  volume={},
  number={},
  pages={468-473},
  keywords={Benchmark testing;Memory management;Data structures;Boolean algebra;Bridge circuits;Tools;Encoding},
  doi={10.23919/DATE.2019.8715061}}```

Number of variables

I have a system of equations with 100 variables out of which I have fixed 25 variables and simplified the system of equations.
Bosphorus still shows 100 variables instead of 75, as it looks at the indexes rather than counting the number of actual variables.
Should I write a program to rename my whole system to a lower number of variables from x1 to x75 or does bosphorus handles it internally?
I was wondering that it might be creating the missing variables by itself and taking more time to solve.

CryptoMiniSat embedded in SageMath can solve these ANFs but Bosphous reports UNSAT

operating system: Linux ubuntu18.04

We use Sage to generate ANF(round4rxoodooMess.anf), and invoke the function solve_sat() to solve this SAT problem, and the solver return solution.

nohup: ignoring input
x(718)
x(423)*x(467) + x(423)*x(476) + x(423)*x(594) + x(423)*x(603) + x(423)*x(651) + x(423)*x(660) + x(423)*x(697) + x(423)*x(851) + x(423)*x(860) + x(423)*x(978) + x(423)*x(987) + x(423)*x(1035) + x(423)*x(1044) + x(423)*x(1081) + x(446)*x(467) + x(446)*x(476) + x(446)*x(594) + x(446)*x(603) + x(446)*x(651) + x(446)*x(660) + x(446)*x(697) + x(446)*x(851) + x(446)*x(860) + x(446)*x(978) + x(446)*x(987) + x(446)*x(1035) + x(446)*x(1044) + x(446)*x(1081) + x(455) + x(467)*x(550) + x(467)*x(573) + x(467)*x(587) + x(467)*x(758) + x(467)*x(767) + x(467)*x(807) + x(467)*x(830) + x(467)*x(934) + x(467)*x(957) + x(467)*x(971) + x(467)*x(1142) + x(467)*x(1151) + x(467) + x(476)*x(550) + x(476)*x(573) + x(476)*x(587) + x(476)*x(758) + x(476)*x(767) + x(476)*x(807) + x(476)*x(830) + x(476)*x(934) + x(476)*x(957) + x(476)*x(971) + x(476)*x(1142) + x(476)*x(1151) + x(476) + x(478) + x(492) + x(550)*x(594) + x(550)*x(603) + x(550)*x(651) + x(550)*x(660) + x(550)*x(697) + x(550)*x(851) + x(550)*x(860) + x(550)*x(978) + x(550)*x(987) + x(550)*x(1035) + x(550)*x(1044) + x(550)*x(1081) + x(573)*x(594) + x(573)*x(603) + x(573)*x(651) + x(573)*x(660) + x(573)*x(697) + x(573)*x(851) + x(573)*x(860) + x(573)*x(978) + x(573)*x(987) + x(573)*x(1035) + x(573)*x(1044) + x(573)*x(1081) + x(582) + x(587)*x(594) + x(587)*x(603) + x(587)*x(651) + x(587)*x(660) + x(587)*x(697) + x(587)*x(851) + x(587)*x(860) + x(587)*x(978) + x(587)*x(987) + x(587)*x(1035) + x(587)*x(1044) + x(587)*x(1081) + x(594)*x(758) + x(594)*x(767) + x(594)*x(807) + x(594)*x(830) + x(594)*x(934) + x(594)*x(957) + x(594)*x(971) + x(594)*x(1142) + x(594)*x(1151) + x(594) + x(603)*x(758) + x(603)*x(767) + x(603)*x(807) + x(603)*x(830) + x(603)*x(934) + x(603)*x(957) + x(603)*x(971) + x(603)*x(1142) + x(603)*x(1151) + x(603) + x(605) + x(651)*x(758) + x(651)*x(767) + x(651)*x(807) + x(651)*x(830) + x(651)*x(934) + x(651)*x(957) + x(651)*x(971) + x(651)*x(1142) + x(651)*x(1151) + x(651) + x(660)*x(758) + x(660)*x(767) + x(660)*x(807) + x(660)*x(830) + x(660)*x(934) + x(660)*x(957) + x(660)*x(971) + x(660)*x(1142) + x(660)*x(1151) + x(660) + x(662) + x(671) + x(697)*x(758) + x(697)*x(767) + x(697)*x(807) + x(697)*x(830) + x(697)*x(934) + x(697)*x(957) + x(697)*x(971) + x(697)*x(1142) + x(697)*x(1151) + x(697) + x(758)*x(851) + x(758)*x(860) + x(758)*x(978) + x(758)*x(987) + x(758)*x(1035) + x(758)*x(1044) + x(758)*x(1081) + x(767)*x(851) + x(767)*x(860) + x(767)*x(978) + x(767)*x(987) + x(767)*x(1035) + x(767)*x(1044) + x(767)*x(1081) + x(1260)
x(38) + x(61) + x(75) + x(165) + x(188) + x(373) + x(382)
...
...
x(810) + x(819) + x(840)*x(842) + x(840)*x(851) + x(840)*x(888) + x(840)*x(969) + x(840)*x(978) + x(840)*x(1026) + x(840)*x(1035) + x(842)*x(863) + x(842)*x(967) + x(842)*x(990) + x(842)*x(1024) + x(842)*x(1047) + x(842)*x(1061) + x(842) + x(851)*x(863) + x(851)*x(967) + x(851)*x(990) + x(851)*x(1024) + x(851)*x(1047) + x(851)*x(1061) + x(851) + x(863)*x(888) + x(863)*x(969) + x(863)*x(978) + x(863)*x(1026) + x(863)*x(1035) + x(888)*x(967) + x(888)*x(990) + x(888)*x(1024) + x(888)*x(1047) + x(888)*x(1061) + x(888) + x(937) + x(946) + x(967)*x(969) + x(967)*x(978) + x(967)*x(1026) + x(967)*x(1035) + x(969)*x(990) + x(969)*x(1024) + x(969)*x(1047) + x(969)*x(1061) + x(969) + x(978)*x(990) + x(978)*x(1024) + x(978)*x(1047) + x(978)*x(1061) + x(978) + x(983) + x(990)*x(1026) + x(990)*x(1035) + x(1024)*x(1026) + x(1024)*x(1035) + x(1026)*x(1047) + x(1026)*x(1061) + x(1026) + x(1035)*x(1047) + x(1035)*x(1061) + x(1035) + x(1122) + x(1131) + x(1784)
x(23) + x(73)*x(103) + x(73)*x(126) + x(73)*x(230) + x(73)*x(253) + x(73)*x(310) + x(73)*x(319) + x(73)*x(324) + x(82)*x(103) + x(82)*x(126) + x(82)*x(230) + x(82)*x(253) + x(82)*x(310) + x(82)*x(319) + x(82)*x(324) + x(103)*x(200) + x(103)*x(209) + x(103)*x(246) + x(103)*x(257) + x(103)*x(266) + x(103) + x(105) + x(114) + x(126)*x(200) + x(126)*x(209) + x(126)*x(246) + x(126)*x(257) + x(126)*x(266) + x(126) + x(200)*x(230) + x(200)*x(253) + x(200)*x(310) + x(200)*x(319) + x(200)*x(324) + x(209)*x(230) + x(209)*x(253) + x(209)*x(310) + x(209)*x(319) + x(209)*x(324) + x(230)*x(246) + x(230)*x(257) + x(230)*x(266) + x(230) + x(232) + x(241) + x(246)*x(253) + x(246)*x(310) + x(246)*x(319) + x(246)*x(324) + x(253)*x(257) + x(253)*x(266) + x(253) + x(257)*x(310) + x(257)*x(319) + x(257)*x(324) + x(266)*x(310) + x(266)*x(319) + x(266)*x(324) + x(289) + x(298) + x(310) + x(319) + x(324) + x(791)
2022-06-20 16:18:47,120 - simple_example - INFO - start solve
2022-06-20 16:20:34,019 - simple_example - INFO - [{x(1919): 0, x(1918): 0, x(1917): 0, x(1916): 0, x(1915): 1, x(1914): 1, x(1913): 1, x(1912): 0, x(1911): 0, x(1910): 1, x(1909): 0, x(1908): 0, x(1907): 0, x(1906): 0, x(1905): 0, x(1904): 0, x(1903): 1, x(1902): 0, x(1901): 0, x(1900): 1, x(1899): 0, x(1898): 0, x(1897): 0, x(1896): 1, x(1895): 1, x(1894): 1, x(1893): 1, x(1892): 1, x(1891): 1, x(1890): 0, x(1889): 0, x(1888): 1, x(1887): 0, x(1886): 0, x(1885): 0, x(1884): 1, x(1883): 1, x(1882): 0, x(1881): 1, x(1880): 0, x(1879): 1, x(1878): 0, x(1877): 0, x(1876): 1, x(1875): 0, x(1874): 1, x(1873): 1, x(1872): 1, x(1871): 0, x(1870): 1, x(1869): 1, x(1868): 0, x(1867): 1, x(1866): 1, x(1865): 1, x(1864): 1, x(1863): 1, x(1862): 1, x(1861): 0, x(1860): 0, x(1859): 0, x(1858): 1, x(1857): 1, x(1856): 0, x(1855): 0, x(1854): 1, x(1853): 0, x(1852): 0, x(1851): 0, x(1850): 0, x(1849): 0, x(1848): 0, x(1847): 0, x(1846): 0, x(1845): 0, x(1844): 0, x(1843): 1, x(1842): 1, x(1841): 1, x(1840): 0, x(1839): 0, x(1838): 1, x(1837): 1, x(1836): 1, x(1835): 0, x(1834): 0, x(1833): 0, x(1832): 1, x(1831): 1, x(1830): 1, x(1829): 1, x(1828): 1, x(1827): 1, x(1826): 1, x(1825): 1, x(1824): 1, x(1823): 1, x(1822): 1, x(1821): 0, x(1820): 0, x(1819): 1, x(1818): 0, x(1817): 1, x(1816): 1, x(1815): 0, x(1814): 1, x(1813): 1, x(1812): 1, x(1811): 0, x(1810): 1, x(1809): 0, x(1808): 0, x(1807): 1, x(1806): 0, x(1805): 1, x(1804): 0, x(1803): 0, x(1802): 0, x(1801): 0, x(1800): 1, x(1799): 1, x(1798): 1, x(1797): 0, x(1796): 0, x(1795): 1, x(1794): 0, x(1793): 0, x(1792): 1, x(1791): 0, x(1790): 1, x(1789): 0, x(1788): 1, x(1787): 0, x(1786): 0, x(1785): 0, x(1784): 1, x(1783): 0, x(1782): 1, x(1781): 0, x(1780): 1, x(1779): 0, x(1778): 1, x(1777): 0, x(1776): 1, x(1775): 0, x(1774): 1, x(1773): 1, x(1772): 0, x(1771): 1, x(1770): 1, x(1769): 1, x(1768): 0, x(1767): 0, x(1766): 1, x(1765): 0, x(1764): 1, x(1763): 0, x(1762): 1, x(1761): 0, x(1760): 1, x(1759): 0, x(1758): 1, x(1757): 0, x(1756): 1, x(1755): 1, x(1754): 0, x(1753): 1, x(1752): 1, x(1751): 0, x(1750): 0, x(1749): 1, x(1748): 0, x(1747): 0, x(1746): 1, x(1745): 0, x(1744): 1, x(1743): 1, x(1742): 1, x(1741): 1, x(1740): 0, x(1739): 1, x(1738): 0, x(1737): 1, x(1736): 1, x(1735): 1, x(1734): 0, x(1733): 0, x(1732): 1, x(1731): 1, x(1730): 0, x(1729): 0, x(1728): 1, x(1727): 0, x(1726): 1, x(1725): 0, x(1724): 0, x(1723): 0, x(1722): 1, x(1721): 1, x(1720): 1, x(1719): 1, x(1718): 1, x(1717): 0, x(1716): 1, x(1715): 0, x(1714): 0, x(1713): 0, x(1712): 1, x(1711): 1, x(1710): 1, x(1709): 0, x(1708): 1, x(1707): 0, x(1706): 0, x(1705): 0, x(1704): 0, x(1703): 1, x(1702): 0, x(1701): 1, x(1700): 0, x(1699): 1, x(1698): 0, x(1697): 1, x(1696): 1, x(1695): 1, x(1694): 0, x(1693): 0, x(1692): 0, x(1691): 0, x(1690): 0, x(1689): 1, x(1688): 1, x(1687): 1, x(1686): 1, x(1685): 1, x(1684): 0, x(1683): 0, x(1682): 0, x(1681): 1, x(1680): 0, x(1679): 0, x(1678): 0, x(1677): 1, x(1676): 1, x(1675): 0, x(1674): 0, x(1673): 0, x(1672): 1, x(1671): 0, x(1670): 0, x(1669): 1, x(1668): 1, x(1667): 0, x(1666): 1, x(1665): 1, x(1664): 0, x(1663): 1, x(1662): 1, x(1661): 0, x(1660): 1, x(1659): 1, x(1658): 1, x(1657): 0, x(1656): 1, x(1655): 1, x(1654): 0, x(1653): 1, x(1652): 1, x(1651): 0, x(1650): 1, x(1649): 0, x(1648): 0, x(1647): 0, x(1646): 1, x(1645): 0, x(1644): 0, x(1643): 0, x(1642): 1, x(1641): 1, x(1640): 0, x(1639): 1, x(1638): 0, x(1637): 0, x(1636): 0, x(1635): 0, x(1634): 0, x(1633): 1, x(1632): 1, x(1631): 1, x(1630): 0, x(1629): 1, x(1628): 0, x(1627): 0, x(1626): 0, x(1625): 0, x(1624): 0, x(1623): 1, x(1622): 0, x(1621): 0, x(1620): 1, x(1619): 1, x(1618): 1, x(1617): 0, x(1616): 1, x(1615): 0, x(1614): 0, x(1613): 0, x(1612): 1, x(1611): 1, x(1610): 1, x(1609): 1, x(1608): 1, x(1607): 0, x(1606): 1, x(1605): 0, x(1604): 1, x(1603): 1, x(1602): 1, x(1601): 0, x(1600): 0, x(1599): 1, x(1598): 0, x(1597): 1, x(1596): 0, x(1595): 0, x(1594): 1, x(1593): 1, x(1592): 0, x(1591): 0, x(1590): 0, x(1589): 1, x(1588): 0, x(1587): 1, x(1586): 1, x(1585): 0, x(1584): 0, x(1583): 0, x(1582): 0, x(1581): 0, x(1580): 1, x(1579): 1, x(1578): 0, x(1577): 0, x(1576): 1, x(1575): 0, x(1574): 0, x(1573): 1, x(1572): 0, x(1571): 0, x(1570): 1, x(1569): 0, x(1568): 0, x(1567): 0, x(1566): 1, x(1565): 1, x(1564): 1, x(1563): 1, x(1562): 0, x(1561): 0, x(1560): 1, x(1559): 0, x(1558): 1, x(1557): 0, x(1556): 1, x(1555): 0, x(1554): 0, x(1553): 1, x(1552): 0, x(1551): 1, x(1550): 0, x(1549): 0, x(1548): 1, x(1547): 0, x(1546): 0, x(1545): 0, x(1544): 1, x(1543): 0, x(1542): 1, x(1541): 0, x(1540): 0, x(1539): 0, x(1538): 0, x(1537): 1, x(1536): 0, x(1535): 0, x(1534): 0, x(1533): 0, x(1532): 0, x(1531): 0, x(1530): 0, x(1529): 0, x(1528): 0, x(1527): 0, x(1526): 0, x(1525): 0, x(1524): 0, x(1523): 0, x(1522): 0, x(1521): 0, x(1520): 0, x(1519): 0, x(1518): 0, x(1517): 0, x(1516): 0, x(1515): 0, x(1514): 0, x(1513): 0, x(1512): 0, x(1511): 0, x(1510): 0, x(1509): 0, x(1508): 0, x(1507): 0, x(1506): 0, x(1505): 0, x(1504): 0, x(1503): 0, x(1502): 0, x(1501): 0, x(1500): 0, x(1499): 0, x(1498): 0, x(1497): 0, x(1496): 0, x(1495): 0, x(1494): 1, x(1493): 0, x(1492): 0, x(1491): 0, x(1490): 0, x(1489): 0, x(1488): 1, x(1487): 0, x(1486): 0, x(1485): 0, x(1484): 0, x(1483): 0, x(1482): 0, x(1481): 0, x(1480): 0, x(1479): 0, x(1478): 1, x(1477): 0, x(1476): 0, x(1475): 0, x(1474): 0, x(1473): 0, x(1472): 1, x(1471): 0, x(1470): 0, x(1469): 0, x(1468): 0, x(1467): 0, x(1466): 0, x(1465): 0, x(1464): 0, x(1463): 0, x(1462): 0, x(1461): 0, x(1460): 0, x(1459): 0, x(1458): 0, x(1457): 0, x(1456): 0, x(1455): 0, x(1454): 0, x(1453): 0, x(1452): 0, x(1451): 0, x(1450): 0, x(1449): 0, x(1448): 0, x(1447): 0, x(1446): 0, x(1445): 0, x(1444): 0, x(1443): 0, x(1442): 0, x(1441): 0, x(1440): 0, x(1439): 0, x(1438): 1, x(1437): 0, x(1436): 0, x(1435): 0, x(1434): 0, x(1433): 0, x(1432): 1, x(1431): 0, x(1430): 0, x(1429): 0, x(1428): 0, x(1427): 1, x(1426): 0, x(1425): 0, x(1424): 0, x(1423): 0, x(1422): 1, x(1421): 0, x(1420): 0, x(1419): 0, x(1418): 0, x(1417): 0, x(1416): 1, x(1415): 0, x(1414): 0, x(1413): 0, x(1412): 0, x(1411): 1, x(1410): 0, x(1409): 0, x(1408): 0, x(1407): 0, x(1406): 0, x(1405): 0, x(1404): 0, x(1403): 0, x(1402): 0, x(1401): 0, x(1400): 0, x(1399): 0, x(1398): 0, x(1397): 0, x(1396): 0, x(1395): 0, x(1394): 0, x(1393): 0, x(1392): 0, x(1391): 0, x(1390): 0, x(1389): 0, x(1388): 0, x(1387): 0, x(1386): 0, x(1385): 0, x(1384): 0, x(1383): 0, x(1382): 0, x(1381): 0, x(1380): 0, x(1379): 0, x(1378): 0, x(1377): 0, x(1376): 0, x(1375): 0, x(1374): 0, x(1373): 0, x(1372): 0, x(1371): 0, x(1370): 0, x(1369): 0, x(1368): 0, x(1367): 0, x(1366): 0, x(1365): 0, x(1364): 0, x(1363): 0, x(1362): 0, x(1361): 0, x(1360): 0, x(1359): 0, x(1358): 0, x(1357): 0, x(1356): 0, x(1355): 0, x(1354): 0, x(1353): 0, x(1352): 0, x(1351): 0, x(1350): 0, x(1349): 0, x(1348): 0, x(1347): 0, x(1346): 0, x(1345): 0, x(1344): 0, x(1343): 0, x(1342): 0, x(1341): 0, x(1340): 0, x(1339): 0, x(1338): 0, x(1337): 0, x(1336): 0, x(1335): 0, x(1334): 0, x(1333): 0, x(1332): 0, x(1331): 0, x(1330): 0, x(1329): 0, x(1328): 0, x(1327): 0, x(1326): 0, x(1325): 0, x(1324): 0, x(1323): 0, x(1322): 0, x(1321): 0, x(1320): 0, x(1319): 0, x(1318): 0, x(1317): 0, x(1316): 0, x(1315): 0, x(1314): 0, x(1313): 0, x(1312): 0, x(1311): 0, x(1310): 0, x(1309): 0, x(1308): 0, x(1307): 0, x(1306): 0, x(1305): 0, x(1304): 0, x(1303): 0, x(1302): 0, x(1301): 0, x(1300): 0, x(1299): 0, x(1298): 0, x(1297): 0, x(1296): 0, x(1295): 0, x(1294): 0, x(1293): 0, x(1292): 0, x(1291): 0, x(1290): 0, x(1289): 0, x(1288): 0, x(1287): 0, x(1286): 0, x(1285): 0, x(1284): 0, x(1283): 0, x(1282): 0, x(1281): 0, x(1280): 0, x(1279): 0, x(1278): 0, x(1277): 0, x(1276): 0, x(1275): 0, x(1274): 0, x(1273): 0, x(1272): 0, x(1271): 0, x(1270): 0, x(1269): 0, x(1268): 0, x(1267): 0, x(1266): 0, x(1265): 0, x(1264): 0, x(1263): 0, x(1262): 0, x(1261): 0, x(1260): 0, x(1259): 0, x(1258): 0, x(1257): 0, x(1256): 0, x(1255): 0, x(1254): 0, x(1253): 0, x(1252): 0, x(1251): 0, x(1250): 0, x(1249): 0, x(1248): 0, x(1247): 0, x(1246): 0, x(1245): 0, x(1244): 0, x(1243): 1, x(1242): 0, x(1241): 0, x(1240): 0, x(1239): 0, x(1238): 1, x(1237): 0, x(1236): 0, x(1235): 0, x(1234): 0, x(1233): 0, x(1232): 1, x(1231): 0, x(1230): 0, x(1229): 0, x(1228): 0, x(1227): 1, x(1226): 0, x(1225): 0, x(1224): 0, x(1223): 0, x(1222): 1, x(1221): 0, x(1220): 0, x(1219): 0, x(1218): 0, x(1217): 0, x(1216): 1, x(1215): 0, x(1214): 0, x(1213): 0, x(1212): 0, x(1211): 0, x(1210): 0, x(1209): 0, x(1208): 0, x(1207): 0, x(1206): 0, x(1205): 0, x(1204): 0, x(1203): 0, x(1202): 0, x(1201): 0, x(1200): 0, x(1199): 0, x(1198): 0, x(1197): 0, x(1196): 0, x(1195): 0, x(1194): 0, x(1193): 0, x(1192): 0, x(1191): 0, x(1190): 0, x(1189): 0, x(1188): 0, x(1187): 0, x(1186): 0, x(1185): 0, x(1184): 0, x(1183): 0, x(1182): 1, x(1181): 0, x(1180): 0, x(1179): 0, x(1178): 0, x(1177): 0, x(1176): 1, x(1175): 0, x(1174): 0, x(1173): 0, x(1172): 0, x(1171): 0, x(1170): 0, x(1169): 0, x(1168): 0, x(1167): 0, x(1166): 1, x(1165): 0, x(1164): 0, x(1163): 0, x(1162): 0, x(1161): 0, x(1160): 1, x(1159): 0, x(1158): 0, x(1157): 0, x(1156): 0, x(1155): 0, x(1154): 0, x(1153): 0, x(1152): 0, x(1151): 1, x(1150): 0, x(1149): 1, x(1148): 0, x(1147): 1, x(1146): 1, x(1145): 1, x(1144): 1, x(1143): 0, x(1142): 1, x(1141): 0, x(1140): 1, x(1139): 1, x(1138): 1, x(1137): 0, x(1136): 1, x(1135): 0, x(1134): 0, x(1133): 1, x(1132): 0, x(1131): 1, x(1130): 0, x(1129): 0, x(1128): 1, x(1127): 0, x(1126): 1, x(1125): 0, x(1124): 0, x(1123): 0, x(1122): 0, x(1121): 1, x(1120): 0, x(1119): 1, x(1118): 0, x(1117): 1, x(1116): 1, x(1115): 0, x(1114): 0, x(1113): 1, x(1112): 0, x(1111): 1, x(1110): 0, x(1109): 0, x(1108): 1, x(1107): 1, x(1106): 1, x(1105): 0, x(1104): 0, x(1103): 1, x(1102): 1, x(1101): 1, x(1100): 1, x(1099): 0, x(1098): 1, x(1097): 0, x(1096): 0, x(1095): 0, x(1094): 0, x(1093): 1, x(1092): 0, x(1091): 0, x(1090): 1, x(1089): 0, x(1088): 1, x(1087): 1, x(1086): 0, x(1085): 1, x(1084): 1, x(1083): 1, x(1082): 0, x(1081): 1, x(1080): 0, x(1079): 1, x(1078): 1, x(1077): 0, x(1076): 0, x(1075): 1, x(1074): 1, x(1073): 1, x(1072): 0, x(1071): 0, x(1070): 0, x(1069): 0, x(1068): 0, x(1067): 1, x(1066): 0, x(1065): 0, x(1064): 1, x(1063): 0, x(1062): 1, x(1061): 0, x(1060): 1, x(1059): 0, x(1058): 1, x(1057): 0, x(1056): 1, x(1055): 0, x(1054): 0, x(1053): 1, x(1052): 1, x(1051): 1, x(1050): 0, x(1049): 0, x(1048): 0, x(1047): 0, x(1046): 1, x(1045): 0, x(1044): 0, x(1043): 1, x(1042): 1, x(1041): 0, x(1040): 0, x(1039): 0, x(1038): 1, x(1037): 1, x(1036): 0, x(1035): 1, x(1034): 1, x(1033): 1, x(1032): 1, x(1031): 1, x(1030): 0, x(1029): 0, x(1028): 1, x(1027): 1, x(1026): 1, x(1025): 0, x(1024): 1, x(1023): 1, x(1022): 0, x(1021): 1, x(1020): 0, x(1019): 0, x(1018): 1, x(1017): 0, x(1016): 0, x(1015): 0, x(1014): 0, x(1013): 1, x(1012): 0, x(1011): 0, x(1010): 1, x(1009): 0, x(1008): 0, x(1007): 0, x(1006): 1, x(1005): 0, x(1004): 1, x(1003): 1, x(1002): 0, x(1001): 1, x(1000): 0, x(999): 0, x(998): 1, x(997): 0, x(996): 1, x(995): 1, x(994): 1, x(993): 0, x(992): 0, x(991): 0, x(990): 0, x(989): 0, x(988): 1, x(987): 0, x(986): 0, x(985): 1, x(984): 0, x(983): 0, x(982): 0, x(981): 1, x(980): 1, x(979): 0, x(978): 0, x(977): 1, x(976): 1, x(975): 0, x(974): 1, x(973): 0, x(972): 0, x(971): 0, x(970): 0, x(969): 0, x(968): 1, x(967): 1, x(966): 1, x(965): 0, x(964): 0, x(963): 1, x(962): 1, x(961): 1, x(960): 1, x(959): 0, x(958): 1, x(957): 0, x(956): 0, x(955): 0, x(954): 1, x(953): 0, x(952): 0, x(951): 0, x(950): 1, x(949): 0, x(948): 0, x(947): 0, x(946): 0, x(945): 1, x(944): 0, x(943): 0, x(942): 1, x(941): 0, x(940): 0, x(939): 0, x(938): 0, x(937): 0, x(936): 1, x(935): 0, x(934): 1, x(933): 1, x(932): 0, x(931): 1, x(930): 1, x(929): 0, x(928): 0, x(927): 1, x(926): 0, x(925): 1, x(924): 0, x(923): 0, x(922): 0, x(921): 0, x(920): 1, x(919): 0, x(918): 1, x(917): 0, x(916): 1, x(915): 0, x(914): 1, x(913): 1, x(912): 0, x(911): 0, x(910): 1, x(909): 1, x(908): 0, x(907): 0, x(906): 0, x(905): 1, x(904): 1, x(903): 1, x(902): 1, x(901): 0, x(900): 0, x(899): 0, x(898): 1, x(897): 0, x(896): 0, x(895): 0, x(894): 0, x(893): 1, x(892): 0, x(891): 1, x(890): 0, x(889): 0, x(888): 0, x(887): 0, x(886): 0, x(885): 0, x(884): 1, x(883): 1, x(882): 1, x(881): 0, x(880): 0, x(879): 0, x(878): 1, x(877): 0, x(876): 0, x(875): 0, x(874): 0, x(873): 1, x(872): 0, x(871): 1, x(870): 0, x(869): 1, x(868): 0, x(867): 0, x(866): 1, x(865): 1, x(864): 0, x(863): 0, x(862): 0, x(861): 0, x(860): 0, x(859): 0, x(858): 1, x(857): 0, x(856): 0, x(855): 1, x(854): 0, x(853): 0, x(852): 0, x(851): 1, x(850): 0, x(849): 0, x(848): 0, x(847): 1, x(846): 0, x(845): 1, x(844): 1, x(843): 0, x(842): 0, x(841): 0, x(840): 0, x(839): 1, x(838): 1, x(837): 0, x(836): 1, x(835): 0, x(834): 0, x(833): 1, x(832): 1, x(831): 1, x(830): 1, x(829): 0, x(828): 1, x(827): 0, x(826): 1, x(825): 0, x(824): 1, x(823): 1, x(822): 0, x(821): 0, x(820): 0, x(819): 1, x(818): 0, x(817): 1, x(816): 1, x(815): 0, x(814): 1, x(813): 0, x(812): 0, x(811): 0, x(810): 0, x(809): 0, x(808): 1, x(807): 0, x(806): 0, x(805): 1, x(804): 0, x(803): 1, x(802): 0, x(801): 0, x(800): 1, x(799): 1, x(798): 0, x(797): 0, x(796): 1, x(795): 0, x(794): 0, x(793): 1, x(792): 0, x(791): 0, x(790): 0, x(789): 0, x(788): 1, x(787): 1, x(786): 0, x(785): 1, x(784): 1, x(783): 0, x(782): 0, x(781): 0, x(780): 0, x(779): 1, x(778): 1, x(777): 0, x(776): 1, x(775): 0, x(774): 1, x(773): 1, x(772): 0, x(771): 1, x(770): 0, x(769): 0, x(768): 1, x(767): 0, x(766): 0, x(765): 0, x(764): 0, x(763): 0, x(762): 0, x(761): 0, x(760): 0, x(759): 0, x(758): 0, x(757): 0, x(756): 0, x(755): 0, x(754): 0, x(753): 0, x(752): 0, x(751): 0, x(750): 0, x(749): 0, x(748): 0, x(747): 0, x(746): 0, x(745): 0, x(744): 0, x(743): 0, x(742): 0, x(741): 0, x(740): 0, x(739): 0, x(738): 0, x(737): 0, x(736): 0, x(735): 0, x(734): 0, x(733): 0, x(732): 0, x(731): 1, x(730): 0, x(729): 0, x(728): 0, x(727): 0, x(726): 0, x(725): 0, x(724): 0, x(723): 0, x(722): 0, x(721): 0, x(720): 1, x(719): 0, x(718): 0, x(717): 0, x(716): 0, x(715): 1, x(714): 0, x(713): 0, x(712): 0, x(711): 0, x(710): 0, x(709): 0, x(708): 0, x(707): 0, x(706): 0, x(705): 0, x(704): 1, x(703): 0, x(702): 0, x(701): 0, x(700): 0, x(699): 0, x(698): 0, x(697): 0, x(696): 0, x(695): 0, x(694): 0, x(693): 0, x(692): 0, x(691): 0, x(690): 0, x(689): 0, x(688): 0, x(687): 0, x(686): 0, x(685): 0, x(684): 0, x(683): 0, x(682): 0, x(681): 0, x(680): 0, x(679): 0, x(678): 0, x(677): 0, x(676): 0, x(675): 0, x(674): 0, x(673): 0, x(672): 0, x(671): 0, x(670): 0, x(669): 0, x(668): 0, x(667): 0, x(666): 0, x(665): 0, x(664): 1, x(663): 0, x(662): 0, x(661): 0, x(660): 0, x(659): 1, x(658): 0, x(657): 0, x(656): 0, x(655): 0, x(654): 0, x(653): 0, x(652): 0, x(651): 0, x(650): 0, x(649): 0, x(648): 1, x(647): 0, x(646): 0, x(645): 0, x(644): 0, x(643): 1, x(642): 0, x(641): 0, x(640): 0, x(639): 0, x(638): 0, x(637): 0, x(636): 0, x(635): 0, x(634): 0, x(633): 0, x(632): 0, x(631): 0, x(630): 0, x(629): 0, x(628): 0, x(627): 0, x(626): 0, x(625): 0, x(624): 0, x(623): 0, x(622): 0, x(621): 0, x(620): 0, x(619): 0, x(618): 0, x(617): 0, x(616): 0, x(615): 0, x(614): 0, x(613): 0, x(612): 0, x(611): 0, x(610): 0, x(609): 0, x(608): 0, x(607): 0, x(606): 0, x(605): 0, x(604): 0, x(603): 0, x(602): 0, x(601): 0, x(600): 0, x(599): 0, x(598): 0, x(597): 0, x(596): 0, x(595): 0, x(594): 0, x(593): 0, x(592): 0, x(591): 0, x(590): 0, x(589): 0, x(588): 0, x(587): 0, x(586): 0, x(585): 0, x(584): 0, x(583): 0, x(582): 0, x(581): 0, x(580): 0, x(579): 0, x(578): 0, x(577): 0, x(576): 0, x(575): 0, x(574): 0, x(573): 0, x(572): 0, x(571): 0, x(570): 0, x(569): 0, x(568): 0, x(567): 0, x(566): 0, x(565): 0, x(564): 0, x(563): 0, x(562): 0, x(561): 0, x(560): 0, x(559): 0, x(558): 0, x(557): 0, x(556): 0, x(555): 0, x(554): 0, x(553): 0, x(552): 0, x(551): 0, x(550): 0, x(549): 0, x(548): 0, x(547): 0, x(546): 0, x(545): 0, x(544): 0, x(543): 0, x(542): 0, x(541): 0, x(540): 0, x(539): 0, x(538): 0, x(537): 0, x(536): 0, x(535): 0, x(534): 0, x(533): 0, x(532): 0, x(531): 0, x(530): 0, x(529): 0, x(528): 0, x(527): 0, x(526): 0, x(525): 0, x(524): 0, x(523): 0, x(522): 0, x(521): 0, x(520): 0, x(519): 0, x(518): 0, x(517): 0, x(516): 0, x(515): 0, x(514): 0, x(513): 0, x(512): 0, x(511): 0, x(510): 0, x(509): 0, x(508): 0, x(507): 0, x(506): 0, x(505): 0, x(504): 0, x(503): 0, x(502): 0, x(501): 0, x(500): 0, x(499): 0, x(498): 0, x(497): 0, x(496): 0, x(495): 0, x(494): 0, x(493): 0, x(492): 0, x(491): 0, x(490): 0, x(489): 0, x(488): 0, x(487): 0, x(486): 0, x(485): 0, x(484): 0, x(483): 0, x(482): 0, x(481): 0, x(480): 0, x(479): 0, x(478): 0, x(477): 0, x(476): 0, x(475): 1, x(474): 0, x(473): 0, x(472): 0, x(471): 0, x(470): 0, x(469): 0, x(468): 0, x(467): 0, x(466): 0, x(465): 0, x(464): 1, x(463): 0, x(462): 0, x(461): 0, x(460): 0, x(459): 1, x(458): 0, x(457): 0, x(456): 0, x(455): 0, x(454): 0, x(453): 0, x(452): 0, x(451): 0, x(450): 0, x(449): 0, x(448): 1, x(447): 0, x(446): 0, x(445): 0, x(444): 0, x(443): 0, x(442): 0, x(441): 0, x(440): 0, x(439): 0, x(438): 0, x(437): 0, x(436): 0, x(435): 0, x(434): 0, x(433): 0, x(432): 0, x(431): 0, x(430): 0, x(429): 0, x(428): 0, x(427): 0, x(426): 0, x(425): 0, x(424): 0, x(423): 0, x(422): 0, x(421): 0, x(420): 0, x(419): 0, x(418): 0, x(417): 0, x(416): 0, x(415): 0, x(414): 0, x(413): 0, x(412): 0, x(411): 0, x(410): 0, x(409): 0, x(408): 1, x(407): 0, x(406): 0, x(405): 0, x(404): 0, x(403): 1, x(402): 0, x(401): 0, x(400): 0, x(399): 0, x(398): 0, x(397): 0, x(396): 0, x(395): 0, x(394): 0, x(393): 0, x(392): 1, x(391): 0, x(390): 0, x(389): 0, x(388): 0, x(387): 1, x(386): 0, x(385): 0, x(384): 0, x(383): 1, x(382): 0, x(381): 1, x(380): 1, x(379): 1, x(378): 0, x(377): 0, x(376): 0, x(375): 0, x(374): 1, x(373): 0, x(372): 0, x(371): 0, x(370): 1, x(369): 0, x(368): 0, x(367): 0, x(366): 0, x(365): 1, x(364): 0, x(363): 0, x(362): 0, x(361): 0, x(360): 0, x(359): 0, x(358): 0, x(357): 0, x(356): 1, x(355): 0, x(354): 0, x(353): 1, x(352): 0, x(351): 0, x(350): 1, x(349): 0, x(348): 0, x(347): 0, x(346): 0, x(345): 0, x(344): 1, x(343): 1, x(342): 0, x(341): 1, x(340): 0, x(339): 0, x(338): 0, x(337): 0, x(336): 0, x(335): 0, x(334): 0, x(333): 1, x(332): 0, x(331): 0, x(330): 0, x(329): 0, x(328): 0, x(327): 0, x(326): 0, x(325): 1, x(324): 0, x(323): 0, x(322): 0, x(321): 0, x(320): 0, x(319): 0, x(318): 0, x(317): 0, x(316): 0, x(315): 1, x(314): 0, x(313): 1, x(312): 0, x(311): 0, x(310): 0, x(309): 0, x(308): 0, x(307): 0, x(306): 0, x(305): 0, x(304): 0, x(303): 0, x(302): 0, x(301): 0, x(300): 0, x(299): 0, x(298): 0, x(297): 0, x(296): 0, x(295): 0, x(294): 0, x(293): 0, x(292): 0, x(291): 1, x(290): 1, x(289): 0, x(288): 0, x(287): 0, x(286): 0, x(285): 0, x(284): 1, x(283): 0, x(282): 1, x(281): 0, x(280): 0, x(279): 0, x(278): 0, x(277): 0, x(276): 0, x(275): 0, x(274): 0, x(273): 0, x(272): 1, x(271): 0, x(270): 0, x(269): 0, x(268): 1, x(267): 0, x(266): 0, x(265): 0, x(264): 0, x(263): 0, x(262): 0, x(261): 0, x(260): 0, x(259): 1, x(258): 0, x(257): 0, x(256): 1, x(255): 0, x(254): 0, x(253): 0, x(252): 0, x(251): 0, x(250): 0, x(249): 0, x(248): 0, x(247): 0, x(246): 0, x(245): 0, x(244): 0, x(243): 0, x(242): 0, x(241): 0, x(240): 0, x(239): 0, x(238): 0, x(237): 0, x(236): 0, x(235): 0, x(234): 0, x(233): 0, x(232): 0, x(231): 0, x(230): 0, x(229): 0, x(228): 0, x(227): 0, x(226): 1, x(225): 0, x(224): 0, x(223): 0, x(222): 0, x(221): 0, x(220): 0, x(219): 0, x(218): 0, x(217): 0, x(216): 0, x(215): 0, x(214): 0, x(213): 0, x(212): 0, x(211): 0, x(210): 0, x(209): 0, x(208): 0, x(207): 0, x(206): 0, x(205): 0, x(204): 0, x(203): 0, x(202): 0, x(201): 1, x(200): 0, x(199): 0, x(198): 0, x(197): 0, x(196): 0, x(195): 1, x(194): 1, x(193): 0, x(192): 1, x(191): 0, x(190): 0, x(189): 1, x(188): 1, x(187): 1, x(186): 0, x(185): 0, x(184): 0, x(183): 0, x(182): 0, x(181): 0, x(180): 1, x(179): 0, x(178): 0, x(177): 1, x(176): 0, x(175): 0, x(174): 0, x(173): 0, x(172): 0, x(171): 0, x(170): 0, x(169): 0, x(168): 1, x(167): 0, x(166): 0, x(165): 1, x(164): 1, x(163): 0, x(162): 0, x(161): 1, x(160): 0, x(159): 0, x(158): 0, x(157): 0, x(156): 0, x(155): 0, x(154): 0, x(153): 0, x(152): 1, x(151): 0, x(150): 0, x(149): 1, x(148): 0, x(147): 0, x(146): 0, x(145): 0, x(144): 0, x(143): 0, x(142): 0, x(141): 0, x(140): 0, x(139): 0, x(138): 0, x(137): 0, x(136): 0, x(135): 0, x(134): 0, x(133): 0, x(132): 0, x(131): 0, x(130): 0, x(129): 1, x(128): 0, x(127): 0, x(126): 0, x(125): 0, x(124): 0, x(123): 0, x(122): 0, x(121): 0, x(120): 0, x(119): 0, x(118): 0, x(117): 0, x(116): 0, x(115): 0, x(114): 0, x(113): 0, x(112): 0, x(111): 0, x(110): 0, x(109): 0, x(108): 0, x(107): 0, x(106): 0, x(105): 0, x(104): 0, x(103): 0, x(102): 0, x(101): 0, x(100): 0, x(99): 1, x(98): 0, x(97): 0, x(96): 0, x(95): 0, x(94): 0, x(93): 0, x(92): 0, x(91): 0, x(90): 0, x(89): 0, x(88): 0, x(87): 0, x(86): 0, x(85): 1, x(84): 0, x(83): 0, x(82): 0, x(81): 0, x(80): 0, x(79): 0, x(78): 0, x(77): 0, x(76): 1, x(75): 1, x(74): 0, x(73): 0, x(72): 0, x(71): 0, x(70): 0, x(69): 0, x(68): 1, x(67): 0, x(66): 0, x(65): 0, x(64): 1, x(63): 0, x(62): 0, x(61): 0, x(60): 0, x(59): 1, x(58): 0, x(57): 0, x(56): 1, x(55): 0, x(54): 0, x(53): 0, x(52): 1, x(51): 0, x(50): 0, x(49): 0, x(48): 0, x(47): 0, x(46): 0, x(45): 0, x(44): 0, x(43): 1, x(42): 0, x(41): 1, x(40): 0, x(39): 0, x(38): 1, x(37): 0, x(36): 0, x(35): 0, x(34): 0, x(33): 0, x(32): 1, x(31): 1, x(30): 0, x(29): 0, x(28): 0, x(27): 1, x(26): 0, x(25): 0, x(24): 1, x(23): 0, x(22): 0, x(21): 0, x(20): 1, x(19): 0, x(18): 0, x(17): 0, x(16): 0, x(15): 0, x(14): 0, x(13): 0, x(12): 0, x(11): 0, x(10): 0, x(9): 0, x(8): 0, x(7): 0, x(6): 0, x(5): 0, x(4): 0, x(3): 1, x(2): 0, x(1): 0, x(0): 0}]
2022-06-20 16:20:34,023 - simple_example - INFO - end adding

However, Bosphous fails on this anf file (round4rxoodooMess.anf):

2022-06-20T07:58:17.619800542Z c Executed with command line: /usr/local/bin/bosphorus --anfread /dat/round4rxoodooMess.anf --anfwrite /dat/round4rxoodooMess_out.anf --cnfwrite /dat/round4rxoodooMess.cnf --solvewrite /dat/round4rxoodooMess_solution
2022-06-20T07:58:17.619824571Z c Compilation env CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS =  -Wall -Wextra -Wunused -pedantic -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -mtune=native -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -ggdb3 | COMPILE_DEFINES =  | STATICCOMPILE = ON | ONLY_SIMPLE =  | Boost_FOUND = TRUE | STATS =  | SQLITE3_FOUND =  | ZLIB_FOUND = TRUE | VALGRIND_FOUND =  | ENABLE_TESTING =  | M4RI_FOUND = TRUE | SLOW_DEBUG =  | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE =  | PYTHON_LIBRARY =  | PYTHON_INCLUDE_DIRS =  | MY_TARGETS =  | LARGEMEM =  | LIMITMEM =  | compilation date time = Apr 29 2021 22:02:25
2022-06-20T07:58:17.619835994Z c --- Configuration --
2022-06-20T07:58:17.619841676Z c maxTime = 1.00e+20
2022-06-20T07:58:17.619847392Z c XL simp (deg = 1; s = 30.00+4.00): 1
2022-06-20T07:58:17.619853535Z c EL simp (s = 30.00): 1
2022-06-20T07:58:17.619859228Z c SAT simp (10000:100000): 1
2022-06-20T07:58:17.619865200Z  using 1 threads
2022-06-20T07:58:17.619871036Z c Cut num: 5
2022-06-20T07:58:17.619876853Z c Brickenstein cutoff: 10
2022-06-20T07:58:17.619882647Z c --------------------
2022-06-20T07:58:21.689087178Z c [ANF Input] read in T: 3.94
2022-06-20T07:58:21.689162300Z c ---- ANF stats -----
2022-06-20T07:58:21.689169508Z c Num total vars: 1920
2022-06-20T07:58:21.689175978Z c Num free vars: 1920
2022-06-20T07:58:21.689181735Z c Num equations: 2704
2022-06-20T07:58:21.807457861Z c Num monoms in eqs: 179264
2022-06-20T07:58:21.851831198Z c Max deg in eqs: 2
2022-06-20T07:58:21.854066651Z c Simple XORs: 1168
2022-06-20T07:58:21.854096420Z c Num vars set: 0
2022-06-20T07:58:21.854173072Z c Num vars replaced: 0
2022-06-20T07:58:21.854187830Z c --------------------
2022-06-20T07:58:21.854293599Z c [ANF hash] Calculating ANF hash...
2022-06-20T07:58:21.865799096Z c [ANF hash] Done. T: 0.00
2022-06-20T07:58:21.865897327Z c Simplifying....
2022-06-20T07:58:21.865904919Z c [boshp] Running iterative simplification...
2022-06-20T07:58:21.865911085Z c [ANF prop] Running ANF propagation...
2022-06-20T07:58:22.769962325Z c [ANF prop] Left eqs: 808 T: 0.90
2022-06-20T07:58:22.770040407Z c [iter-simp] ------ Iteration 0
2022-06-20T07:58:22.770048489Z c [XL] Running XL... ring size: 1920
2022-06-20T07:58:26.127939826Z c [XL] Done. Learnt: 40 T: 3.30
2022-06-20T07:58:26.137337924Z c [XL] learnt 9 new facts in 3.31 seconds.
2022-06-20T07:58:26.137424810Z c [ANF prop] Running ANF propagation...
2022-06-20T07:58:26.158797584Z c [ANF prop] Left eqs: 817 T: 0.02
2022-06-20T07:58:26.158865648Z c [iter-simp] ------ Iteration 0
2022-06-20T07:58:26.158872314Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:58:41.226907049Z c [ElimLin] Done. Learnt: 99 T: 14.84
2022-06-20T07:58:41.231490344Z c [ElimLin] learnt 59 new facts in 14.85 seconds.
2022-06-20T07:58:41.231578187Z c [ANF prop] Running ANF propagation...
2022-06-20T07:58:41.368560109Z c [ANF prop] Left eqs: 852 T: 0.14
2022-06-20T07:58:41.368657046Z c [iter-simp] ------ Iteration 0
2022-06-20T07:58:41.372565145Z c [CNF-gen] Number of value assignments = 792
2022-06-20T07:58:41.372637247Z c Number of equiv assigments = 15
2022-06-20T07:58:45.254639690Z c [SAT] learnt 5 new facts in 3.81 seconds.
2022-06-20T07:58:45.254734638Z c [ANF prop] Running ANF propagation...
2022-06-20T07:58:45.295582989Z c [ANF prop] Left eqs: 847 T: 0.04
2022-06-20T07:58:45.296101886Z c [iter-simp] ------ Iteration 1
2022-06-20T07:58:45.296130123Z c [XL] Running XL... ring size: 1920
2022-06-20T07:58:46.295489505Z c [XL] Done. Learnt: 70 T: 0.99
2022-06-20T07:58:46.312866172Z c [XL] learnt 14 new facts in 1.01 seconds.
2022-06-20T07:58:46.312959147Z c [ANF prop] Running ANF propagation...
2022-06-20T07:58:46.375559114Z c [ANF prop] Left eqs: 851 T: 0.06
2022-06-20T07:58:46.375654804Z c [iter-simp] ------ Iteration 1
2022-06-20T07:58:46.375666038Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:58:50.467696215Z c [ElimLin] Done. Learnt: 79 T: 4.07
2022-06-20T07:58:50.470095980Z c [ElimLin] learnt 14 new facts in 4.07 seconds.
2022-06-20T07:58:50.470149182Z c [ANF prop] Running ANF propagation...
2022-06-20T07:58:50.535355868Z c [ANF prop] Left eqs: 865 T: 0.06
2022-06-20T07:58:50.535453328Z c [iter-simp] ------ Iteration 1
2022-06-20T07:58:50.621469804Z c [CNF-gen] Number of value assignments = 802
2022-06-20T07:58:50.621554870Z c Number of equiv assigments = 15
2022-06-20T07:58:54.933100440Z c [SAT] learnt 4 new facts in 4.38 seconds.
2022-06-20T07:58:54.933212770Z c [ANF prop] Running ANF propagation...
2022-06-20T07:58:54.969196099Z c [ANF prop] Left eqs: 861 T: 0.04
2022-06-20T07:58:54.969789128Z c [iter-simp] ------ Iteration 2
2022-06-20T07:58:54.969838139Z c [XL] Running XL... ring size: 1920
2022-06-20T07:58:55.889765109Z c [XL] Done. Learnt: 75 T: 0.92
2022-06-20T07:58:55.903924765Z c [XL] learnt 33 new facts in 0.93 seconds.
2022-06-20T07:58:55.904039661Z c [ANF prop] Running ANF propagation...
2022-06-20T07:58:55.978438165Z c [ANF prop] Left eqs: 874 T: 0.08
2022-06-20T07:58:55.978535023Z c [iter-simp] ------ Iteration 2
2022-06-20T07:58:55.978545206Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:58:58.761932698Z c [ElimLin] Done. Learnt: 78 T: 2.78
2022-06-20T07:58:58.763874554Z c [ElimLin] learnt 11 new facts in 2.78 seconds.
2022-06-20T07:58:58.763911840Z c [ANF prop] Running ANF propagation...
2022-06-20T07:58:58.834256688Z c [ANF prop] Left eqs: 885 T: 0.07
2022-06-20T07:58:58.834349010Z c [iter-simp] ------ Iteration 2
2022-06-20T07:58:58.938050793Z c [CNF-gen] Number of value assignments = 814
2022-06-20T07:58:58.938142592Z c Number of equiv assigments = 15
2022-06-20T07:59:02.759033216Z c [SAT] learnt 7 new facts in 3.92 seconds.
2022-06-20T07:59:02.759120954Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:02.813073219Z c [ANF prop] Left eqs: 878 T: 0.06
2022-06-20T07:59:02.813595612Z c [iter-simp] ------ Iteration 3
2022-06-20T07:59:02.813628110Z c [XL] Running XL... ring size: 1920
2022-06-20T07:59:03.595304894Z c [XL] Done. Learnt: 71 T: 0.78
2022-06-20T07:59:03.607622804Z c [XL] learnt 6 new facts in 0.79 seconds.
2022-06-20T07:59:03.607706063Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:03.636517663Z c [ANF prop] Left eqs: 878 T: 0.03
2022-06-20T07:59:03.636615313Z c [iter-simp] ------ Iteration 3
2022-06-20T07:59:03.636629949Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:59:06.503275015Z c [ElimLin] Done. Learnt: 80 T: 2.86
2022-06-20T07:59:06.505205142Z c [ElimLin] learnt 12 new facts in 2.86 seconds.
2022-06-20T07:59:06.505251433Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:06.552887902Z c [ANF prop] Left eqs: 890 T: 0.05
2022-06-20T07:59:06.552975282Z c [iter-simp] ------ Iteration 3
2022-06-20T07:59:06.628935508Z c [CNF-gen] Number of value assignments = 824
2022-06-20T07:59:06.629029964Z c Number of equiv assigments = 15
2022-06-20T07:59:10.082231185Z c [SAT] learnt 9 new facts in 3.53 seconds.
2022-06-20T07:59:10.082335692Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:10.245426899Z c [ANF prop] Left eqs: 881 T: 0.16
2022-06-20T07:59:10.246041063Z c [iter-simp] ------ Iteration 4
2022-06-20T07:59:10.246071033Z c [XL] Running XL... ring size: 1920
2022-06-20T07:59:11.072053258Z c [XL] Done. Learnt: 71 T: 0.82
2022-06-20T07:59:11.085552069Z c [XL] learnt 12 new facts in 0.84 seconds.
2022-06-20T07:59:11.085639460Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:11.110836285Z c [ANF prop] Left eqs: 886 T: 0.02
2022-06-20T07:59:11.110924175Z c [iter-simp] ------ Iteration 4
2022-06-20T07:59:11.110971998Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:59:14.878682038Z c [ElimLin] Done. Learnt: 85 T: 3.77
2022-06-20T07:59:14.880571202Z c [ElimLin] learnt 17 new facts in 3.77 seconds.
2022-06-20T07:59:14.880605017Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:14.927853802Z c [ANF prop] Left eqs: 902 T: 0.04
2022-06-20T07:59:14.927934476Z c [iter-simp] ------ Iteration 4
2022-06-20T07:59:15.001706938Z c [CNF-gen] Number of value assignments = 837
2022-06-20T07:59:15.001784388Z c Number of equiv assigments = 15
2022-06-20T07:59:18.613005552Z c [SAT] learnt 12 new facts in 3.69 seconds.
2022-06-20T07:59:18.613105080Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:18.663592353Z c [ANF prop] Left eqs: 888 T: 0.05
2022-06-20T07:59:18.664302469Z c [iter-simp] ------ Iteration 5
2022-06-20T07:59:18.664340439Z c [XL] Running XL... ring size: 1920
2022-06-20T07:59:19.426965627Z c [XL] Done. Learnt: 71 T: 0.76
2022-06-20T07:59:19.437345746Z c [XL] learnt 13 new facts in 0.77 seconds.
2022-06-20T07:59:19.437449821Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:19.454591070Z c [ANF prop] Left eqs: 891 T: 0.02
2022-06-20T07:59:19.454680105Z c [iter-simp] ------ Iteration 5
2022-06-20T07:59:19.454689408Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:59:23.942814972Z c [ElimLin] Done. Learnt: 103 T: 4.49
2022-06-20T07:59:23.949122717Z c [ElimLin] learnt 34 new facts in 4.49 seconds.
2022-06-20T07:59:23.949195092Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:24.034200227Z c [ANF prop] Left eqs: 913 T: 0.09
2022-06-20T07:59:24.034299719Z c [iter-simp] ------ Iteration 5
2022-06-20T07:59:24.115732697Z c [CNF-gen] Number of value assignments = 853
2022-06-20T07:59:24.115826187Z c Number of equiv assigments = 18
2022-06-20T07:59:27.089524936Z c [SAT] learnt 13 new facts in 3.05 seconds.
2022-06-20T07:59:27.089614748Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:27.169555359Z c [ANF prop] Left eqs: 896 T: 0.08
2022-06-20T07:59:27.170697483Z c [iter-simp] ------ Iteration 6
2022-06-20T07:59:27.170733702Z c [XL] Running XL... ring size: 1920
2022-06-20T07:59:27.921510766Z c [XL] Done. Learnt: 87 T: 0.75
2022-06-20T07:59:27.931854032Z c [XL] learnt 24 new facts in 0.76 seconds.
2022-06-20T07:59:27.931944701Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:27.962633094Z c [ANF prop] Left eqs: 908 T: 0.03
2022-06-20T07:59:27.962731885Z c [iter-simp] ------ Iteration 6
2022-06-20T07:59:27.962747578Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:59:31.781160183Z c [ElimLin] Done. Learnt: 111 T: 3.82
2022-06-20T07:59:31.782785054Z c [ElimLin] learnt 29 new facts in 3.82 seconds.
2022-06-20T07:59:31.782826232Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:31.896200672Z c [ANF prop] Left eqs: 908 T: 0.11
2022-06-20T07:59:31.896289048Z c [iter-simp] ------ Iteration 6
2022-06-20T07:59:31.962825438Z c [CNF-gen] Number of value assignments = 882
2022-06-20T07:59:31.962924770Z c Number of equiv assigments = 28
2022-06-20T07:59:34.661815546Z c [SAT] learnt 12 new facts in 2.76 seconds.
2022-06-20T07:59:34.661936221Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:34.727860991Z c [ANF prop] Left eqs: 898 T: 0.06
2022-06-20T07:59:34.728569188Z c [iter-simp] ------ Iteration 7
2022-06-20T07:59:34.728595537Z c [XL] Running XL... ring size: 1920
2022-06-20T07:59:35.336091982Z c [XL] Done. Learnt: 88 T: 0.60
2022-06-20T07:59:35.345916057Z c [XL] learnt 28 new facts in 0.62 seconds.
2022-06-20T07:59:35.346001907Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:35.368619827Z c [ANF prop] Left eqs: 915 T: 0.02
2022-06-20T07:59:35.368708689Z c [iter-simp] ------ Iteration 7
2022-06-20T07:59:35.368720660Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:59:40.231021324Z c [ElimLin] Done. Learnt: 132 T: 4.86
2022-06-20T07:59:40.233582906Z c [ElimLin] learnt 49 new facts in 4.86 seconds.
2022-06-20T07:59:40.233632430Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:40.330154049Z c [ANF prop] Left eqs: 898 T: 0.10
2022-06-20T07:59:40.330242902Z c [iter-simp] ------ Iteration 7
2022-06-20T07:59:40.390813583Z c [CNF-gen] Number of value assignments = 910
2022-06-20T07:59:40.390902131Z c Number of equiv assigments = 36
2022-06-20T07:59:42.610645098Z c [SAT] learnt 7 new facts in 2.28 seconds.
2022-06-20T07:59:42.610737296Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:42.646195297Z c [ANF prop] Left eqs: 888 T: 0.04
2022-06-20T07:59:42.647039607Z c [iter-simp] ------ Iteration 8
2022-06-20T07:59:42.647065952Z c [XL] Running XL... ring size: 1920
2022-06-20T07:59:43.190866671Z c [XL] Done. Learnt: 110 T: 0.54
2022-06-20T07:59:43.199209295Z c [XL] learnt 50 new facts in 0.55 seconds.
2022-06-20T07:59:43.199290514Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:43.257203695Z c [ANF prop] Left eqs: 894 T: 0.06
2022-06-20T07:59:43.257285621Z c [iter-simp] ------ Iteration 8
2022-06-20T07:59:43.257297947Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:59:47.270156265Z c [ElimLin] Done. Learnt: 127 T: 4.01
2022-06-20T07:59:47.272524026Z c [ElimLin] learnt 33 new facts in 4.02 seconds.
2022-06-20T07:59:47.272595541Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:47.332473907Z c [ANF prop] Left eqs: 919 T: 0.06
2022-06-20T07:59:47.332566629Z c [iter-simp] ------ Iteration 8
2022-06-20T07:59:47.385981735Z c [CNF-gen] Number of value assignments = 935
2022-06-20T07:59:47.386062644Z c Number of equiv assigments = 42
2022-06-20T07:59:49.766131035Z c [SAT] learnt 9 new facts in 2.43 seconds.
2022-06-20T07:59:49.766214333Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:49.824292292Z c [ANF prop] Left eqs: 894 T: 0.06
2022-06-20T07:59:49.825107979Z c [iter-simp] ------ Iteration 9
2022-06-20T07:59:49.825133936Z c [XL] Running XL... ring size: 1920
2022-06-20T07:59:50.357870207Z c [XL] Done. Learnt: 108 T: 0.53
2022-06-20T07:59:50.366334463Z c [XL] learnt 38 new facts in 0.54 seconds.
2022-06-20T07:59:50.366423621Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:50.416525014Z c [ANF prop] Left eqs: 910 T: 0.05
2022-06-20T07:59:50.416601681Z c [iter-simp] ------ Iteration 9
2022-06-20T07:59:50.416611980Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:59:53.273058749Z c [ElimLin] Done. Learnt: 112 T: 2.86
2022-06-20T07:59:53.275078584Z c [ElimLin] learnt 15 new facts in 2.86 seconds.
2022-06-20T07:59:53.275120226Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:53.339225501Z c [ANF prop] Left eqs: 917 T: 0.06
2022-06-20T07:59:53.339314830Z c [iter-simp] ------ Iteration 9
2022-06-20T07:59:53.412038897Z c [CNF-gen] Number of value assignments = 956
2022-06-20T07:59:53.412123888Z c Number of equiv assigments = 48
2022-06-20T07:59:55.507490488Z c [SAT] learnt 8 new facts in 2.16 seconds.
2022-06-20T07:59:55.507580500Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:55.567542990Z c [ANF prop] Left eqs: 902 T: 0.06
2022-06-20T07:59:55.568355624Z c [iter-simp] ------ Iteration 10
2022-06-20T07:59:55.568380533Z c [XL] Running XL... ring size: 1920
2022-06-20T07:59:56.034057014Z c [XL] Done. Learnt: 104 T: 0.46
2022-06-20T07:59:56.040183340Z c [XL] learnt 26 new facts in 0.47 seconds.
2022-06-20T07:59:56.040260846Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:56.067725858Z c [ANF prop] Left eqs: 901 T: 0.02
2022-06-20T07:59:56.067807139Z c [iter-simp] ------ Iteration 10
2022-06-20T07:59:56.067819223Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:59:59.645220405Z c [ElimLin] Done. Learnt: 128 T: 3.58
2022-06-20T07:59:59.647154176Z c [ElimLin] learnt 33 new facts in 3.58 seconds.
2022-06-20T07:59:59.647194462Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:59.718167267Z c [ANF prop] Left eqs: 911 T: 0.07
2022-06-20T07:59:59.718291005Z c [iter-simp] ------ Iteration 10
2022-06-20T07:59:59.765949081Z c [CNF-gen] Number of value assignments = 984
2022-06-20T07:59:59.766028518Z c Number of equiv assigments = 55
2022-06-20T08:00:01.826250829Z c [SAT] learnt 9 new facts in 2.11 seconds.
2022-06-20T08:00:01.826326359Z c [ANF prop] Running ANF propagation...
2022-06-20T08:00:01.891122043Z c [ANF prop] Left eqs: 902 T: 0.06
2022-06-20T08:00:01.892364967Z c [iter-simp] ------ Iteration 11
2022-06-20T08:00:01.892398426Z c [XL] Running XL... ring size: 1920
2022-06-20T08:00:02.524764928Z c [XL] Done. Learnt: 109 T: 0.63
2022-06-20T08:00:02.530938259Z c [XL] learnt 29 new facts in 0.64 seconds.
2022-06-20T08:00:02.531020246Z c [ANF prop] Running ANF propagation...
2022-06-20T08:00:02.557478092Z c [ANF prop] Left eqs: 917 T: 0.03
2022-06-20T08:00:02.557561234Z c [iter-simp] ------ Iteration 11
2022-06-20T08:00:02.557573516Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T08:00:05.511004820Z c [ElimLin] Done. Learnt: 130 T: 2.95
2022-06-20T08:00:05.512747579Z c [ElimLin] learnt 28 new facts in 2.95 seconds.
2022-06-20T08:00:05.512790493Z c [ANF prop] Running ANF propagation...
2022-06-20T08:00:05.592247821Z c [ANF prop] Left eqs: 898 T: 0.08
2022-06-20T08:00:05.592336615Z c [iter-simp] ------ Iteration 11
2022-06-20T08:00:05.635623341Z c [CNF-gen] Number of value assignments = 1008
2022-06-20T08:00:05.635709815Z c Number of equiv assigments = 68
2022-06-20T08:00:06.671523225Z c [SAT] learnt 1 new facts in 1.08 seconds.
2022-06-20T08:00:06.671610062Z c [ANF prop] Running ANF propagation...
2022-06-20T08:00:06.697521482Z c [ANF prop] Left eqs: 897 T: 0.03
2022-06-20T08:00:06.698409972Z c [iter-simp] ------ Iteration 12
2022-06-20T08:00:06.698438465Z c [XL] Running XL... ring size: 1920
2022-06-20T08:00:07.111982401Z c [XL] Done. Learnt: 121 T: 0.41
2022-06-20T08:00:07.116467059Z c [XL] learnt 51 new facts in 0.42 seconds.
2022-06-20T08:00:07.116541073Z c [ANF prop] Running ANF propagation...
2022-06-20T08:00:07.155870081Z c [ANF prop] Left eqs: 904 T: 0.04
2022-06-20T08:00:07.155961179Z c [iter-simp] ------ Iteration 12
2022-06-20T08:00:07.155972878Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T08:00:08.358255336Z c [GJ] UnSAT
2022-06-20T08:00:08.358341190Z c [ElimLin] learnt 0 new facts in 1.20 seconds.
2022-06-20T08:00:08.397669682Z c [ after 12.2 iteration(s) in 106.01 seconds.]
2022-06-20T08:00:08.397755334Z c Simplifying finished.
2022-06-20T08:00:08.397772071Z c ---- ANF stats -----
2022-06-20T08:00:08.397779898Z c Num total vars: 1920
2022-06-20T08:00:08.397826334Z c Num free vars: 862
2022-06-20T08:00:08.397834030Z c Num equations: 904
2022-06-20T08:00:08.401528820Z c Num monoms in eqs: 27752
2022-06-20T08:00:08.404940346Z c Max deg in eqs: 2
2022-06-20T08:00:08.404995352Z c Simple XORs: 256
2022-06-20T08:00:08.405005318Z c Num vars set: 1025
2022-06-20T08:00:08.405011921Z c Num vars replaced: 71
2022-06-20T08:00:08.405018350Z c --------------------
2022-06-20T08:00:08.427854447Z c [CNF-out] added UNSAT to CNF
2022-06-20T08:00:08.432458504Z c [CNF-gen] Number of value assignments = 1025
2022-06-20T08:00:08.432530241Z c Number of equiv assigments = 71
2022-06-20T08:00:08.871734367Z c [CNF conversion] in 0.44 seconds.
2022-06-20T08:00:08.871803920Z c ---- CNF stats -----
2022-06-20T08:00:08.871814251Z c Map sizes            : 15816/21627
2022-06-20T08:00:08.871823135Z c Clause Sets          : 15897
2022-06-20T08:00:08.871830112Z c Added as CNF         : 53
2022-06-20T08:00:08.871836314Z c Added as simple ANF  : 1352
2022-06-20T08:00:08.871842314Z c Added as complex  ANF: 595
2022-06-20T08:00:08.871848690Z c --------------------
2022-06-20T08:00:09.843517509Z s ANF-UNSATISFIABLE
2022-06-20T08:00:09.852624934Z c Learnt 918 fact(s) in 111.32 seconds using 172.41MB.

Solution found is not a solution to the ANF

Hi,

We have the following problem. For the attached set of equations over GF(2) in the ANF (task1.txt) , we created CNF attached (poly5513ep.cnf). This CNF does not make any result for CryptoMiniSat but with MiniSat 1.14 we got the solution attached (solution.txt), but it does not correspond with the solution of the original ANF. Could you explain us the problem please?
Petr & Vojtěch

task1.txt
solution.txt
poly5513ep.zip

Evaluating the key research space

Hello,
how to modify the source code such that enable it to support counting and outputting all the
possible key solutions automatically?

Another solution found is not a solution to the ANF

Hi,

I have another problem with Bosphorus (version 5e9d72d) similar to previous one. Given ANF (task2.anf.txt) was processed by Bosphorus to generate CNF (task2.cnf.txt). Cryptominisat solved the CNF, but its outcome (solution2_cnf_false.txt) is not a valid solution of the ANF. I attach the correct solution of the ANF (solution2_anf_right.txt) obtained differently. Furthemore, I am confused that I had to call Cryptominisat separately.
Could you please help?

Thank you
Vojtech

solution2_anf_right.txt
solution2_cnf_false.txt
task2.anf.txt
task2.cnf.txt

We should implement the Linear/Double Partner Strategy, Quadratic Partner Substitution etc ideas by Jovanovic and Kreuzer

Paper here. "Algebraic Attacks using SAT-Solvers". Authors: Philipp Jovanovic and Martin Kreuzer. Implementation here.

These strategies look like they could be interesting to improve the translation. Some checking is needed to verify whether our espresso-based system covers these cases.

different CNF

Hi!
I have been using both bosphorus and anf2cnf.py. For some fixed system of ANF equations, even by changing the cut parameter, I have been unable to generate by bosphorus the same CNF that I obtain by anf2cnf.py. Is it possible to do this in some way? I'm very interested to the CNF obtained by anf2cnf.py because I have found that, for my problem, this is more efficient than the ones that I'm be able to obtain by bosphorus. But I need bosphorus to convert back solutions to the ANF form.
Many thanks in advance. Bob

--solvewrite() within Bosphorus is faster than Cryptominisat5 to solve cnf file

Hi!, Mate
Bosphorus uses CryptoMiniSat for the SAT solving stage internally, but why when I solve my output file (6rgimli.cnf),
--anfread 6rgimli.anf --cnfwrite 6rgimli.cnf --solvewrite 6rgimli_solution then Bosphorus is faster than Cryptominisat5 to solve the same 6rgimli.cnf file? For Bosphorus, it takes only 24s,

but for Cryptominisat5(the same version 5.8.0 ) , cryptominisat5 6rgimli.cnf,

it is still running, more than 9 hours.

Thanks you in advance!
Huina

c Compilation env CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS =  -Wall -Wextra -Wunused -pedantic -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -mtune=native -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -ggdb3 | COMPILE_DEFINES =  | STATICCOMPILE = OFF | ONLY_SIMPLE =  | Boost_FOUND = 1 | STATS =  | SQLITE3_FOUND =  | ZLIB_FOUND = TRUE | VALGRIND_FOUND =  | ENABLE_TESTING =  | M4RI_FOUND = TRUE | SLOW_DEBUG =  | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE =  | PYTHON_LIBRARY =  | PYTHON_INCLUDE_DIRS =  | MY_TARGETS =  | LARGEMEM =  | LIMITMEM =  | compilation date time = Jun 29 2022 21:11:00
c --- Configuration --
c maxTime = 1.00e+20
c XL simp (deg = 1; s = 30.00+4.00): 1
c EL simp (s = 30.00): 1
c SAT simp (10000:100000): 1
 using 1 threads
c Cut num: 5
c Brickenstein cutoff: 10
c --------------------
c [ANF Input] read in T: 0.06
c ---- ANF stats -----
c Num total vars: 5023
c Num free vars: 5023
c Num equations: 6298
c Num monoms in eqs: 25750
c Max deg in eqs: 2
c Simple XORs: 2222
c Num vars set: 0
c Num vars replaced: 0
c --------------------
c [ANF hash] Calculating ANF hash...
c [ANF hash] Done. T: 0.00
c Simplifying....
c [boshp] Running iterative simplification...
c [ANF prop] Running ANF propagation...
c [ANF prop] Left eqs: 2897 T: 0.04
c [iter-simp] ------ Iteration 0
c [XL] Running XL... ring size: 5023
c [XL] Done. Learnt: 133 T: 0.19
c [XL] learnt 23 new facts in 0.19 seconds.
c [ANF prop] Running ANF propagation...
c [ANF prop] Left eqs: 2915 T: 0.00
c [iter-simp] ------ Iteration 0
c [ElimLin] Running ElimLin... ring size: 5023
c [ElimLin] Done. Learnt: 131 T: 0.18
c [ElimLin] learnt 0 new facts in 0.18 seconds.
c [iter-simp] ------ Iteration 0
c [CNF-gen] Number of value assignments = 1838
c Number of equiv assigments = 596
c [SAT] learnt 1 new facts in 0.65 seconds.
c [ANF prop] Running ANF propagation...
c [ANF prop] Left eqs: 2913 T: 0.01
c [iter-simp] ------ Iteration 1
c [XL] Running XL... ring size: 5023
c [XL] Done. Learnt: 135 T: 0.18
c [XL] learnt 2 new facts in 0.18 seconds.
c [ANF prop] Running ANF propagation...
c [ANF prop] Left eqs: 2915 T: 0.00
c [iter-simp] ------ Iteration 1
c [ElimLin] Running ElimLin... ring size: 5023
c [ElimLin] Done. Learnt: 136 T: 0.26
c [ElimLin] learnt 1 new facts in 0.26 seconds.
c [ANF prop] Running ANF propagation...
c [ANF prop] Left eqs: 2916 T: 0.00
c [iter-simp] ------ Iteration 1
c [CNF-gen] Number of value assignments = 1852
c Number of equiv assigments = 598
c [SAT] learnt 0 new facts in 0.60 seconds.
c [iter-simp] ------ Iteration 2
c [XL] Running XL... ring size: 5023
c [XL] Done. Learnt: 136 T: 0.18
c [XL] learnt 0 new facts in 0.18 seconds.
c [iter-simp] ------ Iteration 2
c [ElimLin] Running ElimLin... ring size: 5023
c [ElimLin] Done. Learnt: 136 T: 0.19
c [ElimLin] learnt 0 new facts in 0.19 seconds.
c [iter-simp] ------ Iteration 2
c [CNF-gen] Number of value assignments = 1852
c Number of equiv assigments = 598
c [SAT] learnt 0 new facts in 0.58 seconds.
c [ after 3.0 iteration(s) in 3.08 seconds.]
c Simplifying finished.
c ---- ANF stats -----
c Num total vars: 5023
c Num free vars: 2876
c Num equations: 2916
c Num monoms in eqs: 13590
c Max deg in eqs: 2
c Simple XORs: 157
c Num vars set: 1852
c Num vars replaced: 598
c --------------------
c [CNF-gen] Number of value assignments = 1852
c Number of equiv assigments = 598
c [CNF conversion] in 0.24 seconds.
c ---- CNF stats -----
c Map sizes            : 5023/5025
c Clause Sets          : 5366
c Added as CNF         : 2759
c Added as simple ANF  : 2607
c Added as complex  ANF: 0
c --------------------
s ANF-SATISFIABLE
v x(0) x(1) x(2) x(3) x(4) x(5) x(6) 1+x(7) ...
c Solution found is correct.
c Learnt 537 fact(s) in 23.95 seconds using 92.59MB.
solve end time is: 2022/07/03/22:16:45:26
solve exec time is: 24.111012s

6rgimli.zip

Current master branch does not properly NULL terminate arguments to execl

First of all, many thanks for making this tool freely available!

It appears that a recent commit (dabd13a) removed the last argument to execl in satsolve.cpp which needs to be NULL:

bosphorus/src/satsolve.cpp

Line 73 in 5a3e24f

execl(solverExecutable.c_str(), solverExecutable.c_str(), "--polar" , "false");

Coupled with the redirection of stdout and stderr to the pipe, this leads to an error of the form

ERROR! Line 'ERROR! Could not execute '/usr/local/bin/cryptominisat5'' doesn't contain correct starting character

which is not easily interpreted as being a problem with running the child process (at least, it wasn't obvious to me).

To reproduce, build from master branch and run the example in README

My suggestion is that it may be better to not redirect stderr to the pipe, which would allow the error to be printed at the right place.

I will shortly submit a PR that makes both these changes. Please merge if appropriate.

Thanks
Avinash

ANF projection set parsing skips file after first comment

Upon reading a regular comment line c foo ..., the following lines in the projection set parser appear to break entirely out of the ANF parsing loop (and ignore the rest of the input file). I guess they should continue instead of break.

https://github.com/meelgroup/bosphorus/blob/master/src/anf.cpp#L131
https://github.com/meelgroup/bosphorus/blob/master/src/anf.cpp#L133
https://github.com/meelgroup/bosphorus/blob/master/src/anf.cpp#L135

Example file:

x(0)
x(2)
c foo
x(1)

Bosphorus with --allsol gives:

...
s ANF-SATISFIABLE
v x(0) x(1) x(2) 
c Solution found is correct.
s ANF-SATISFIABLE
v x(0) 1+x(1) x(2) 
c Solution found is correct.
s ANF-UNSATISFIABLE
c Number of solutions found: 2

How can one get all the solutions from Bosphorus?

The question has been asked: "given an ANF, how can I find all the solutions to the system given Bosphorus?"

Recommend Projects

React

A declarative, efficient, and flexible JavaScript library for building user interfaces.
Vue.js

🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
TensorFlow

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
D3

Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

javascript

JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
web

Some thing interesting about web. New door for the world.
server

A server is a program made to process requests and deliver data to clients.
Machine learning

Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.