# Verication
We verify the our proposition in this part. Please refer to [reproducing _scripts.txt](https://github.com/ML-PL/satnet-rules/blob/main/verifications/reproducing_scripts.txt) for more details.
## Naive Rounding
Run SATNet on sudoku4 (see [Experiments](https://github.com/ML-PL/satnet-rules/#experiments)). 
Iterate all the possible threhoding values and test if one of them leads to success:

[//]: # (<pre>)

[//]: # (<code>)

[//]: # (verifications)

[//]: # (├── naive_thresh)

[//]: # (    ├── satnet_m50_a0.pth)

[//]: # (</code>)

[//]: # (</pre>)

```angular2html
cd verifications/naive_thresh
bash naive_thresh.sh
```

## Stream Transformation
Run SATNet on addition and counting tasks (see [Experiments](https://github.com/ML-PL/satnet-rules/#experiments)), and generate all the possible cases for verification:
```angular2html
python data/bits_add/gen_all_pos.py
python data/k_modulo/gen_all_pos.py
```

Check if SATNet and our interpretable rules handle all the cases:
```angular2html
cd verifications/stream
bash streams.sh
```

## Sudoku4 Solving
Run the following command to get a sparse max equality matrix:
```angular2html
python exps/sudoku4.py --model mixnet -- aux 0 --sparse
```
Verify general functional equivalence:
```angular2html
cd verifications/sdk4_solving
bash sdk4_solve_all.sh
```

## Sudoku4 Ground Truth Verification
Generate the human-written constraints and verify:
```angular2html
python exps/sudoku_gt_rules.py
cd verifications/sdk4_gt
bash sdk4_gt.sh
```

## Sudoku4 Additive Prior Knowledge
Generate the ground truth rules:
```angular2html
python exps/sudoku_gt_rules.py && python sudoku_gt_matrix.py
```
Verify prior knowledge can be encoded into the learned rules via simply addition:
```angular2html
cd verifications/w_extra_info
bash sdk4_ranking.sh
```

## Sudoku9 Suboptimal Solution
Run SATNet on sudoku9 and get the max equality matrix with:
```angular2html
python exps/sudoku.py --save_c
```
Verify wrong solutions generated by SATNet is suboptimal solutions for the 
weighted MaxSAT:
```angular2html
cd verifications/subopt9
bash sdk9_subopt.sh
```

[//]: # (<pre>)

[//]: # (<code>)

[//]: # (verifications)

[//]: # (├── stream)

[//]: # (    ├── weights )

[//]: # (        ├── 2_modulo_c_n_3_aux_1.npy)

[//]: # (        └── 4_modulo_c_n_5_aux_2.npy)

[//]: # (        └── 8_modulo_c_n_7_aux_4.npy)

[//]: # (        └── 16_modulo_c_n_9_aux_8.npy)

[//]: # (        └── addition_c_n_5_aux_2.npy)

[//]: # (    └── data)

[//]: # (        ├── 2_modulo_all_pos.pickle)

[//]: # (        └── 4_modulo_all_pos.pickle)

[//]: # (        └── 8_modulo_all_pos.pickle)

[//]: # (        └── 16_modulo_all_pos.pickle)

[//]: # (        └── addition_full_space.pickle)

[//]: # (</code>)

[//]: # (</pre>)

