Opened 5 months ago

Closed 4 months ago

#26676 closed defect (fixed)

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

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

Description (last modified by tmonteil)

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 gh-essayhaveusers 5 months ago.

Download all attachments as: .zip

Change History (19)

comment:1 Changed 5 months ago by jdemeyer

Can you be more concrete exactly what the problem is?

comment:2 follow-up: Changed 5 months ago by tmonteil

  • Authors Thierry Monteil deleted
  • Cc tmonteil added
  • Component changed from PLEASE CHANGE to packages: experimental
  • Keywords Thierry Monteil removed
  • Milestone changed from sage-8.5 to sage-pending
  • Status changed from new to needs_info
  • Summary changed from solve_sat doesn't work correctly after Thierry Monteil changed the original CryptoMiniSat Solver to solve_sat doesn't work correctly after migration of CryptoMiniSat from version 2 to 5
  • Type changed from PLEASE CHANGE to defect

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 5 months ago by tmonteil (previous) (diff)

comment:3 in reply to: ↑ 2 ; follow-up: Changed 5 months ago by 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

Last edited 5 months ago by gh-hadipourh (previous) (diff)

Changed 5 months ago by gh-essayhaveusers

comment:4 in reply to: ↑ 3 Changed 5 months ago by gh-hadipourh

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 5 months ago by gh-hadipourh

  • Status changed from needs_info to needs_work

comment:6 Changed 4 months 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 months 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 months ago by gh-jvpeetz (previous) (diff)

comment:8 Changed 4 months ago by gh-hadipourh

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 months ago by gh-hadipourh (previous) (diff)

comment:9 Changed 4 months ago by tmonteil

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 months ago by tmonteil (previous) (diff)

comment:10 Changed 4 months 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 months ago by tmonteil

  • Branch set to u/tmonteil/fix_var_for_cryptominisat_and_picosat_solvers

comment:12 Changed 4 months ago by git

  • Commit set to 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 months ago by tmonteil

  • Authors set to Thierry Monteil
  • Component changed from packages: experimental to packages: optional
  • Keywords picosat added
  • Status changed from needs_work to needs_review
  • Summary changed from solve_sat doesn't work correctly after migration of CryptoMiniSat from version 2 to 5 to Fix 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 months ago by tmonteil

  • Description modified (diff)

comment:15 Changed 4 months ago by tmonteil

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

comment:16 Changed 4 months ago by chapoton

  • Reviewers set to Frédéric Chapoton
  • Status changed from needs_review to positive_review

ok

comment:17 Changed 4 months ago by chapoton

  • Milestone changed from sage-pending to sage-8.7

comment:18 Changed 4 months ago by vbraun

  • Branch changed from u/tmonteil/fix_var_for_cryptominisat_and_picosat_solvers to c492724e2af4918c65360b82cded10f1f9d5877b
  • Resolution set to fixed
  • Status changed from positive_review to closed
Note: See TracTickets for help on using tickets.