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:  sage8.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: 
Description (last modified by )
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 sagedevel: https://groups.google.com/forum/?fromgroups#!topic/sagedevel/2EhgHzGgUnQ
Attachments (1)
Change History (19)
comment:1 Changed 4 years ago by
comment:2 followup: 3 Changed 4 years ago by
Authors:  Thierry Monteil 

Cc:  Thierry Monteil added 
Component:  PLEASE CHANGE → packages: experimental 
Keywords:  Thierry Monteil removed 
Milestone:  sage8.5 → sagepending 
Status:  new → needs_info 
Summary:  solve_sat doesn't work correctly after Thierry Monteil changed the original CryptoMiniSat Solver → solve_sat doesn't work correctly after migration of CryptoMiniSat from version 2 to 5 
Type:  PLEASE CHANGE → 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.
comment:3 followup: 4 Changed 4 years ago by
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 BiviumB 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
Changed 4 years ago by
Attachment:  ph1234.pdf added 

comment:4 Changed 4 years ago by
Replying to ghhadipourh:
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 BiviumB 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 runtime of solve_sat has been increased in comparison with previous versions.
comment:5 Changed 4 years ago by
Status:  needs_info → needs_work 

comment:6 Changed 4 years ago by
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 reused 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 reused 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
A remedy for this bug is (at least for my little example) to change the var()
function in local/lib/python2.7/sitepackages/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.
comment:8 Changed 4 years ago by
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
comment:9 Changed 4 years ago by
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 ?
comment:10 Changed 4 years ago by
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
Branch:  → u/tmonteil/fix_var_for_cryptominisat_and_picosat_solvers 

comment:12 Changed 4 years ago by
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
Authors:  → Thierry Monteil 

Component:  packages: experimental → packages: optional 
Keywords:  picosat added 
Status:  needs_work → needs_review 
Summary:  solve_sat doesn't work correctly after migration of CryptoMiniSat from version 2 to 5 → 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 years ago by
Description:  modified (diff) 

comment:15 Changed 4 years ago by
Just to state the obvious: if nobody review this ticket, it will never get merged.
comment:16 Changed 4 years ago by
Reviewers:  → Frédéric Chapoton 

Status:  needs_review → positive_review 
ok
comment:17 Changed 4 years ago by
Milestone:  sagepending → sage8.7 

comment:18 Changed 4 years ago by
Branch:  u/tmonteil/fix_var_for_cryptominisat_and_picosat_solvers → c492724e2af4918c65360b82cded10f1f9d5877b 

Resolution:  → fixed 
Status:  positive_review → closed 
Can you be more concrete exactly what the problem is?