SAT solver output parser #86

atimaly · 2024-04-11T15:46:04Z

SAT solver output parser
SAT solver output parser

Description of the Contribution

PR Checklist

I read and agree to CONTRIBUTING.md
I have formatted my code with rustfmt / cargo fmt --all
Commits are named following conventional commits
I have added documentation for new features
The test suite still passes on this PR
I have added tests for new features / tests that would have caught the bug this PR fixes (please explain if not)

rustsat/src/types.rs

rustsat/src/instances/fio.rs

chrjabs

Here is some overall comments. Feel free to ask if you have any questions regarding what I mean. Also, I'm writing these suggestions without checking whether they compile, so take them more as ideas than as exact changes to make.

rustsat/src/instances/fio.rs

chrjabs · 2024-04-12T10:46:54Z

rustsat/src/instances/fio.rs

+            let mut current_assignment = match sat_solver_output {
+                SolverOutput::Sat(ref mut assign) => assign,
+                _ => return Err(anyhow::anyhow!(SatSolverOutputError::Nonsolution)),
+            };
+
+            current_assignment.from_vline(&line_ls)?;


For this entire block of code, see my suggestions on changing from_vline to a constructor, then this becomes a lot simpler.

Suggested change

let mut current_assignment = match sat_solver_output {

SolverOutput::Sat(ref mut assign) => assign,

_ => return Err(anyhow::anyhow!(SatSolverOutputError::Nonsolution)),

};

current_assignment.from_vline(&line_ls)?;

if is_sat {

return SatSolverOutput::Sat(Assignment::from_vline(&line));

}

solution = Some(Assignment::from_vline(&line));

The problem I had with creating a constructor is that there can be multiple v lines and so I did not see how to solve this with the same function.

PS: I am very thankful for the helpful comments.

Right, I forgot about the fact that the assignment might be split over multiple lines. I'll have to think about this a bit, will probably get back with an idea next week.

After thinking about this some more, I still think that for usability and intuitiveness, from_vline should be a constructor. I'd therefore suggest to introduce a second method extend_from_vline that does what your current implementation does. The constructor can then simply initialize a default empty assignment and call extend_from_vline, but it's still available for useability.

rustsat/src/instances/fio.rs

rustsat/src/types.rs

chrjabs · 2024-04-15T08:30:02Z

Another question to keep generally in mind for this is what to treat as an actual error and what to accept even though it might not technically be according to the specification. I try to implement my parsers to still accept things that "make sense". For example if an assignment here is not terminated by a zero, I think that's worth still accepting. On the other hand, if an assignment has conflicting literals, this parser shouldn't silently choose one but actually fail.

chrjabs

Before I give more implementation specific comments, could you please add these basic tests and make sure they pass, so that I don't have to worry about whether the parsing logic is correct when looking at the code? Thanks.

Here are some additional tests that should at the bottom of the types module.

    #[test]
    fn parse_vline() {
        let vline = "v 1 -2 4 -5 6 0";
        let ground_truth = Assignment::from(vec![
            TernaryVal::True,
            TernaryVal::False,
            TernaryVal::DontCare,
            TernaryVal::True,
            TernaryVal::False,
            TernaryVal::True,
        ]);
        assert_eq!(Assignment::from_vline(vline).unwrap(), ground_truth);
        assert_eq!(
            {
                let mut asign = Assignment::default();
                asign.extend_from_vline(vline).unwrap();
                asign
            },
            ground_truth
        );
    }

    #[test]
    #[should_panic]
    fn vline_invalid_lit_from() {
        let vline = "v 1 -2 4 foo -5 bar 6 0";
        Assignment::from_vline(vline).unwrap();
    }

    #[test]
    #[should_panic]
    fn vline_invalid_lit_extend() {
        let vline = "v 1 -2 4 foo -5 bar 6 0";
        let mut assign = Assignment::default();
        assign.extend_from_vline(vline).unwrap();
    }

    #[test]
    #[should_panic]
    fn vline_invalid_tag_from() {
        let vline = "b 1 -2 4 -5 6 0";
        Assignment::from_vline(vline).unwrap();
    }

    #[test]
    #[should_panic]
    fn vline_invalid_tag_extend() {
        let vline = "b 1 -2 4 -5 6 0";
        let mut assign = Assignment::default();
        assign.extend_from_vline(vline).unwrap();
    }

rustsat/src/instances/fio.rs

ChrisJefferson · 2024-04-16T04:03:37Z

Some suggestions from parsing a bunch of SAT output (I'd add tests for all of these):

Some solvers output INDETERMINATE instead of UNKNOWN (I'd treat them exactly the same, in both cases the solver probably ran out of time, or some other limit). For an example discussion, arminbiere/cadical#18

When solvers get very confused they won't output an s line at all. If there is no s line, even if there are v lines, output the solver errored because you can't be sure what happened.

atimaly · 2024-04-16T10:36:47Z

Before I give more implementation specific comments, could you please add these basic tests and make sure they pass, so that I don't have to worry about whether the parsing logic is correct when looking at the code? Thanks.

Here are some additional tests that should at the bottom of the types module.

    #[test]
    fn parse_vline() {
        let vline = "v 1 -2 4 -5 6 0";
        let ground_truth = Assignment::from(vec![
            TernaryVal::True,
            TernaryVal::False,
            TernaryVal::DontCare,
            TernaryVal::True,
            TernaryVal::False,
            TernaryVal::True,
        ]);
        assert_eq!(Assignment::from_vline(vline).unwrap(), ground_truth);
        assert_eq!(
            {
                let mut asign = Assignment::default();
                asign.extend_from_vline(vline).unwrap();
                asign
            },
            ground_truth
        );
    }

    #[test]
    #[should_panic]
    fn vline_invalid_lit_from() {
        let vline = "v 1 -2 4 foo -5 bar 6 0";
        Assignment::from_vline(vline).unwrap();
    }

    #[test]
    #[should_panic]
    fn vline_invalid_lit_extend() {
        let vline = "v 1 -2 4 foo -5 bar 6 0";
        let mut assign = Assignment::default();
        assign.extend_from_vline(vline).unwrap();
    }

    #[test]
    #[should_panic]
    fn vline_invalid_tag_from() {
        let vline = "b 1 -2 4 -5 6 0";
        Assignment::from_vline(vline).unwrap();
    }

    #[test]
    #[should_panic]
    fn vline_invalid_tag_extend() {
        let vline = "b 1 -2 4 -5 6 0";
        let mut assign = Assignment::default();
        assign.extend_from_vline(vline).unwrap();
    }

Currently I have added both yours (@chrjabs ), @ChrisJefferson's and my tests. All of them are passed. For the error checking, currently I only check if error is given back. I couldn't find out how to do anyhow::Error assert_eq!() checking (Quick Googling did not help).

chrjabs · 2024-04-16T10:46:16Z

Looks like the tests I suggested for rustsat/src/types.rs are still missing?

atimaly · 2024-04-16T10:47:42Z

Looks like the tests I suggested for rustsat/src/types.rs are still missing?

Sorry forgot about that part.

ChrisJefferson · 2024-04-16T10:56:49Z

Couple of comments (and note I'm just some person, so obviously don't do what I say if it disagrees with @chrjabs ! )

I don't know if a solver would produce it, but you don't handle:

"c this is a comment\nv 1 -2 4 \ns SATISFIABLE\nv -5 6 0\n";

Because you return early if you have some solution. I'd personally just never return from line.contains("SATISFIABLE"), just remember is_sat, then gather up the solution at the end.

Also, sorry for poorly explaining, I don't think you should error if there are no returned values, having an empty SAT instance is perfectly fine!, just return SAT, and no variables. I just wanted to check that case didn't break.

Also, I think lines 146-163 are a bit messy. I think the cases are:

if !is_sat: In this case something bad has happened, error (as on 146-148 currently, this is right).

After this, we should have a vline (as we know we are satisfiable), so you can just check if you have a solution (if so return it), or if you don't, return NoVline?

atimaly · 2024-04-16T13:07:28Z

Looks like the tests I suggested for rustsat/src/types.rs are still missing?

Added and passed.

chrjabs · 2024-04-16T13:14:00Z

I'll go through this in detail again in the next days. If you (@atimaly) have time before that, feel free to clean up the logic a bit and possibly write some documentation already. From a quick look, I also agree with the comment from @ChrisJefferson, these are exactly the edge cases I was talking about that should be handled "reasonably". You could also run Minisat/glucose/cadical/kissat on an instance and use their output files in tests.

chrjabs

I think we're getting there, this is already significantly more solid code than the first version. I hope you can see why I am relatively picky about catching edge cases we can think of here, if this code is supposed to go into this library I would like the problems I can already see to be worked out.
Thanks for your work on this 👍

rustsat/src/instances/fio.rs

rustsat/src/types.rs

rustsat/src/instances/fio.rs

rustsat/src/types.rs

chrjabs · 2024-04-17T13:34:22Z

rustsat/src/instances/fio.rs

+                _ => return Err(anyhow::anyhow!(SatSolverOutputError::InvalidSLine)),
+            }
+        }
+


Suggested change

if line.starts_with("c s UNKNOWN") {

// special case for CaDiCaL

return Ok(SolverOutput::Unknown);

}

@ChrisJefferson, based on the CaDiCaL discussion you linked, do you think catching this special case makes sense?

chrjabs · 2024-04-17T13:37:09Z

Also, don't worry about the failing macos test, that one has some weird flakeyness that I haven't figured out how to avoid yet.

atimaly · 2024-04-17T13:58:08Z

I think we're getting there, this is already significantly more solid code than the first version. I hope you can see why I am relatively picky about catching edge cases we can think of here, if this code is supposed to go into this library I would like the problems I can already see to be worked out. Thanks for your work on this 👍

I am happy that we are getting there. Also I am really thankful for the comments and suggestions. I fully understand why you would be picky about the edge cases. The edge case that I want to handle most is the case where there is the same literal but with different sign in the solution.

chrjabs

Can you please still include these changes. After that, the last thing I see missing right now are some tests with actual solver output files. So maybe you could run some solvers, e.g., CaDiCaL / MiniSAT on the this instance and this instance, put the solver output files in the data/ directory and include tests for fio::parse_sat_solver_output on those files. That would be great.

chrjabs · 2024-04-23T07:09:12Z

rustsat/src/instances/fio.rs

@@ -66,3 +75,179 @@ pub(crate) fn open_compressed_uncompressed_write<P: AsRef<Path>>(
    }
    Ok(Box::new(io::BufWriter::new(raw_writer)))
 }
+
+/// The possible values a corretly working SAT solver outputs.


Suggested change

/// The possible values a corretly working SAT solver outputs.

/// Possible results from SAT solver output parsing

chrjabs · 2024-04-23T07:09:49Z

rustsat/src/instances/fio.rs

+    Unknown,
+}
+
+/// The possible errors that can happen to a SAT solver's output.


Suggested change

/// The possible errors that can happen to a SAT solver's output.

/// Possible errors in SAT solver output parsing

rustsat/src/instances/fio.rs

chrjabs · 2024-04-23T07:10:57Z

rustsat/src/instances/fio.rs

+    InvalidSLine,
+}
+
+/// The possible errors that can happen to a value line in the SAT solver's output.


Suggested change

/// The possible errors that can happen to a value line in the SAT solver's output.

/// Possible errors in parsing a SAT solver value line

chrjabs · 2024-04-23T07:11:45Z

rustsat/src/instances/fio.rs

+    Emptyline,
+}
+
+//Parse a SAT solver's output


Suggested change

//Parse a SAT solver's output

/// Parses SAT solver output

chrjabs · 2024-04-23T09:22:40Z

rustsat/src/types.rs

+    /// Given a value line of a SAT solver's solution create an Assignment with
+    /// this line's literal values already included


Suggested change

/// Given a value line of a SAT solver's solution create an Assignment with

/// this line's literal values already included

/// Creates an assignment from a SAT solver value line

chrjabs · 2024-04-23T09:24:46Z

rustsat/src/types.rs

+        let line = &line[1..].trim_start();
+        for number in line.trim().split(' ').filter(|x| !x.is_empty()) {


Suggested change

let line = &line[1..].trim_start();

for number in line.trim().split(' ').filter(|x| !x.is_empty()) {

let line = &line[1..];

for number in line.split_whitespace() {

split_whitespace automatically removes empty elements and basically performs the trim operation.

chrjabs · 2024-04-23T09:31:30Z

rustsat/src/types.rs

+
+    /// Parses and saves literals from a value line.
+    pub fn extend_from_vline(&mut self, line: &str) -> anyhow::Result<()> {
+        if !line.starts_with("v ") {


Suggested change

if !line.starts_with("v ") {

for line in line.lines() {

if !line.starts_with("v ") {

I just realized that a user could call this function with a huge string slice that already contains multiple v lines. Even though I would not recommend this, I think it might make sense to still support this usecase. (Of course close the for loop at the end and indent appropriately.)

rustsat/src/types.rs

chrjabs · 2024-04-23T09:38:07Z

rustsat/src/instances/fio.rs

+    #[error("The value line does not start with 'v ' ")]
+    InvalidTag(char),
+    #[error("The output of the SAT solver assigned the same variable different values.")]
+    ConflictingAssignment(types::Var),
+    #[error("Empty value line.")]
+    Emptyline,


Suggested change

#[error("The value line does not start with 'v ' ")]

InvalidTag(char),

#[error("The output of the SAT solver assigned the same variable different values.")]

ConflictingAssignment(types::Var),

#[error("Empty value line.")]

Emptyline,

#[error("The value line does not start with 'v ' but with '{}'")]

InvalidTag(char),

#[error("The output of the SAT solver assigned different values to variable {}")]

ConflictingAssignment(types::Var),

#[error("Empty value line")]

EmptyLine,

chrjabs · 2024-04-23T12:11:00Z

Ah, btw, I'll most likely squash this PR in the end into a single commit anyway, so don't worry about conventional commits right now.

atimaly · 2024-04-24T12:48:41Z

Can you please still include these changes. After that, the last thing I see missing right now are some tests with actual solver output files. So maybe you could run some solvers, e.g., CaDiCaL / MiniSAT on the this instance and this instance, put the solver output files in the data/ directory and include tests for fio::parse_sat_solver_output on those files. That would be great.

I have been trying to make this but for some reason I get back the following message "the trait bound rustsat_minisat::core::Minisat: Solve is not satisfied" for both of the codes below.

use crate::{
            instances::{BasicVarManager, SatInstance},
            solvers,
            solvers::SolverResult,
        };
            let inst: SatInstance<BasicVarManager> =
                SatInstance::from_dimacs_path("./data/AProVE11-12.cnf.gz").unwrap();
            let mut solver = rustsat_minisat::core::Minisat::default();
            solvers::Solve::add_cnf(&mut solver, inst.as_cnf().0);
            //solver.add_cnf(inst.into_cnf().0).unwrap();
            let res = solver.solve().unwrap();
            assert_eq!(res, SolverResult::Sat);

use crate::{
            instances::{SatInstance},
            lit,
            solvers::{Solve, SolveIncremental, SolverResult::{Sat, Unsat}},
        };
        
        let mut instance = SatInstance::<instances::BasicVarManager>::from_dimacs_path("../../data/AProVE11-12.cnf").unwrap();
        let mut solver = rustsat_minisat::core::Minisat::default();
        super::super::super::solvers::Solve::add_cnf(&mut solver, instance.as_cnf().0);
        //super::solvers::Solve::add_cnf(instance.as_cnf().0).unwrap();
        let res = solver.solve().unwrap();

chrjabs · 2024-04-24T13:30:20Z

I have been trying to make this but for some reason I get back the following message "the trait bound rustsat_minisat::core::Minisat: Solve is not satisfied" for both of the codes below.

What are you trying to use this code for? In the tests?
What I meant you should do is use a separately compiled binary of Minisat (e.g., from this repo) and CaDiCal (from this repo) and run those binaries as a CLI tool on the instances in data/ and collect their output. This is entirely separate from Rust and simulates the intended usecase of running an external solver that is not included in RustSAT. You can then use the collected solver output file in tests.

chrjabs · 2024-04-24T13:44:58Z

Well, I just checked this and figured out that Minisat/Glucose don't actually adhere to the output format we're trying to parse here. I ran CaDiCaL/Kissat/Gimsatul instead, here are the 6 output files, please use those in tests.

cadical-AProVW11-12.txt
cadical-smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.txt
kissat-AProVE11-12.txt
kissat-smtlib-qfbv-aigs-exp_con_032_008_0256-tseitin.txt
gimsatul-AProVE11-12.txt
gimsatul-smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.txt

chrjabs · 2024-04-26T12:04:09Z

I think this looks pretty good now. I'll merge this next week, but probably manually instead of on GitHub through this PR. Are you (@atimaly) fine with me removing the authorship of @atimalyfreiburg, which I assume is just another email address of yours?

atimaly · 2024-04-26T12:06:04Z

I think this looks pretty good now. I'll merge this next week, but probably manually instead of on GitHub through this PR. Are you (@atimaly) fine with me removing the authorship of @atimalyfreiburg, which I assume is just another email address of yours?

Yeah, I am fine with removing the @atimalyfreiburg authorship (university email).

allow parsing of output of externally run SAT solvers closes #86 SAT solver output parser SAT solver output parser Error handling Adding constructor and reorganizing code Adding tests and small correction Adding tests for empty solution and error Adding tests for types and correction for parsing Adding InvalidVline error and cleaning up logic docs: Add simple documentation File reading tests and other additions

atimalyfreiburg added 2 commits April 11, 2024 12:45

SAT solver output parser

07c375b

SAT solver output parser

7daf306

suomela reviewed Apr 11, 2024

View reviewed changes

rustsat/src/types.rs Outdated Show resolved Hide resolved

suomela reviewed Apr 11, 2024

View reviewed changes

rustsat/src/types.rs Outdated Show resolved Hide resolved

suomela reviewed Apr 11, 2024

View reviewed changes

rustsat/src/instances/fio.rs Outdated Show resolved Hide resolved

SAT solver output parser Error handling

61c6094

chrjabs requested changes Apr 12, 2024

View reviewed changes

chrjabs changed the title ~~SAT solver output parser corrected~~ SAT solver output parser Apr 12, 2024

Adding constructor and reorganizing code

116a594

chrjabs requested changes Apr 15, 2024

View reviewed changes

rustsat/src/instances/fio.rs Show resolved Hide resolved

rustsat/src/instances/fio.rs Show resolved Hide resolved

atimaly added 2 commits April 16, 2024 11:39

Adding tests and small correction

9cd10be

Adding tests for empty solution and error

a8d45ad

Adding tests for types and correction for parsing

1f431b8

chrjabs requested changes Apr 17, 2024

View reviewed changes

atimaly added 2 commits April 18, 2024 16:33

Adding InvalidVline error and cleaning up logic

8f0cf64

docs: Add simple documentation

bb46402

chrjabs requested changes Apr 23, 2024

View reviewed changes

chrjabs added the enhancement New feature or request label Apr 24, 2024

File reading tests and other additions

f4d19ab

chrjabs added the solvers Related to solver interfaces label Apr 25, 2024

chrjabs added this to the Version 0.5.0 milestone Apr 26, 2024

chrjabs mentioned this pull request Apr 29, 2024

Parse solver output of external solvers #94

Merged

6 tasks

chrjabs closed this in f4ca1ef Apr 29, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

SAT solver output parser #86

SAT solver output parser #86

atimaly commented Apr 11, 2024 •

edited

Loading

chrjabs left a comment

chrjabs Apr 12, 2024

atimaly Apr 12, 2024 •

edited

Loading

chrjabs Apr 12, 2024

chrjabs Apr 15, 2024

chrjabs commented Apr 15, 2024

chrjabs left a comment

ChrisJefferson commented Apr 16, 2024

atimaly commented Apr 16, 2024 •

edited

Loading

chrjabs commented Apr 16, 2024

atimaly commented Apr 16, 2024

ChrisJefferson commented Apr 16, 2024

atimaly commented Apr 16, 2024

chrjabs commented Apr 16, 2024

chrjabs left a comment

chrjabs Apr 17, 2024

chrjabs commented Apr 17, 2024

atimaly commented Apr 17, 2024

chrjabs left a comment

chrjabs Apr 23, 2024

chrjabs Apr 23, 2024

chrjabs Apr 23, 2024

chrjabs Apr 23, 2024

chrjabs Apr 23, 2024

chrjabs Apr 23, 2024

chrjabs Apr 23, 2024

chrjabs Apr 23, 2024

chrjabs commented Apr 23, 2024

atimaly commented Apr 24, 2024 •

edited by chrjabs

Loading

chrjabs commented Apr 24, 2024

chrjabs commented Apr 24, 2024

chrjabs commented Apr 26, 2024

atimaly commented Apr 26, 2024

+    if line.starts_with("c s UNKNOWN") {
+        // special case for CaDiCaL
+        return Ok(SolverOutput::Unknown);
+    }

	/// The possible values a corretly working SAT solver outputs.
	/// Possible results from SAT solver output parsing

	/// The possible errors that can happen to a SAT solver's output.
	/// Possible errors in SAT solver output parsing

	/// The possible errors that can happen to a value line in the SAT solver's output.
	/// Possible errors in parsing a SAT solver value line

		/// Given a value line of a SAT solver's solution create an Assignment with
		/// this line's literal values already included

	/// Given a value line of a SAT solver's solution create an Assignment with
	/// this line's literal values already included
	/// Creates an assignment from a SAT solver value line

		let line = &line[1..].trim_start();
		for number in line.trim().split(' ').filter(\|x\| !x.is_empty()) {

	if !line.starts_with("v ") {
	for line in line.lines() {
	if !line.starts_with("v ") {

SAT solver output parser #86

SAT solver output parser #86

Conversation

atimaly commented Apr 11, 2024 • edited Loading

Description of the Contribution

PR Checklist

chrjabs left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

atimaly Apr 12, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chrjabs commented Apr 15, 2024

chrjabs left a comment

Choose a reason for hiding this comment

ChrisJefferson commented Apr 16, 2024

atimaly commented Apr 16, 2024 • edited Loading

chrjabs commented Apr 16, 2024

atimaly commented Apr 16, 2024

ChrisJefferson commented Apr 16, 2024

atimaly commented Apr 16, 2024

chrjabs commented Apr 16, 2024

chrjabs left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chrjabs commented Apr 17, 2024

atimaly commented Apr 17, 2024

chrjabs left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chrjabs commented Apr 23, 2024

atimaly commented Apr 24, 2024 • edited by chrjabs Loading

chrjabs commented Apr 24, 2024

chrjabs commented Apr 24, 2024

chrjabs commented Apr 26, 2024

atimaly commented Apr 26, 2024

atimaly commented Apr 11, 2024 •

edited

Loading

atimaly Apr 12, 2024 •

edited

Loading

atimaly commented Apr 16, 2024 •

edited

Loading

atimaly commented Apr 24, 2024 •

edited by chrjabs

Loading