Description: Connect here and find the flag: `nc asis-ctf.ir 12435`

After we connect to the server, it show us the following message:

Hmmm, it's seems like it give us a some kind of expression, which `∨`

means **OR**, `∧`

means **AND** and `¬`

means **NOT**. And we have to send "**something**" to make the literal True. After having some discussion with teammates, I finally understand what we should send.

Let us define that `x1`

is a **variable** and `(¬x2 ∨ ¬x4)`

is a **clause**. **The number of the variable depends on how many clause are in the expression**.

For example, for the following expression: `(¬x2 ∨ ¬x4) ∧ (¬x1 ∨ x2) ∧ (x5 ∨ ¬x1) ∧ (x1 ∨ ¬x1) ∧ (x4 ∨ ¬x5)`

there are **5** clauses in the expression, so the number of the variable is **5**, which means `x1`

~`x5`

.

As for the following expression: `(¬x6 ∨ x2) ∧ (x3 ∨ x1) ∧ (¬x5 ∨ ¬x6) ∧ (¬x2 ∨ ¬x7) ∧ (¬x4 ∨ ¬x1) ∧ (x2 ∨ x8) ∧ (¬x6 ∨ ¬x2) ∧ (¬x3 ∨ ¬x7) ∧ (x3 ∨ ¬x6)`

there are **9** clauses in the expression, so the number of the variable should be **9**, which means `x1`

~`x9`

, even though `x9`

doesn't appear in the expression.

We have to send a string which represent the value of each variable, that make the literal **True**.

For instance, as for the expression `(¬x2 ∨ ¬x4) ∧ (¬x1 ∨ x2) ∧ (x5 ∨ ¬x1) ∧ (x1 ∨ ¬x1) ∧ (x4 ∨ ¬x5)`

we can send `00000`

, which makes `(¬0 ∨ ¬0) ∧ (¬0 ∨ 0) ∧ (0 ∨ ¬0) ∧ (0 ∨ ¬0) ∧ (0 ∨ ¬0)`

equals **True**.

And for the expression `(¬x6 ∨ x2) ∧ (x3 ∨ x1) ∧ (¬x5 ∨ ¬x6) ∧ (¬x2 ∨ ¬x7) ∧ (¬x4 ∨ ¬x1) ∧ (x2 ∨ x8) ∧ (¬x6 ∨ ¬x2) ∧ (¬x3 ∨ ¬x7) ∧ (x3 ∨ ¬x6)`

both `110000000`

and `110000001`

will all make the literal True, since `x9`

doesn't appear in the expression.

So we finally know what should we send to pass the level and get the flag, time to write some code. For this challenge I decide to write a python script to calculate the answer and send it automatically.

I assume that the number of variable won't larger than 20 ( just a wild guess, and luckily, I was right ^_^ ). So I decide to calculate the answer by brute-forcing all the possible string. If there are 5 variables, I just went through all the string from `00000`

~ `11111`

. The time complexity is `2^n`

, which isn't very effective, but it can still calculate the right answer in less than 5 seconds.

So here is what I'm going to do:

1. parse the input expression, convert it into a string that `eval`

can recognize & evaluate the result.

2. run through `00...0`

to `11...1`

, substitute variables with `0`

or `1`

3. use `eval`

to evaluate the result. If it's `1`

, send the answer, or else run the next string.

For example, the input expression is `(¬x2 ∨ ¬x4) ∧ (¬x1 ∨ x2) ∧ (x5 ∨ ¬x1) ∧ (x1 ∨ ¬x1) ∧ (x4 ∨ ¬x5)`

After the parsing function, the string will be like this:`(~2 | ~4) & (~1 | 2) & (5 | ~1) & (1 | ~1) & (4 | ~5)`

and then run through `00...0`

to `11...1`

, substitute `1`

,`2`

...to `0`

or `1`

. To ensure the result will be only `1`

or `0`

, each `0`

& `1`

will do the `& 0x1`

operation ( convert operands to 1 bit ). So the final evaluate string will be: `(~0 & 0x1 | ~0 & 0x1) & (~0 & 0x1 | 0 & 0x1) & (0 & 0x1 | ~0 & 0x1) & (0 & 0x1 | ~0 & 0x1) & (0 & 0x1 | ~0 & 0x1)`

Finally, we get the flag!

flag: `ASIS_5b5e15ec25479ac8b743c6e818d75464`