Opened 4 years ago

Closed 4 years ago

#26676 closed defect (fixed)

Fix var() method for cryptominisat and picosat, which breaks solve_sat for boolean polynomial systems

Reported by: Hosein Hadipour Owned by:
Priority: major Milestone: sage-8.7
Component: packages: optional Keywords: solve_sat, CryptoMiniSat, picosat
Cc: Thierry Monteil Merged in:
Authors: Thierry Monteil Reviewers: Frédéric Chapoton
Report Upstream: N/A Work issues:
Branch: c492724 (Commits, GitHub, GitLab) Commit: c492724e2af4918c65360b82cded10f1f9d5877b
Dependencies: Stopgaps:

Status badges

Description (last modified by Thierry Monteil)

When I used Sage7.2, I could easily solve my boolean equations with solve_sat commands, and it's results were verified by the papers and other tools, but when I upgraded my sage to version 8 (or later version) I found that the new solve_sat solver (especially when we use CryptoMiniSat? as the SAT solver) doesn't work as correct as before. For example, when I solve a system of equations via solve_sat which used CryptoMiniSat? as a SAT solver, I get different number of solutions in different version of SageMath. I believe that there is something wrong in newer version of SageMath because my previous experiences shows that the older version's results were verified by the other tools and papers. I hope someone could solve this problem.

See also the following thread on sage-devel: https://groups.google.com/forum/?fromgroups#!topic/sage-devel/2EhgHzGgUnQ

Attachments (1)

ph1234.pdf (31.7 KB) - added by faustjonson 4 years ago.

Download all attachments as: .zip

Change History (19)

comment:1 Changed 4 years ago by Jeroen Demeyer

Can you be more concrete exactly what the problem is?

comment:2 Changed 4 years ago by Thierry Monteil

Authors: Thierry Monteil
Cc: Thierry Monteil added
Component: PLEASE CHANGEpackages: experimental
Keywords: Thierry Monteil removed
Milestone: sage-8.5sage-pending
Status: newneeds_info
Summary: solve_sat doesn't work correctly after Thierry Monteil changed the original CryptoMiniSat Solversolve_sat doesn't work correctly after migration of CryptoMiniSat from version 2 to 5
Type: PLEASE CHANGEdefect

As suggested by Jeroen, you should provide explicit (if possible minimal) code so that we can understand the actual issue and work from something. There might indeed be an issue with boolean equations since it relied on a learnt_clauses method that does not exist anymore, and the code lacks of doctests.

By the way, a good way to hint some developer about an issue is to add her nickname in the CC field so that she could recieve an email. In the title, author field or keywords field, only the people who have a regular look at the timeline will notice.

Last edited 4 years ago by Thierry Monteil (previous) (diff)

comment:3 in reply to:  2 ; Changed 4 years ago by Hosein Hadipour

Replying to tmonteil:

As suggested by Jeroen, you should provide explicit (if possible minimal) code so that we can understand the actual issue and work from something. There might indeed be an issue with boolean equations since it relied on a learnt_clauses method that does not exist anymore, and the code lacks of doctests.

By the way, a good way to hint some developer about an issue is to add her nickname in the CC field so that she could recieve an email. In the title, author field or keywords field, only the people who have a regular look at the timeline will notice.

Dear Monteli,

Regarding to explicit code for understanding the actual issue: I'll upload a code that generate a system of boolean equations which shows the issue exactly. This system of equations is extracted from a stream cipher called Bivium-B and I've solved it several times in Sage 7.2, and I'm certain that it has a unique solution, but when I want to solve it via the newer versions of SageMath (after 8.0), solver returns False as the output, which means there is not any solutions! I'll upload the code as soon as possible.

Thanks in advance for your help

Last edited 4 years ago by Hosein Hadipour (previous) (diff)

Changed 4 years ago by faustjonson

Attachment: ph1234.pdf added

comment:4 in reply to:  3 Changed 4 years ago by Hosein Hadipour

Replying to gh-hadipourh:

Replying to tmonteil:

As suggested by Jeroen, you should provide explicit (if possible minimal) code so that we can understand the actual issue and work from something. There might indeed be an issue with boolean equations since it relied on a learnt_clauses method that does not exist anymore, and the code lacks of doctests.

By the way, a good way to hint some developer about an issue is to add her nickname in the CC field so that she could recieve an email. In the title, author field or keywords field, only the people who have a regular look at the timeline will notice.

Dear Monteli,

Regarding to explicit code for understanding the actual issue: I'll upload a code that generate a system of boolean equations which shows the issue exactly. This system of equations is extracted from a stream cipher called Bivium-B and I've solved it several times in Sage 7.2, and I'm certain that it has a unique solution, but when I want to solve it via the newer versions of SageMath (after 8.0), solver returns False as the output, which means there is not any solutions! I'll upload the code as soon as possible.

Thanks in advance for your help

Dear Monteli,
Here's the code which shows the issue. This script generates 441 cubic equations for the SBox of the AES cipher. The SBox is a bijective function from GF(2)8 to GF(2)8. for example let (y0, y1, ..., y7) = S(x0, x1, ..., x7) and we have system of 441 equations like this:
f1(x0, ..., x8, y0, ..., y7) = 0
.
.
.
f441(x0, ..., x8, y0, ..., y7) = 0

which it's solutions must satisfy the (y0, y1, ..., y7) = S(x0, x1, ..., x7) relation. Since S is a bijective function from GF(2)8 to GF(2)8, there are at least 256 solutions for the above system of equations. But when I used solve_sat to solve the above system of equations, it returned only 27 solutions which shows that the solve_sat can't find all solutions even the parameter "n" in solve_sat command is equal to "infinity"!

A Sage script which generates the cubic equations of the AES SBox and solves it via the solve_sat command:

from sage.rings.polynomial.multi_polynomial_sequence import PolynomialSequence
from sage.sat.boolean_polynomials import solve as solve_sat
sr = sage.crypto.mq.SR(1, 4, 4, 8, allow_zero_inversions = True)
sb = sr.sbox()
eqs = sb.polynomials(degree = 3)
eqs = PolynomialSequence(eqs)
variables = map(str, eqs.variables())
variables = ",".join(variables)
R = BooleanPolynomialRing(16, variables)
eqs = map(R, eqs)
%time sls_aes = solve_sat(eqs, n = infinity, s_verbosity = 8)
print("Number of solutions = %s" % len(sls_aes))

When I executed the above code in my own laptop, I got the bellow solutions:

CPU times: user 6.49 s, sys: 10.3 s, total: 16.8 s
Wall time: 23.1 s
Number of solutions = 27

In addition, I feel the run-time of solve_sat has been increased in comparison with previous versions.

comment:5 Changed 4 years ago by Hosein Hadipour

Status: needs_infoneeds_work

comment:6 Changed 4 years ago by gh-jvpeetz

Hi,

I can add a small example which might help to fix the problem:

varl = ['k{0}'.format(p) for p in range(29)]  # no solution

B = BooleanPolynomialRing(names = varl)
B.inject_variables(verbose=False)

keqs = [
    k0 + k6 + 1,
    k3 + k9 + 1,
    k5*k18 + k6*k18 + k7*k16 + k7*k10,
    k9*k17 + k8*k24 + k11*k17,
    k1*k13 + k1*k15 + k2*k12 + k3*k15 + k4*k14,
    k5*k18 + k6*k16 + k7*k18,
    k3 + k26,
    k0 + k19,
    k9 + k28,
    k11 + k20]

from sage.sat.boolean_polynomials import solve as solve_sat

kpsol = solve_sat(keqs, n=1)

The Boolean equation system (ANF) definitly has a solution but solve_sat() returns False.

The interface to cryptominisat implemented in src/sage/sat/solvers/cryptominisat.py has a bug in the enumeration of the CNF variables. This bug results in faulty ANF to CNF conversion and failures in the solver routine sat.boolean_polynomials.solve().

When using the ANF to CNF converter CNFEncoder with the solver CryptoMiniSat (which the function sat.boolean_polynomials.solve() does) with this example some of the variable indices are re-used for different monomials of the ANF which is a bug.

The variable indices used when converting the fifth equation (k1*k13 + k1*k15 + k2*k12 + k3*k15 + k4*k14) get re-used when converting equations with the monomials k26 and k28.

When using the DIMACS solver instead, the conversion to CNF works correctly, the resulting CNF file can be solved by a SAT solver.

Comparing the functions in src/sage/sat/solvers/cryptominisat.py and src/sage/sat/solvers/dimacs.py I see discrepancies, for example in the functions var() and add_clause().

This bug is also present in the picosat binding, I think.

Any ideas?

Regards, Jörg.

comment:7 Changed 4 years ago by gh-jvpeetz

A remedy for this bug is (at least for my little example) to change the var() function in local/lib/python2.7/site-packages/sage/sat/solvers/cryptominisat.py (source file is in src/sage/sat/solvers/cryptominisat.py) from

        return self._nvars + 1

to

        self._nvars += 1
        return self._nvars

which corresponds to the code of the DIMACS solver. Removing the file cryptominisat.pyc, starting sage and importing CryptoMiniSat will use the modified version of cryptominisat.py. With this modification the ANF to CNF converter CNFEncoder produces the same CNF with CryptoMiniSat as with DIMACS as solver. And my example can be solved by sat.boolean_polynomials.solve().

Regards, Jörg.

Last edited 4 years ago by gh-jvpeetz (previous) (diff)

comment:8 Changed 4 years ago by Hosein Hadipour

Dear Jörg,

I did as you said. It works for my example too. I think this modification solves the problem. I appreciate your time and efforts.

Sincerely, H. Hadipour

Last edited 4 years ago by Hosein Hadipour (previous) (diff)

comment:9 Changed 4 years ago by Thierry Monteil

Great ! Should i go ahead and upload a branch with the fix (and doctests to avoid further regressions), or do you want to fix it yourself ?

Last edited 4 years ago by Thierry Monteil (previous) (diff)

comment:10 Changed 4 years ago by gh-jvpeetz

Hi Thierry,

it's fine with me if you uploa d the fixes. As I mentioned this fix might also apply to the picosat binding.

By the way, thanks for making the newer version of CryptoMiniSat available in SageMath.

Regards, Jörg.

comment:11 Changed 4 years ago by Thierry Monteil

Branch: u/tmonteil/fix_var_for_cryptominisat_and_picosat_solvers

comment:12 Changed 4 years ago by git

Commit: c492724e2af4918c65360b82cded10f1f9d5877b

Branch pushed to git repo; I updated commit sha1. New commits:

c492724#26676 : add doctests for solving boolean polynomial systems with picosat

comment:13 Changed 4 years ago by Thierry Monteil

Authors: Thierry Monteil
Component: packages: experimentalpackages: optional
Keywords: picosat added
Status: needs_workneeds_review
Summary: solve_sat doesn't work correctly after migration of CryptoMiniSat from version 2 to 5Fix var() method for cryptominisat and picosat, which breaks solve_sat for boolean polynomial systems

I fixed the var() methods in cryptominisat and picosat and added the two examples you both provided as doctests to prevent future regressions with both solvers.

comment:14 Changed 4 years ago by Thierry Monteil

Description: modified (diff)

comment:15 Changed 4 years ago by Thierry Monteil

Just to state the obvious: if nobody review this ticket, it will never get merged.

comment:16 Changed 4 years ago by Frédéric Chapoton

Reviewers: Frédéric Chapoton
Status: needs_reviewpositive_review

ok

comment:17 Changed 4 years ago by Frédéric Chapoton

Milestone: sage-pendingsage-8.7

comment:18 Changed 4 years ago by Volker Braun

Branch: u/tmonteil/fix_var_for_cryptominisat_and_picosat_solversc492724e2af4918c65360b82cded10f1f9d5877b
Resolution: fixed
Status: positive_reviewclosed
Note: See TracTickets for help on using tickets.