Support for external solvers and solver output parsing?

[suomela]

Hi, I'm checking if there are any plans or thoughts related to these features that would be useful for us:

1. Ability to read and parse solver output files into rustsat::types::Assignment objects, maybe something like Assignment::from_solver_output(reader) and Assignment::from_solver_output_path(path).
2. Ability to run an external program as a solver. The user would just specify the path + command line arguments, and under the hood it'd invoke an external process, pipe the output of SatInstance::to_dimacs to the solver, check the exit status as usual (supporting also external processes that report satisfiability using error codes 0/10/20) and parse the output using Assignment::from_solver_output.

In particular, we'd be currently interested in using multi-threaded Gimsatul as the external solver.

Here feature 1 alone would already be useful, and even if we had feature 2, we'd still like to have also feature 1, as it'd make it possible to have workflows in which e.g. SAT instance generation and solution parsing is done on one computer, while SAT solving is done in another machine.

If it helps, I can try to find someone who could contribute these features, but I'd like to first know if this makes sense, if this kind of features should be insider RustSAT or in another crate that depends on it, and if there are already some plans related to this?

[chrjabs]

Since I am developing RustSAT mainly based on what I need for my own work, there isn't really a clear roadmap for what I would want to do (except for some rough ideas tracked as issues). That being said, I agree that a more flexible option to include any solver via files/pipes sounds quite helpful, and I think it would nicely extend RustSAT. I can give this a try myself sometime, but if you need it urgently, you would need to find somebody else to contribute this.

[chrjabs]

Skimming through gimsatul a bit right now, it looks like including it via the API more directly is not as trivial as for the other solvers I've worked on so far. So even more reason to add functionality for external solvers.

[chrjabs]

Since I am not sure when I will get to this, I'll drop some notes on how I would approach this here, in case somebody else wants to pick this up. Also, if anybody is interested to do this, feel free to reach out to me to talk about this more.

Solver output parsing:

• Add Assignment::from_vline(line: String) function, creating an assignment from a solver output assignment line (starting with a v, hence dubbed v-line
• Add Assignment::from_solver_output<R: BufRead>(reader: R), scanning through solver output and calling from_vline when a v-line is detected
• Add Assignment::from_solver_output_path<P: AsRef<Path>>(path: P) calling from_solver_output

External solver:

• Implement in rustsat::solvers::external and reexport main type(s) from rustsat::solvers
• One main type ExternalSolver with a ExternalSolver::new(config: Config) initializer
• Config specifies executable path, optional arguments, whether to write output to file or capture via a pipe, ...
• Run solver via std::process::Command
• Detect solving result from exit code or s-line and parse solution from v-line

If I get to this at one point myself, these notes should also be quite helpful.

[atimaly]

Hi @chrjabs. I am currently working on the first problem @suomela mentioned. I have a few questions about the implementation.

1. Is there any style that I have to format my code according to?
2. Can I create new enum for the return value like SATISFIABLE, UNSAT,. I did not see such an enum in the documentation file?

3. This roughly the code if there is anything you want to point out please do so.

   ///Get the solution from a solvers output
   pub fn from_solver_output_path(&mut self, filepath: &str) -> Option<SATRESULT> {
       let sat_solution_file = fs::File::open(filepath).expect("Can not read SAT solution file");
   
       let sat_solution_reader = BufReader::new(sat_solution_file);
   
       let sat_result: &str = "";
   
       for line in sat_solution_reader.lines() {
           let line_ls = line.as_ref().expect("Couldn't read SAT solution line");
   
           if line_ls.starts_with('s') {
               for result_of_sat in ["SATISFIABLE", "UNSATISFIABLE", "UNKNOWN"] {
                   if line_ls.contains(result_of_sat) {
                       //We have a solution line
                       sat_result = result_of_sat;
                   }
               }
           }
   
           if line_ls.starts_with('v') {
               // There is a solution and the literals have values 
               //I assume that the output literal is 2*variable_index + signe
               for number in line_ls.split(' ') {
                   if number.parse::<u32>().is_ok() {
                       let number_v = number.parse::<u32>().unwrap();
                       //End of the value lines
                       if number_v == 0 {
                           continue;
                       }
                       self.assignment[(number_v >> 1) as usize] = match number_v > 0 {
                           true => TernaryVal::True,
                           false => TernaryVal::False,
                       };
                   }
               }
           }
       }
   
       return match sat_result {
           "SATISFIABLE" => Some(SATRESULT::SATISFIABLE),
           _ => None,
       };
   
   }

[chrjabs]

1. Yes, please use rustfmt via cargo fmt --all to format code

I guess I should write some proper contribution guidelines, now that some more people are working with this library.

Some more general thoughts on this now that I see your code:

Maybe it makes more sense to have a separate parsing function within the fio module, something along the lines of this

pub enum SolverOutput {
    Sat(Assignment),
    Unsat,
    Unknown,
}

pub fn parse_sat_solver_output<R: BufRead>(reader: R) -> anyhow::Result<SolverOutput> {
    // Parsing code goes here
    // when encoutering vline, call `Assignment::from_vline`
}

And then in Assignment one could do

impl Assignment {
    pub fn from_solver_output_path<P: AsRef<Path>>(path: P) -> anyhow::Result<Self> {
        let reader = fio::open_compressed_uncompressed_read(path).context("failed to open reader")?;
        match fio::parse_sat_solver_output(reader) {
            SolverOutput::Sat(assignment) => assignment,
            _ => // return some error
        }
    }

    pub fn from_vline(line: &str) -> Assignment {
        // parse the actual vline
    }
}

I guess this would feel a bit more clean to me and the parse_sat_solver_output function could then also be used in the ExternalSolver type in the future.

Two more things:

• Make sure to use Lit::from_ipasir in combination with Lit::vidx to index the assignment correctly
• It would be great if Assignment::from_vline could support the newer v-line format of the MaxSAT evaluation as well (even though I'm not sure there any SAT solvers outputting in the format)

Thanks for working on this and feel free to open a draft pull request once you have some things done, it might be easier to comment on the actual code.

[atimaly]

Hi @chrjabs. I think I am almost finished (okay I just miracolusly used rm -rf in the wrong directory), but still I have one problems now.

1. In the code that you have sent the let reader = fio::open_compressed_uncompressed_read(path).context("failed to open reader")?; variable does not satisfy the BufRead trait and I could not solve this.

[chrjabs]

Just wrap the reader in a std::io::BufReader. In the file parsers in the fio module I'm mostly doing that inside the parser function, but I should change that to not potentially buffer a reader again that is already buffered.

[chrjabs]

For completeness, note that with the just released RustSAT 0.6 you can now use ExternalSolver

[suomela]

Awesome, many thanks!

[atimaly]

Great, thank you so much!

Attila Mályusz

On Thu 17. Oct 2024 at 16:38, Jukka Suomela @.***> wrote:

Awesome, many thanks!

— Reply to this email directly, view it on GitHub https://github.com/chrjabs/rustsat/issues/78#issuecomment-2419735935, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHDEVUQMGHEOABR7ZMNOWWDZ37DWBAVCNFSM6AAAAABP46JWF6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDIMJZG4ZTKOJTGU . You are receiving this because you commented.Message ID: @.***>