Comments (3)
Hi,
Sorry, I don't understand. What kind of improvement are we missing? You are trying to simplify:
x1 ⊕ x2 ⊕ x5 = 0
x1 * x2 ⊕ x3 ⊕ x4 ⊕ x6 = 0
As far as I can see, these don't have any common larger-than-1 monomials, and none of them are 2-long or 1-long. They don't share significant parts of their (any-sized) monomials, either. What simplification are we missing here?
You mention: When I use other [CNF] equation simplification tools
-- which ones, and what do these do? And what do you give them as input? Given the CNF, it seems like they managed to remove exactly one clause (15 vs 16)? And they removed zero variables (7 vs 7). In fact, the only difference is:
@@ -2,7 +2,6 @@
-2 -3 -4 5 -7 0
-2 -3 4 -5 -7 0
-2 -3 4 5 7 0
--2 -3 -6 0
-2 3 6 0
2 -3 6 0
2 3 -6 0
@@ -10,7 +9,7 @@
2 -4 5 7 0
2 4 -5 7 0
2 4 5 -7 0
-3 -4 -5 -7 0
-3 -4 5 7 0
-3 4 -5 7 0
-3 4 5 -7 0
+-4 -5 -6 -7 0
+-4 5 -6 7 0
+4 -5 -6 7 0
+4 5 -6 -7 0
Which seems minor, and perhaps also incorrect -- are you 100% sure the clause it removed, -2 -3 -6 0
can be removed without affecting the number of solutions? We output a CNF that is guaranteed to have as many solutions over the inputs as the original ANF. Maybe removing that clause is possible to preserve equisatisfiability, but are you sure it can be removed and preserve the number of solutions?
All in all, your bug report is either misunderstood by me or incomplete. Can you please be more precise, and in particular, can you please let me know why diff above is correct?
from bosphorus.
The other simplification tool in question is the use of the wolframalpha site which offers a logical equation conversion and minimisation program, here is how I went about obtaining the simplified CNF formula for the double equation:
first of all I had to adapt the double equation to the format supported by wolframalpha, reduce the double equation to a single equation:
- initial equations:
x1 ⊕ x2 ⊕ x5 <=> 0
x1 * x2 ⊕ x3 ⊕ x4 ⊕ x6 <=> 0
- ANF format :
x1 + x2 + x5 <=> 0
x1 * x2 + x3 + x4 + x6 <=> 0
- add parentheses respecting the operator priority rules:
(x1 + x2 + x5) <=> 0
((x1 * x2) + x3 + x4 + x6) <=> 0
- replacement of the variables x(n) by the variables (a, b, c, d, e, f) :
(a + b + e) <=> 0
((a * b) + c + d + f) <=> 0
- link equations by an AND operator to form a single equation:
(((a + b + e) <=> 0) * (((a * b) + c + d + f) <=> 0)) <=> 1
- equivalence at 0 :
((((a + b + e) <=> 0) * (((a * b) + c + d + f) <=> 0)) + 1) <=> 0
- change the syntax of the operators:
((((a xor b xor e) <=> 0) and (((a and b) xor c xor d xor f) <=> 0)) xor 1) <=> 0
- result of the CNF conversion and simplification on the Wolframalpha site:
(¬ a ∨ ¬ b ∨ ¬ c ∨ ¬ d ∨ f) ∧
(¬ a ∨ ¬ b ∨ ¬ c ∨ d ∨ ¬ f) ∧
(¬ a ∨ ¬ b ∨ c ∨ ¬ d ∨ ¬ f) ∧
(¬ a ∨ ¬ b ∨ c ∨ d ∨ f) ∧
(¬ a ∨ b ∨ e) ∧
(a ∨ ¬ b ∨ e) ∧
(a ∨ b ∨ ¬ e) ∧
(a ∨ ¬ c ∨ ¬ d ∨ ¬ f) ∧
(a ∨ ¬ c ∨ d ∨ f) ∧
(a ∨ c ∨ ¬ d ∨ f) ∧
(a ∨ c ∨ d ∨ ¬ f) ∧
(¬ c ∨ ¬ d ∨ ¬ e ∨ ¬ f) ∧
(¬ c ∨ d ∨ ¬ e ∨ f) ∧
(c ∨ ¬ d ∨ ¬ e ∨ f) ∧
(c ∨ d ∨ ¬ e ∨ ¬ f)
DIMACS cnf format of the solution :
p cnf 7 15
-2 -3 -4 -5 7 0
-2 -3 -4 5 -7 0
-2 -3 4 -5 -7 0
-2 -3 4 5 7 0
-2 3 6 0
2 -3 6 0
2 3 -6 0
2 -4 -5 -7 0
2 -4 5 7 0
2 4 -5 7 0
2 4 5 -7 0
-4 -5 -6 -7 0
-4 5 -6 7 0
4 -5 -6 7 0
4 5 -6 -7 0
I am not sure that the simplification of wolframalpha preserves all solutions which explains the CNF output formula proposed by the site.
I am still learning the domain, I am sorry I did not assimilate this feature which preserves the number of solutions, I understand now why the CNF formulas of Bosphorus are different.
However, why would you want to preserve all possible combinations of solutions if only one combination of solutions is sufficient to satisfy the CNF equation?
Is there a configuration of the Bosphorus that avoids having a CNF formula that preserves all solutions as on wolframalpha?
thank you for your help and your work
from bosphorus.
However, why would you want to preserve all possible combinations of solutions if only one combination of solutions is sufficient to satisfy the CNF equation?
-- because many use-cases require the user to be able to count the solutions. For example, to calculate propbabilities.
Is there a configuration of the Bosphorus that avoids having a CNF formula that preserves all solutions as on wolframalpha?
-- no. However, the difference is minor, and will not affect the performance at all. It is extremely likely that the transformation used by Wolfram Alpha is nowhere near as sophisticated on complicated examples as Bosphorus. I would strongly suggest checking out a much more complicated equation set. The difference will almost surely be in favour of Bosphorus, by a large margin.
I am closing, because I don't see any issue here, we are doing exactly as we should. The difference is minor, and on larger instances we are almost surely way better. However, if you find an large formula where we are measurably worse, please let us know, and we'll look into it. However, a single clause on a tiny example is simply not a good indicator.
from bosphorus.
Related Issues (20)
- Unexpected behavior on a factored system HOT 3
- Bug in `subsitute` function? HOT 7
- Thoughts on Bosphorus HOT 2
- Bosphorus reports unsat but CryptoMiniSat can solve this SHA-256 CNF HOT 9
- Tests gone missing HOT 4
- How to count the number of solutions to an ANF input?
- Error running: Segmentation fault (core dumped) HOT 2
- CryptoMiniSat embedded in SageMath can solve these ANFs but Bosphous reports UNSAT HOT 5
- --solvewrite() within Bosphorus is faster than Cryptominisat5 to solve cnf file HOT 7
- If the Bosporus has executable file in Windows system? HOT 1
- It can't convert ANF to CNF. HOT 2
- Multi-thread trigger assertion HOT 5
- The executable file about the newest bosphorus HOT 4
- cnf to anf conversion makes it unsat HOT 2
- ANF independent set is not translated to CNF indep set HOT 1
- CNF reading does not care about independent set and will lose/create solutions.
- ANF projection set parsing skips file after first comment HOT 1
- Missing end-to-end tests
- Paper link and bib link broken HOT 1
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.
from bosphorus.