Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Miscellaneous fixes #1

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Miscellaneous fixes #1

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
0e19b3f
Fix compilation-breaking typo.
waywardmonkeys May 5, 2018
5ca601c
Fix typos in comments.
waywardmonkeys May 5, 2018
9b19a8b
Replace tabs with spaces to get things lined up.
waywardmonkeys May 5, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 12 additions & 12 deletions microsat.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ void restart (struct solver* S) { // Perform a
S->processed = S->forced; } // Reset the processed pointer

void assign (struct solver* S, int* reason, int forced) { // Make the first literal of the reason true
int lit = reason[0]; // Let lit be the first ltieral in the reason
int lit = reason[0]; // Let lit be the first literal in the reason
S->false[-lit] = forced ? IMPLIED : 1; // Mark lit as true and IMPLIED if forced
*(S->assigned++) = -lit; // Push it on the assignment stack
S->reason[abs (lit)] = 1 + (int) ((reason)-S->DB); // Set the reason clause of lit
Expand Down Expand Up @@ -97,7 +97,7 @@ int implied (struct solver* S, int lit) { // Check if lit(eral)
while (*(++p)) // While there are literals in the reason
if ((S->false[*p] ^ MARK) && !implied (S, *p)) { // Recursively check if non-MARK literals are implied
S->false[lit] = IMPLIED - 1; return 0; } // Mark and return not implied (denoted by IMPLIED - 1)
S->false[lit] = IMLPIED; return 1; } // Mark and return that the literal is implied
S->false[lit] = IMPLIED; return 1; } // Mark and return that the literal is implied

int* analyze (struct solver* S, int* clause) { // Compute a resolvent from falsified clause
S->res++; S->nConflicts++; // Bump restarts and update the statistic
Expand Down Expand Up @@ -136,7 +136,7 @@ int propagate (struct solver* S) { // Performs unit propagation
int* watch = &S->first[lit]; // Obtain the first watch pointer
while (*watch != END) { // While there are watched clauses (watched by lit)
int i, unit = 1; // Let's assume that the clause is unit
int* clause = (S->DB + *watch + 1); // Get the clause from DB
int* clause = (S->DB + *watch + 1); // Get the clause from DB
if (clause[-2] == 0) clause++; // Set the pointer to the first literal in the clause
if (clause[ 0] == lit) clause[0] = clause[1]; // Ensure that the other watched literal is in front
for (i = 2; unit && clause[i]; i++) // Scan the non-watched literals
Expand All @@ -151,11 +151,11 @@ int propagate (struct solver* S) { // Performs unit propagation
if (!S->false[ clause[0]]) { // If the other watched literal is falsified,
assign (S, clause, forced); } // A unit clause is found, and the reason is set
else { if (forced) return UNSAT; // Found a root level conflict -> UNSAT
int* lemma = analyze (S, clause); // Analyze the conflict return a conflict clause
int* lemma = analyze (S, clause); // Analyze the conflict return a conflict clause
if (!lemma[1]) forced = 1; // In case a unit clause is found, set forced flag
assign (S, lemma, forced); break; } } } } // Assign the conflict clause as a unit
if (forced) S->forced = S->processed; // Set S->forced if applicable
return SAT; } // Finally, no conflict was found
if (forced) S->forced = S->processed; // Set S->forced if applicable
return SAT; } // Finally, no conflict was found

int solve (struct solver* S) { // Determine satisfiability
int decision = S->head; S->res = 0; // Initialize the solver
Expand All @@ -170,7 +170,7 @@ int solve (struct solver* S) { // Determine
S->res = 0; S->fast = (S->slow / 100) * 125; restart (S); // Restart and update the averages
if (S->nLemmas > S->maxLemmas) reduceDB (S, 6); } } // Reduce the DB when it contains too many lemmas

while (S->false[decision] || S->false[-decision]) { // As long as the temporay decision is assigned
while (S->false[decision] || S->false[-decision]) { // As long as the temporary decision is assigned
decision = S->prev[decision]; } // Replace it with the next variable in the decision list
if (decision == 0) return SAT; // If the end of the list is reached, then a solution is found
decision = S->model[decision] ? decision : -decision; // Otherwise, assign the decision variable based on the model
Expand All @@ -181,7 +181,7 @@ int solve (struct solver* S) { // Determine
void initCDCL (struct solver* S, int n, int m) {
if (n < 1) n = 1; // The code assumes that there is at least one variable
S->nVars = n; // Set the number of variables
S->nClauses = m; // Set the number of clauases
S->nClauses = m; // Set the number of clauses
S->mem_max = 1 << 30; // Set the initial maximum memory
S->mem_used = 0; // The number of integers allocated in the DB
S->nLemmas = 0; // The number of learned clauses -- redundant means learned
Expand All @@ -203,7 +203,7 @@ void initCDCL (struct solver* S, int n, int m) {
S->first = getMemory (S, 2*n+1); S->first += n; // Offset of the first watched clause
S->DB[S->mem_used++] = 0; // Make sure there is a 0 before the clauses are loaded.

int i; for (i = 1; i <= n; i++) { // Initialize the main datastructes:
int i; for (i = 1; i <= n; i++) { // Initialize the main datastructures:
S->prev [i] = i - 1; S->next[i-1] = i; // the double-linked list for variable-move-to-front,
S->model[i] = S->false[-i] = S->false[i] = 0; // the model (phase-saving), the false array,
S->first[i] = S->first[-i] = END; } // and first (watch pointers).
Expand All @@ -212,7 +212,7 @@ void initCDCL (struct solver* S, int n, int m) {
int parse (struct solver* S, char* filename) { // Parse the formula and initialize
int tmp; FILE* input = fopen (filename, "r"); // Read the CNF file
do { tmp = fscanf (input, " p cnf %i %i \n", &S->nVars, &S->nClauses); // Find the first non-comment line
if (tmp > 0 && tmp != EOF) break; tmp = fscanf (input, "%*s\n"); } // In case a commment line was found
if (tmp > 0 && tmp != EOF) break; tmp = fscanf (input, "%*s\n"); } // In case a comment line was found
while (tmp != 2 && tmp != EOF); // Skip it and read next line

initCDCL (S, S->nVars, S->nClauses); // Allocate the main datastructures
Expand All @@ -230,8 +230,8 @@ int parse (struct solver* S, char* filename) { // Par
fclose (input); // Close the formula file
return SAT; } // Return that no conflict was observed

int main (int argc, char** argv) { // The main procedure for a STANDALONE solver
struct solver S; // Create the solver datastructure
int main (int argc, char** argv) { // The main procedure for a STANDALONE solver
struct solver S; // Create the solver datastructure
if (parse (&S, argv[1]) == UNSAT) printf("s UNSATISFIABLE\n"); // Parse the DIMACS file in argv[1]
else if (solve (&S) == UNSAT) printf("s UNSATISFIABLE\n"); // Solve without limit (number of conflicts)
else printf("s SATISFIABLE\n") ; // And print whether the formula has a solution
Expand Down