Justin Pitera 2.26.23 DAA Spring 23 SAT Bruteforcer SAT BruteForcer is a Java program that takes in DIMACS CNF files and generates all possible variations in a method similar to binary addition. It then tests all the variations against the formula's list of clauses and determines if the formula is satisfiable. When you run the program, you will be brought to a main screen with the following options: 1. Test a specific formula file 2. Test all formula files in the /formulas/ directory 3. View all formula files in the /formulas/ directory 4. Exit the program To test a specific formula file, select option 1 from the main screen and enter the filename of the formula file. The program will generate all possible variations and test them against the formula's list of clauses. If the formula is satisfiable, the program will output "Satisfiable: Yes". If the formula is unsatisfiable, the program will output "Satisfiable: No". To test all formula files in the /formulas/ directory, select option 2 from the main screen. The program will loop through all formula files in the /formulas/ directory, generate all possible variations for each file, and output whether each formula is satisfiable or unsatisfiable. To view all formula files in the /formulas/ directory, select option 3 from the main screen. The program will display a list of all formula files in the /formulas/ directory. To exit the program, select option 4 from the main screen.