This program generates a random material of the C2 or C6 class, as defined in the associated manuscript. The material has a given defect density, or probability of having a defect at any given grid point. The program then attempts to find a realization of the material using a SAT solver. Here, we include instructions for installing and running the program.

Requirements

The program requires Python and git.

Installing PySAT:

pip install python-sat[aiger,approxmc,cryptosat,pblib]

(see PySAT's dependencies).

Usage

First, get the code:

git clone https://github.com/yotamfe/defect-realizability-solver
cd defect-realizability-solver

Below are several possible usages.

Generating and solving random realizations

To run a C2 grid dislocation problem,

python run_c2.py -l <lattice size> -n <num random realizations> -p <dislocation probability>

Likewise, for C6:

python run_c6.py -l <lattice size> -n <num random realizations> -p <dislocation probability>

For example, to generate and solve 10 random realizations of the 4x4x4 grid dislocation problem with 10 percent dislocation density,

python run_c2.py -l 4 -n 10 -p 0.1

The output should look (e.g.) like this:

Running 10 realizations of size 4x4x4 with 10.0% random dislocations
Running realization 0
Solution found
Running realization 1
Solution found
Running realization 2
Solution found
Running realization 3
Solution found
Running realization 4
Solution found
Running realization 5
Solution found
Running realization 6
Solution found
Running realization 7
Solution found
Running realization 8
Solution found
Running realization 9
Solution found...

The last realization is stored in a file called latest_lattice.txt in the current directory.

Solving precomputed realizations

Alternatively, you can use a method of your choice to generate a text file describing a dislocation configuration, in the same format as the output file generated by the program. Then, you can run the following utility to test it for the existence of a solution. For example, in the C2 case,

python solve_from_file_c2.py -i <input_file>

Similarly, for C6

python solve_from_file_c6.py -i <input_file>

Choosing solver

The SAT solver can be selected by specifying, e.g.,

python solve_from_file_c6.py -i <input_file> -s <solver>

Here <solver> can be either minisat or z3. The use of Z3 requires an installation of Z3 including the python bindings (--python flag for mk_make.py).